Claude writes 180 million lines of proof, uncovering vulnerabilities missed by a trillion fuzzing runs

Anthropic Frontier Red Team and Theorem Labs released a report in which Claude was used to complete formal verification of 239 test entry points across 123 open-source code repositories; about 180 million lines of Rocq proofs passed machine checking, finding vulnerabilities that Google OSS-Fuzz's trillion fuzzing runs missed. The method rewrites test entry points into mathematical propositions, requiring proof that no input within 64MiB triggers a crash or ASan error; a stuck proof may mean a bug exists, and after Claude finds a bug it patches it itself and then continues the proof; in a test on a Rust version of the Python interpreter with 7 bugs planted, random testing missed 5, while the proofs found all of them. The proofs are done at the RISC-V machine code level, and Claude also autonomously wrote a mathematical model of the x86 instruction set, finding hundreds of errors in the official x86 documentation and a small number of CPU hardware bugs. Theorem measured verification speed roughly doubling every two months, and proofs for the first batch of 25 libraries and 60 entry points have been made public on GitHub.