Claude now writes code and proves it safe automatically

Anthropic has enabled Claude to both write and verify software with formal proofs. The model produced roughly 180 million lines of proof code for 123 open-source libraries in just a few weeks, along with finding hundreds of bugs that conventional testing had missed. This approach addresses a core issue with AI-generated software, but it still has practical limits.

Proving that software runs error-free under all circumstances has always been prohibitively expensive. A team of specialists needed 20 person-years just to formally verify the small operating system kernel seL4, so the method was reserved for extreme cases like Airbus avionics software.

Anthropic's Frontier Red Team, working with partner Theorem, let Claude take over the proof work instead. The model produced roughly 180 million lines of mathematical proof code in just a few weeks, drawing on test programs from 123 open-source libraries in Google's OSS-Fuzz security project.

Rather than writing new code, Claude verified existing software by translating crash tests into mathematical problems, analyzing the compiled machine code, and producing extensive proofs. An independent verification program called Rocq automatically checks those proofs, and according to Anthropic, the process needs almost no human reviewers. The researchers call it 'fully autonomous' proof generation, though the tools and formal foundations were built by humans at Theorem.

Claude catches bugs that years of testing missed. While generating proofs, Claude ran into hundreds of bugs and was allowed to fix them itself. Many would have slipped past conventional testing because they only show up under very specific conditions, like unusually large input files or a particular sequence of accesses, the researchers say.

What formal verification can and can't do. Anthropic acknowledges that 'formally verified' doesn't mean 'error-free.' The proofs only hold under strict conditions: a specific processor architecture, single-threaded programs, and inputs under 64 MB. In practice, these libraries run on different hardware and in different configurations.

The compute cost is steep, with individual proofs running up hundreds of millions of tokens. Anthropic doesn't report total project costs. But if AI can verify its own code, developers can trust AI-generated software more and spend less time reviewing it. That saves costs not just on verification but on the entire coding process.