Anthropic's Claude now writes code and proves it safe automatically

Why it matters

Anthropic, working with partner Theorem, used Claude to mathematically verify existing open-source code rather than write new software, generating an enormous volume of formal proofs across libraries in Google's OSS-Fuzz security project within weeks. The model translated crash tests into mathematical problems, analyzed compiled machine code, and produced proofs that an independent checker, Rocq, validates automatically with minimal human review. Along the way Claude found hundreds of bugs that conventional testing had missed, including a logical error that had gone undetected for over a decade in one application, and security flaws in a widely used PDF reader at a pace far exceeding typical annual reports. The context matters: formal verification has historically been so costly that it was reserved for extreme cases like avionics, with even small kernels requiring years of specialist labor. Anthropic acknowledges limits, since proofs hold only under strict conditions such as single-threaded programs and bounded input sizes, and compute costs remain high. Still, the result suggests AI-assisted verification could become routine, with Theorem targeting critical infrastructure like OpenSSL and glibc.