Anthropic: LLMs make formal software verification feasible at much larger scale
Anthropic
Claude wrote Rocq proofs at the RISC-V assembly level for 239 OSS-Fuzz entry points across 123 open-source libraries, roughly 180 million lines of proof, establishing that the binaries never crash on inputs below 64 MB under a modelled Linux memory layout. The effort surfaced hundreds of bugs, including a rediscovery of CVE-2026-56132 in libexpat, and a companion experiment checked a Claude-built Rust Python interpreter against CPython on over 1.7 million programs with 99.95% agreement.
Why it matters
It is the first large-scale demonstration of AI-authored machine-checked proofs on production code, with guarantees explicitly conditional on specs and a single-threaded RISC-V model rather than amounting to bug-free software.
Importance: 4/5
first large-scale AI-authored formal verification of production code