Claude wrote 180 million lines of proofs to check 123 open-source libraries

Anthropic says it worked with Theorem to have Claude produce machine-checked proofs of security properties at the RISC-V assembly level for 239 entry points across 123 open-source libraries. Anthropic’s Frontier Red Team published the work on October 22.

Anthropic calls it “the first large-scale effort to use AI to apply formal verification to production software at the assembly code level.” The company says the work took a few weeks.

What the proofs actually guarantee

The libraries come from Google’s OSS-Fuzz project. Each library’s existing fuzz test became a formal specification with a single rule: the program never crashes on any input under 64 MB. The specification is defined over compiled RISC-V instructions, using Theorem’s formal models of RISC-V and Linux processes, and the Rocq proof checker verifies each proof. According to Anthropic, a developer only has to trust the two models, the exact theorem statements and the checker.

Claude patched the bugs it found first, then proved that each program exits normally, with no memory-safety errors or failed assertions. The proofs assume a single-threaded static binary, a fixed memory budget, a RISC-V CPU and Linux.

The total comes to about 180 million lines of Rocq. A typical proof runs about 600,000 lines and covers binaries with a median of 18,000 RISC-V instructions. Anthropic reports that Claude wrote roughly a billion lines in all, and that about 180 million passed the checker.

Hundreds of bugs, some a fuzzer would miss

Anthropic says the proof attempts surfaced hundreds of bugs, some of which had gone unnoticed for years despite heavy fuzzing. Its examples include a counter underflow in a decompressor that causes an out-of-bounds write, triggered only by inputs of around 20 MB with a rare memory layout, and an image decoder read that needs a 64 MB input and over 2 GB of memory. It also reports rediscovering CVE-2026-56132 in libexpat.

The company adds two claims that outsiders cannot yet check: verification of several widely used applications turned up a logic bug that had been latent for more than a decade, and work on a widely used PDF reader surfaced as many security bugs in one week as are typically reported in a year.

Anthropic also describes side experiments. Claude proved that the Linux kernel’s zlib implementation matches a formal specification of RFC 1950, working on the x86 binary, and repeated this for about six other libraries. A Python interpreter written in Rust matched CPython in 99.95% of 1.7 million random programs, and in the company’s test five of seven deliberately injected bugs survived random testing while all seven broke the proof.

Numbers in context: From person-years to weeks

Anthropic frames the scale against the seL4 kernel, which it says took about 2 person-years to implement and about 20 person-years to formally verify. Formal proofs have traditionally been limited to small, carefully chosen systems for that reason.

The efficiency figures matter as much as the headline. On 36 small verification tasks built from real OSS-Fuzz entry points, Anthropic says Opus 5.5 proved half of them using about 40% fewer tokens than Opus 5. Agents that shared a workspace and could reuse each other’s proofs used 17% fewer tokens than solo agents. Anthropic also concedes that proofs can take hundreds of millions of tokens, so cost remains a barrier.

The result also fits a pattern of security work from the same company. A Techmeme item dated October 21 reported that Claude flagged 493 security issues across 25 open-source projects, covering more than 5 million lines of code. That was bug-finding; this work tries to show the absence of a class of bugs. The defensive angle sits against reports such as our coverage of a hacker who reportedly ran AI agents against scores of sites.

Who can use it, and what to watch

According to the Unite.AI summary of the post, Theorem offers the pipeline free to qualifying open-source projects through its OSS Verify program. Projects enroll by pull request, with review similar to OSS-Fuzz and priority for widely used critical infrastructure. Maintainers receive a Rocq proof that each fuzz target does not crash on inputs up to 64 MiB, and bugs are disclosed privately by email with no deadline. Theorem’s stated roadmap aims at the whole Nix ecosystem, including glibc, OpenSSL and cURL. Anthropic says it released a subset of the proofs and the RISC-V and operating-system semantics on GitHub, while withholding proofs that could reveal an unpatched bug.

The limits are stated plainly by Anthropic. As it puts it, “‘Formally verified’ does not mean ‘bug-free.'” The proofs cover static, single-threaded RISC-V binaries linked against musl libc, while most people run these libraries on x86 or ARM with glibc. AddressSanitizer does not catch every memory-safety bug, only some entry points were verified, and misuse by calling programs could still corrupt memory.

Anthropic also flags the risk that Claude could make a theorem provable by changing a program’s behavior. It says it penalized patches, gave extra credit for proving which inputs a patch changed, and audited all of them. Those controls are the company’s own description and have not been independently reviewed. Signs to watch: whether the semantics extend to x86, ARM or multi-threaded code, how many projects enroll in OSS Verify, and what the per-library token cost turns out to be.