Anthropic says it proved no crashes across 239 entry points in 123 libraries

Anthropic says the proofs establish that covered programs exit normally without memory-safety errors or failed assertions.[1] The property is stated to cover every input under 64 MB and every modeled Linux response and memory layout.[1] These are proofs about compiled RISC-V instructions, rather than direct proofs over source code.[1] Anthropic describes the work as, to its knowledge, the first large-scale AI formal-verification effort on production software at the assembly-code level.[1]

The project covered 239 entry points across 123 OSS-Fuzz libraries, and Anthropic says it carried out the work for hundreds of projects in Google's OSS-Fuzz initiative.[1] The proofs assume each program is a single-threaded static binary with a fixed memory budget, running on RISC-V and Linux.[1] Anthropic reports about 180 million lines of Rocq across the project, with a typical proof containing about 600,000 lines; binaries covered by a typical proof had a median length of 18,000 RISC-V instructions.[1]

Anthropic says the proof attempts surfaced hundreds of bugs, including logic bugs that do not cause crashes.[1] Reported examples include a decompressor counter underflow leading to an out-of-bounds write on inputs around 20 MB with a rare layout, and an image-decoder out-of-bounds read requiring a 64 MB input and more than 2 GB of memory.[1] Claude also rediscovered CVE-2026-56132 in libexpat, which required deeply nested input.[1] Anthropic cautions that the libraries are not necessarily bug-free.[1]

Anthropic says the Rocq checker verifies each completed proof against its specification, and that developers need to trust only certain artifacts.[1] The company says it is publishing a subset of the proofs and the RISC-V and operating-system semantics, along with complete proofs for fuzz tests that needed no patching and specifications for tests it could not prove.[1] Theorem offers to run the same pipeline for other open-source projects.[1] Unite.AI reports that Anthropic penalized patches and logged and audited them to reduce reward-hacking risk.[2]