Anthropic's Claude generates machine-checked correctness proofs for 123 open-source libraries

Anthropic had Claude write mathematical proofs that existing code is correct, producing roughly 180 million lines of proof code across 123 open-source libraries. In the process the model found bugs that years of conventional testing had missed. Anthropic's stated goal is to make AI-driven formal verification as routine as standard testing.

Why it matters: Formal verification has been too labor-intensive for most software, so AI that can write and check proofs at this scale changes its cost curve. As AI-written code and AI-driven attacks both grow, proof-backed correctness is one of few defenses that does not rely on spotting bugs after the fact. Finding bugs in well-tested libraries also suggests the method catches classes of errors that testing structurally misses.