Anthropic, Theorem use Claude to verify 123 OSS libraries

Anthropic and the startup Theorem have used Claude to produce formal proofs of crash-freedom at the RISC-V assembly level for 239 entry points across 123 open-source libraries drawn from OSS-Fuzz, in what Anthropic's research post calls "the first large-scale effort to use AI to apply formal verification to production software at the assembly code level." The proofs run only against "single-threaded, static RISC-V binaries linked against musl libc," while "most people run these libraries on x86 or ARM and dynamically link them against glibc."

"Most software is riddled with bugs, which AI can now easily find and exploit," the post opens. "The standard defenses against cyberattacks are no longer sufficient: we need ways to prove that code is free of bugs." Formal verification could in principle supply that guarantee, the authors write, "but it has historically required years of expert effort, making it impractical for most real-world projects." Their claim is that an LLM collapses that cost: "In a collaboration with Theorem, however, we show this is no longer the case: LLMs can now produce formal proofs at large scale."

The scale is literal. The proofs "comprise about 180 million lines of Rocq, with a typical proof running to about 600,000 lines." Along the way Claude surfaced "a counter underflow in its copy of a decompressor that led to an out-of-bounds write, but only on inputs of around 20 MB", "an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory", "a rediscovery of CVE-2026-56132 in libexpat", and in a separate application "a previously unknown logic bug that had been latent for more than a decade." Verifying "a widely used PDF reader," the team reports surfacing "as many security bugs in one week as are typically reported in a year." A parallel Rust port of CPython was tested on 1.7 million randomly generated Python programs and showed "identical behavior with CPython in 99.95% of tests."

The authors are blunt about what the proofs do not promise. "'Formally verified' does not mean 'bug-free,'" they write, adding that "ASan doesn't detect all memory safety bugs, and we didn't verify all the entry points for each library."

"Formal verification, which was historically practical only for bespoke expert-crafted guarantees in the most safety-critical code," the post concludes, "will soon be as practical as fuzzing is today for almost all production software."