Anthropic: Claude writes machine-checked no-crash proofs for 123 OSS libraries
Anthropic and Theorem report that Claude produced RISC-V assembly-level proofs that 239 entry points across 123 open-source libraries never crash for any input under 64 MB under stated assumptions. The release is about 180 million lines of Rocq, checked by an external proof checker. Anthropic stresses that “formally verified” does not mean bug-free.
On Oct 22, 2026, Anthropic’s Frontier Red Team published a research post on work with Theorem: using Claude to produce formal proofs at assembly (RISC-V) scale for production open-source software. Anthropic says this is, to its knowledge, the first large-scale AI effort to apply formal verification to production software at the assembly level. Specs come from existing fuzz harnesses—proving the entry point never crashes for any input under 64 MB (including AddressSanitizer-detected memory errors).
Results (Anthropic’s account): over a few weeks Claude patched bugs it found, then proved no-crash for 239 entry points across 123 OSS-Fuzz libraries—about 180 million lines of Rocq, typically ~600,000 lines per proof for binaries with a median ~18,000 RISC-V instructions. Proofs use Theorem’s RISC-V and Linux process semantics and currently assume a single-threaded static binary with a fixed memory budget on RISC-V/Linux. Anthropic is publishing a subset of proofs and semantics; Theorem offers the same pipeline for other projects and a Claude skill.
Limits are explicit: “formally verified” does not mean “bug-free.” A proof only shows the compiled program meets the formal spec; if the spec or machine model diverges from real deployments (most libraries run on x86/ARM with dynamic glibc), guarantees do not transfer. ASan does not catch every memory bug, and not every entry point was verified. The effort also found long-latent bugs (including an OOB write needing ~20 MB inputs with a rare layout). Claude could patch code while proving; Anthropic describes penalties against reward-hacking the program into a trivially crash-free form.