Anthropic says Claude wrote formal proofs that 123 open-source libraries cannot crash

In a collaboration with Theorem, Anthropic says it used Claude to prove security properties at the assembly level (RISC-V) in over 100 real-world open-source libraries, which it calls the first large-scale use of AI to formally verify production software at that level.

According to Anthropic:

• What was proved: for 239 fuzz-test entry points across 123 OSS-Fuzz libraries, the programs always exit normally, with no memory-safety errors or failed assertions, for every input under 64 MB. This holds under assumptions: a single-threaded static binary with a fixed memory budget, on a RISC-V CPU running Linux. The proofs total about 180 million lines of Rocq, checked by the Rocq proof checker.
• How: each library's existing fuzz test was turned into a specification ("this test never crashes"), and Claude wrote the proof, patching bugs it found along the way. Anthropic says this found hundreds of bugs, including ones a fuzzer would be unlikely to reach, such as an out-of-bounds write that needs a rare 20 MB input, and a rediscovery of CVE-2026-56132 in libexpat.
• Other experiments: Claude proved the Linux kernel's zlib implementation matches a specification of RFC 1950 at the x86 binary level, and built a Rust Python interpreter whose behavior matched CPython in 99.95% of 1.7 million random programs. Anthropic also says formal-verification attempts on a widely used PDF reader turned up as many security bugs in one week as are typically reported in a year.
• Cost: proofs can take hundreds of millions of tokens. On 36 small verification tasks, Anthropic says Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5, and that agents sharing proofs needed 17% fewer tokens.

Anthropic is publishing a subset of the proofs and the RISC-V and Linux semantics. Theorem offers to run the same pipeline for other open-source projects and is publishing a Claude skill for verifying your own code. Anthropic notes this does not show the libraries are bug-free: remaining bugs would lie in the trusted components or outside the proofs' scope.