Claude Proves Code Correct, Anthropic Says

Software that runs correctly in every case has traditionally been expensive to certify, a task specialists once needed 20 person-years to complete for a small operating system kernel called seL4.

Anthropic says it used its Claude model to generate mathematical proofs that existing software behaves as intended, work the company frames as a step toward trusting AI-generated code, while stating strict limits on what the proofs guarantee.

Anthropic's Frontier Red Team partnered with Theorem to hand proof generation to Claude. In weeks, the model produced roughly 180 million lines of mathematical proof code, drawing on test programs from 123 open-source libraries in Google's OSS-Fuzz security project.

Claude did not write new software. It verified existing code by converting crash tests into mathematical problems, analyzing compiled machine code and building proofs; a separate program called Rocq checks them automatically. The researchers call proof generation fully autonomous, while noting that humans at Theorem built the tools and formal foundations.

During the work, Claude found hundreds of bugs and was allowed to fix them. The researchers say many would likely have escaped conventional testing because they surface only under narrow conditions, such as unusually large input files or a specific sequence of accesses. While working on a widely used PDF reader, the team turned up as many security bugs in one week as are normally reported for that software across a year. In another application, Claude identified a logical error that had gone unnoticed for more than a decade.

Anthropic states that formally verified does not mean error-free. The proofs hold only under defined conditions: a particular processor architecture, single-threaded programs and inputs under 64 MB. Real-world deployments of these libraries often run on different hardware and configurations.

Cost is another constraint. Individual proofs consume hundreds of millions of tokens, and Anthropic has not published total project costs. A smaller test run indicated proofs can be reused, and efficiency is improving: Opus 5.5 solves half the proofs using about 40 percent fewer tokens than Opus 5.

Anthropic expects formal verification with AI to become as practical as standard testing, and Theorem's roadmap already targets critical infrastructure including glibc, OpenSSL and cURL.