Claude writes code and mathematically proves it is safe, according to Anthropic and Theorem

Anthropic has used Claude to mathematically prove that existing code is correct. According to The Decoder’s article, the approach tackles a central problem of AI-generated software, though it has strict practical limits.

Until now, proving that a program runs without errors under all circumstances was prohibitively expensive. A team of specialists needed 20 person-years to formally verify seL4, a small operating system kernel, so the method was reserved for extreme cases such as Airbus avionics software.

Anthropic’s Frontier Red Team, together with its partner Theorem, let Claude take on the work of writing the proofs. The model produced some 180 million lines of mathematical proof code in a few weeks, based on test programs from 123 open-source libraries in Google’s OSS-Fuzz security project.

Claude did not write new code but verified existing software: it translated fault tests into mathematical problems, analyzed the compiled machine code and generated extensive proofs. An independent verification program, Rocq, automatically checks those proofs, and according to Anthropic the process requires hardly any human reviewers. The researchers describe it as “fully autonomous” proof generation, although the tools and formal foundations were built by people at Theorem.

During the process, Claude found hundreds of bugs and was allowed to fix them. Many would have gone unnoticed in conventional testing because they only appear under very specific conditions, such as unusually large input files or a particular sequence of accesses. In the attempt to verify a widely used PDF reader, the team found in one week as many security bugs as are typically reported for that software in an entire year. In another application, Claude detected a logic error that had gone undiscovered for more than a decade. Anthropic notes that even if a full proof ultimately fails, the attempt still surfaces real bugs.

Anthropic acknowledges that “formally verified” does not mean “bug-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 other hardware and with other configurations. The compute cost is also high: each proof can consume hundreds of millions of tokens, and Anthropic does not disclose the project’s total cost.

A smaller test showed that the proofs are reusable and that newer models are more efficient: according to the article, Opus 5.5 solves half of the tests with roughly 40% fewer tokens than Opus 5.

The broader takeaway is that if AI can verify its own code, developers could place more trust in AI-generated software and spend less time reviewing it. The question would shift from “can AI code?” to “can AI prove that the code it writes is safe?” Anthropic hopes AI-driven formal verification will become as practical as standard testing, and Theorem’s roadmap already targets critical infrastructure such as glibc, OpenSSL and cURL.

Note: the downloaded text is The Decoder’s full article, which is based on Anthropic’s announcement; the figures cited are those published by that outlet.