Anthropic uses Claude to formally verify code in 123 open-source libraries

On 22 October 2026 Anthropic's Frontier Red Team described a project, done with the company Theorem, in which Claude wrote formal proofs for real open-source software. Claude turned existing OSS-Fuzz fuzz tests into specifications and proved that 239 entry points across 123 libraries never crash for any input under 64 MB. The proofs work on compiled RISC-V binaries, add up to about 180 million lines of Rocq and are checked by the Rocq proof checker, so they do not need manual review.

While writing the proofs, Claude found and patched bugs that fuzzing had missed, such as an out-of-bounds write in a decompressor that appeared only on inputs of about 20 MB, and it rediscovered CVE-2026-56132 in libexpat. Other experiments covered the zlib code in the Linux kernel and a Python interpreter written in Rust.

Anthropic lists the limits: the proofs assume a single-threaded static binary on RISC-V Linux with musl, while most users run x86 or ARM with glibc, and AddressSanitizer does not catch every memory error. Proofs can take hundreds of millions of tokens; on 36 test tasks Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5. A subset of the proofs and the RISC-V and OS semantics are published, and Theorem offers to run the same pipeline for other open-source projects.