Anthropic has Claude perform assembly-level formal verification of open-source libraries, producing about 180 million lines of proof code

Anthropic, in collaboration with Theorem, had Claude complete formal verification of 239 test entry points across 123 open-source libraries within a few weeks, producing about 180 million lines of machine-checked proof code. The team says this is the first large-scale formal verification of production software at the assembly code level that it is aware of. Specifically, Claude was made to prove that all inputs within a specified range would not trigger agreed-upon errors, and the proof process in turn helped it find vulnerabilities; for example, in a decompressor it found an out-of-bounds write that is triggered only by a specially arranged input of about 20MB, whereas conventional fuzzing usually limits inputs to within 1MB; the team says it has thereby found hundreds of bugs. In the cJSON library, a 391-line C code parsing entry point corresponds to about 630,000 lines of proof, more than half of which was automatically generated by tools Claude wrote itself, and was ultimately checked by the human-developed Rocq proof checker. The team has released proofs for 25 libraries and 60 test entry points for developers to download and reuse.