Anthropic says Claude formally proved that 239 entry points across 123 open-source libraries cannot crash

On October 22, Anthropic’s Frontier Red Team published work on using Claude for formal verification at scale. With collaborator Theorem, the team turned existing OSS-Fuzz fuzz tests into formal specifications stating that each test never crashes. Claude then proved them for 239 entry points across 123 libraries. The proofs show the programs never trigger memory-safety errors or failed assertions for any input under 64 MB. They were written against compiled RISC-V machine code and checked by the Rocq proof checker. Anthropic calls it the first large-scale effort to use AI to apply formal verification to production software.

According to Anthropic, the effort took a few weeks and produced about 180 million lines of Rocq in total, with a typical proof around 600,000 lines. Hundreds of bugs surfaced during the proof attempts, and Claude patched them. Examples include an out-of-bounds write triggered only by rare inputs of about 20 MB and a rediscovery of CVE-2026-56132 in libexpat. On 36 small verification tasks, Opus 5.5 proved half of them using about 40% fewer tokens than Opus 5.

Anthropic stresses that “formally verified” does not mean “bug-free.” The proofs assume single-threaded RISC-V binaries statically linked with musl libc, while most users run x86 or ARM with dynamically linked glibc. Not every entry point of each library was verified, and a proof can take hundreds of millions of tokens. The company is not releasing proofs that could reveal unpatched bugs.