Claude Wrote 180 Million Lines of Proof to Show 123 Open-Source Libraries Never Crash

Anthropic's Frontier Red Team and the verification startup Theorem published research on October 22 that they describe as the first large-scale effort to apply formal verification to production software at the assembly code level, with Claude writing the proofs and the Rocq proof assistant checking them mechanically. The claim is narrow and, for once, precisely measurable: 239 entry points across 123 open-source libraries drawn from Google's OSS-Fuzz program, each proven never to crash on any input smaller than 64 megabytes.

The method is the interesting part. Rather than ask the model to write new specifications from scratch, the team converted each project's existing fuzz test into a formal statement, in effect "this test suite always passes," interpreted over Theorem's formal semantics for the RISC-V instruction set and for Linux processes. Each library is compiled to a RISC-V binary, translated into a mathematical model, and then Claude writes a proof that the Rocq kernel either accepts or rejects. A developer only has to trust three artifacts: the RISC-V and Linux models, the theorem statements, and the proof checker.

The scale is unusual. Anthropic says the proofs comprise about 180 million lines of Rocq, with a typical proof running to roughly 600,000 lines for binaries whose median length is 18,000 RISC-V instructions. For comparison, the company notes that the seL4 microkernel took two person-years to build and about 20 person-years to verify by hand. A single 391-line parser in cJSON received a proof of some 630,000 lines.

The bug list is what makes the exercise more than a demonstration. Fuzzers mutate small inputs, typically capped around 1 MB, so several defects sat outside their reach entirely. Claude found a counter underflow in a decompressor that produced an out-of-bounds write only on inputs of about 20 MB with one rare memory layout, and an out-of-bounds read in an image decoder that required a 64 MB input and more than 2 GB of memory to manifest. It independently rediscovered CVE-2026-56132 in libexpat, a heap-based buffer overflow rated 6.9 and fixed in version 2.8.2. It also flagged logic bugs that never crash at all, such as a file-access restriction that is not consistently enforced, which is the class of defect fuzzing cannot see by construction.

Two side studies push the claim beyond C libraries. Claude wrote a formal specification of RFC 1950 and proved that the Linux kernel's zlib implementation matches it at the x86 binary level, using x86 semantics the model generated. In another experiment it built a Python interpreter in Rust and proved adherence to CPython semantics with the Verus tool, reporting a 99.95 percent behavioural match across 1.7 million random programs. A separate effort on a widely used PDF reader turned up, in one week, as many security bugs as are typically reported in a year.

Verification has always lost on cost, and the paper attacks that directly. On 36 tasks drawn from real OSS-Fuzz code, Opus 5.5 completed half the proofs using roughly 40 percent fewer tokens than Opus 5. When agents were allowed to share a workspace and copy each other's proofs, token consumption fell 17 percent, and some agents solved tasks they had failed alone. Because proofs for similar programs share components such as C runtime and AddressSanitizer initialisation, the marginal cost of verifying library number N plus one falls as N grows.

The limitations section is unusually candid, and worth repeating. The proofs cover single-threaded, statically linked RISC-V binaries against musl libc, while most deployments run x86 or ARM, dynamically linked against glibc. Not every entry point of every library was verified. AddressSanitizer does not catch all memory-safety bugs, caller misuse is out of scope, and generating the proofs consumed hundreds of millions of tokens. "Formally verified does not mean bug-free," the team writes; a proof shows the program meets its specification, and a specification converted from a fuzz test is only as good as that test.

There is also a reward-hacking hazard the team had to design around: Claude could in principle make any program provable by rewriting it into something that trivially never crashes. The countermeasure was to penalise patches, award extra credit for proving which inputs a patch changes, and log and audit every patch. Theorem is now offering the same pipeline to open-source projects free of charge and has published a Claude skill for developers who want to start verifying their own code. The near-term value is not a safety certificate for the internet; it is a cheaper way to find the bugs that a trillion fuzz runs never touched.