Claude just machine-proved 123 open-source libraries crash-free

Fuzzers have hammered these libraries for years, and Claude still found bugs in them. Working with verification firm Theorem, Anthropic had Claude write machine-checked proofs that 239 entry points across 123 OSS-Fuzz libraries cannot crash on any input up to 64 MB. That covers memory-safety errors and failed assertions. The proofs target the compiled RISC-V binary, not the source code, and the Rocq proof checker confirms every one. The full set runs to about 180 million lines of proof, with a typical proof around 600,000 lines, and it took a few weeks.

Trying to prove the code safe turned up hundreds of bugs, which Claude then patched before re-proving the fixed code. One was a counter underflow in a decompressor that caused an out-of-bounds write, triggered only by a rare ~20 MB input. Another was an image-decoder read error that needed a 64 MB file and over 2 GB of RAM. Claude also rediscovered a known libexpat vulnerability and found a file-restriction feature that wasn't always enforced.

Anthropic is upfront about the limits: "formally verified" does not mean "bug-free." The guarantees assume single-threaded, statically linked binaries on a modeled Linux, which is not how most real deployments run. A proof also covers only what the spec describes. To stop Claude from cheating by quietly rewriting the code until a proof passed, its patches were penalized and audited.

Why it matters: formal verification used to be too slow and expensive for anything but tiny codebases, and LLMs are starting to make it practical at scale.