Anthropic and Theorem Deploy Claude to Generate Formal Proofs of Software Code

Artificial intelligence labs are increasingly focused on automating software development, but Anthropic is tackling a deeper challenge by using its Claude model to mathematically prove the safety of existing software code. The company announced the results of a project conducted with its Frontier Red Team and partner Theorem, marking a significant step in the field of automated formal verification.

Formal verification has historically been prohibitively expensive, requiring specialized teams and decades of effort to validate even small components like operating system kernels. Consequently, the practice has been reserved for critical systems such as avionics software for Airbus aircraft. Anthropic and Theorem aim to change this dynamic by automating the generation of proofs.

In a period of just a few weeks, Claude produced roughly 180 million lines of mathematical proof code. The effort targeted test programs from 123 open-source libraries associated with Google's OSS-Fuzz security project. Rather than generating new code, the model analyzed compiled machine code and translated crash tests into mathematical problems to verify existing software.

The process involved generating proofs that are automatically checked by an independent verification program called Rocq. According to Anthropic, the workflow requires almost no human oversight, allowing the model to produce proofs fully autonomously. While the formal foundations were established by humans at Theorem, the execution of the proof generation was handled by Claude.

During the generation of these proofs, the model encountered hundreds of bugs that it was permitted to fix itself. Anthropic reported that many of these issues would have slipped past conventional testing because they only manifest under specific conditions, such as unusually large input files or particular sequences of accesses. In one instance involving a widely used PDF reader, the team identified as many security bugs in a week as are typically reported for that software in an entire year. In another case, Claude identified a logical error that had remained undetected for more than a decade.

Anthropic acknowledges limitations regarding what formal verification can guarantee. A status of formally verified does not equate to error-free, as the proofs only hold under strict parameters involving a specific processor architecture, single-threaded programs, and inputs under 64 MB. In real-world scenarios, these libraries run on various hardware and in different configurations.

The computational cost for generating these proofs is substantial, with individual proofs running up hundreds of millions of tokens. However, Anthropic did not report the total cost of the project. The company argues that if AI can verify its own code, developers can trust AI-generated software more and reduce the time spent on review, saving costs across the entire coding process.

A smaller test run demonstrated that proofs are reusable. Anthropic noted that newer models are becoming more efficient at this task, with Opus 5.5 solving half the proofs with about 40 percent fewer tokens than Opus 5. The company expects that formal verification with AI will soon become as practical as standard testing.

The project strengthens the case for software automation. If AI can write code and guarantee its correctness under defined conditions, the question shifts from whether AI can program to whether it can prove that the code it writes is safe. Theorem's roadmap already targets critical infrastructure such as glibc, OpenSSL, and cURL.