LLMs are making formal software verification feasible at a much larger scale

gist

Anthropic and Theorem had Claude prove that 239 fuzzing entry points in 123 OSS-Fuzz libraries never crash on any input under 64 MB. The Rocq proofs target compiled RISC-V binaries under formal RISC-V and Linux semantics, totaling about 180 million lines, roughly 600,000 per proof. Proving surfaced hundreds of bugs, including a decompressor out-of-bounds write needing about 20 MB inputs. Opus 5.5 proved half of 36 benchmark tasks with about 40% fewer tokens than Opus 5, and sharing proofs cut tokens 17%. A six-page appendix details the theorems.

ideas

• Existing fuzz tests become specs. Each OSS-Fuzz harness, built with AddressSanitizer, is turned into the theorem that no input under 64 MB faults, aborts or hits unmodeled behavior, so assertions like LZO's compress-decompress round trip get proved too.
• Only a small base must be trusted. Reviewers need to trust the RISC-V and Linux process models, the theorem statements and the Rocq checker, not the proofs; the appendix adds that Claude wrote about one billion lines to land the 180 million that passed.
• Proving finds bugs fuzzers miss. Fuzzers usually cap inputs near 1 MB, while proof attempts reached a 64 MB image-decoder read needing over 2 GB of memory, a rediscovered libexpat CVE and a file-restriction logic bug.
• Other methods also worked. Claude proved the Linux kernel's x86 zlib against an RFC 1950 spec, and built a Verus-proved Python interpreter in Rust that matched CPython on 99.95% of 1.7 million random programs.
• The guarantees have stated limits. Proofs cover single-threaded static RISC-V binaries linked against musl, not deployed x86 or ARM builds with glibc, and ASan does not catch every memory-safety bug.

quotes