Anthropic's Claude wrote machine-checked proofs that 239 fuzz-test entry points, spread across 123 open-source libraries, cannot crash on any input up to 64 MB, under stated assumptions about how the program runs. The proofs cover compiled RISC-V binaries rather than source code, and Theorem, Anthropic's collaborator on the project, supplied the formal models they rest on.
Anthropic's Frontier Red Team took fuzz tests that Google's OSS-Fuzz program already runs, across hundreds of projects, and restated them as a claim: this harness never crashes. Random input generation samples only a sliver of what a program might receive. A proof speaks for every input under the size limit, and the Rocq proof checker, not a reviewer, confirms Claude's argument. The output totals roughly 180 million lines, with a typical proof near 600,000 lines for binaries with a median length of about 18,000 RISC-V instructions.
Claude fixed bugs on the way to a proof. A counter underflow in one decompressor let writes land out of bounds, but only on inputs of around 20 MB with one rare layout. An out-of-bounds read in an image decoder needed a 64 MB input and over 2 GB of memory. Anthropic says many of the bugs are ones a fuzzer would be unlikely to find, since fuzzers mutate small inputs, typically capped at 1 MB. Claude also rediscovered CVE-2026-56132 in libexpat, which needed deeply nested input. Because a model allowed to edit code could cheat by turning a program into one that trivially never crashes, Anthropic penalized every patch, offered extra credit for proving which inputs a patch changes and how few, and audited the edits.
Token cost is one of the key limitations, Anthropic says, since proofs can take hundreds of millions of tokens. On 36 small verification tasks built from OSS-Fuzz code, Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5. Agents allowed to copy one another's finished proofs used 17% fewer tokens than agents working alone. In the full OSS-Fuzz effort, most of each proof covered code every program contains, chiefly C runtime and AddressSanitizer setup, so very different programs ended up with overlapping proofs.
A proof describes only the machine it models. The proofs assume one thread, a statically linked program, a fixed memory ceiling, a RISC-V chip and Linux with musl libc, while most deployments run x86 or ARM chips with glibc. They also cover entry points, not whole libraries, and AddressSanitizer does not catch every memory-safety bug. Anthropic says "formally verified" does not mean bug-free, and that a developer needs to trust three artifacts: the RISC-V and Linux process models, the exact theorem statements and the Rocq checker, along with the hardware, operating system and OCaml compiler the checker relies on. To its knowledge, Anthropic says, this is the first large-scale effort to use AI to formally verify production software at the assembly code level.
Anthropic published a subset of the proofs along with the RISC-V and operating-system semantics. Theorem now offers its AI-driven verification free to qualifying open-source projects through a program called OSS Verify. Per Theorem, eligibility is reviewed one project at a time, on maturity, usage, an OSI-approved license and how much of the code sits on a security boundary, and only core maintainers can enroll. Enrollment is a pull request with OSS-Fuzz-style project files, and the build must yield static riscv64 binaries, which may mean porting. Bugs go privately to the project's contact, and proofs are published after fixes are public unless the project chooses otherwise. Projects under 1 MB of binary code are likely to be verified sooner, and Theorem's roadmap for the Nix ecosystem names glibc, OpenSSL and cURL as targets.
