Claude Wrote 180 Million Lines of Proofs for 123 Open-Source Libraries
Anthropic and Theorem used Claude to produce machine-checked proofs that 239 fuzz-test entry points across 123 open-source libraries never crash or violate memory safety for any input under 64 MB, verified at compiled RISC-V level. About 180 million lines of Rocq proofs passed checking, and the effort rediscovered a known libexpat CVE plus bugs that survived trillions of fuzz-testing runs.
On this page
What was proven, and at what level
Anthropic, working with the verification company Theorem, used Claude to prove security properties for 239 fuzz-test entry points drawn from 123 open-source libraries, taken from Google's OSS-Fuzz projects. The guarantee is concrete: the test never crashes for any input under 64 MB, with no memory-safety errors and no assertion failures, checked not at the source level but on the compiled RISC-V machine code, against every modeled Linux operating system response and memory layout. Anthropic describes it as, to its knowledge, the first large-scale AI application of formal verification to production software at assembly level.
The scale is the part that would have sounded absurd two years ago. About 180 million lines of Rocq proofs passed the checker; Claude wrote around one billion lines in total to get there. A typical proof runs about 600,000 lines covering a binary with a median of 18,000 RISC-V instructions. cJSON's 391-line parser produced a 630,000-line proof; fftw3's 51,000 linked lines produced 480,000.
The trust base is the whole story
A formal proof is only as good as what it assumes, and here the trust base has exactly three components: formal models of RISC-V and Linux processes, the exact theorem statements, and the Rocq proof checker itself. Everything else, including Claude's own reasoning, is checked mechanically. That is what separates this from a model claiming code is safe.
The limitations are stated just as plainly. The proofs cover single-threaded, statically linked RISC-V binaries using musl libc, while most real deployments run x86 or ARM with glibc. AddressSanitizer instrumentation does not catch every memory-safety bug, and bugs can still hide in the trusted components. As an exercise in honesty, the side experiments are as interesting as the headline: an effort to generate x86 semantics from documentation found hundreds of documentation errors and some hardware bugs, and a Rust Python interpreter proved against CPython semantics matched on 1.7 million random programs while all seven deliberately injected bugs broke the proof.
The bugs that fuzzing never found
These libraries were not untested. They came from OSS-Fuzz, meaning they had already survived trillions of fuzzing runs, and the proofs still found hundreds of bugs, many of them ones a fuzzer would be unlikely to reach. Examples include a decompressor counter underflow that only corrupts memory on inputs around 20 MB with a rare memory layout, an image decoder out-of-bounds read requiring both a 64 MB input and 2 GB of memory, and the rediscovery of CVE-2026-56132 in libexpat. Verifying one PDF reader surfaced as many bugs in a single week as the project typically receives in a year.
Claude patched the bugs it found before proving the fixed code, and the reward setup penalized patches themselves to keep the agent from cheating its way to a provable program. That detail matters: a verifier plus an agent is only trustworthy if the agent cannot weaken the target to make the theorem easier, and Anthropic built that incentive in explicitly.
What it means beyond the benchmark
Formal verification has been the security community's always-just-over-the-horizon technology: provably correct code, at a cost in expert proof-writing that made it practical only for seL4 microkernels and crypto libraries. The Anthropic result does not end that era, but it moves the line. Theorem is offering the pipeline free through its OSS Verify program, enrollment is a pull request, and the roadmap targets the Nix ecosystem including glibc, OpenSSL and cURL.
For anyone who runs software, the practical takeaway is that proof coverage may become an ordinary property of the libraries you depend on, the way fuzzing went from research curiosity to CI staple. And for anyone following model capability, note what the efficiency numbers say: Opus 5.5 proved half of a shrunken benchmark with about 40 percent fewer tokens than its predecessor, and agents that shared proofs in a workspace cut token use by another 17 percent. The bottleneck in AI-assisted verification is shifting from whether models can reason rigorously to how cheaply they can do it.