Anthropic's Claude now writes code and proves it safe automatically
Anthropic's Frontier Red Team, working with partner Theorem, used Claude to generate roughly 180 million lines of mathematical proof code in a few weeks, verifying existing software from 123 open-source libraries in Google's OSS-Fuzz project by translating crash tests into mathematical problems and analyzing compiled machine code, with the Rocq program automatically checking the proofs. The researchers say Claude found hundreds of bugs, including as many security bugs in one week in a widely used PDF reader as are typically reported for that software in a year, and caught a logical error undetected for over a decade. Anthropic notes the proofs hold only under strict conditions—a specific processor architecture, single-threaded programs, and inputs under 64 MB—and that compute costs are steep, with individual proofs running up hundreds of millions of tokens.
Why it matters: It offers a concrete look at AI-assisted formal verification, including its demonstrated bug-finding results and the practical limits Anthropic itself acknowledges.