Anthropic and Theorem Automate Software Safety Checks via Claude

Anthropic’s Frontier Red Team and its partner, Theorem, have demonstrated a method for automatically generating formal proofs of software correctness using the company’s Claude model. This latest development marks a significant shift in how code safety is validated, moving away from traditional testing toward mathematical certainty. The initiative aims to make formal verification a routine part of the software development lifecycle, a process that has historically been reserved for critical systems due to its high cost and complexity.

The scale of the output is substantial. Over a period of just a few weeks, Claude produced approximately 180 million lines of proof code. This work covered 123 open-source libraries drawn from Google’s OSS-Fuzz security project. The computational intensity of the task is notable, with individual proofs consuming hundreds of millions of tokens. While total project costs were not disclosed, the efficiency is improving; newer versions of the model, such as Opus 5.5, are solving half the proofs with roughly 40 percent fewer tokens compared to the previous iteration.

The process involves Claude translating crash tests into mathematical problems and analyzing compiled machine code to produce extensive proofs. An independent verification program named Rocq automatically checks these proofs, a workflow that Anthropic describes as requiring minimal human review. Although the researchers characterize the process as fully autonomous, they acknowledge that the underlying formal foundations and tools were constructed by human engineers at Theorem. This division of labor allows the AI to handle the heavy lifting of proof generation while human experts maintain the theoretical framework.

Beyond generating proofs, the system identified hundreds of bugs that conventional testing methods had previously missed. These defects often only manifest under specific conditions, such as unusually large input files or particular sequences of data access. In one notable instance involving a widely used PDF reader, the team discovered as many security bugs in a single week as are typically reported for that software in an entire year. In another case, Claude uncovered a logical error that had remained undetected for more than a decade.

Despite these achievements, the method has practical limitations. Anthropic clarifies that formal verification does not guarantee a program is entirely error-free. The proofs are valid only under strict conditions, including a specific processor architecture, single-threaded execution, and inputs under 64 MB. Since these libraries often run on varied hardware and configurations, the findings are specific to those defined parameters.

The broader implication is that if AI can verify its own code, developers may place greater trust in AI-generated software, reducing the time spent on manual review. This could lead to significant cost savings across the entire coding process. Anthropic anticipates that AI-driven formal verification will soon become as practical as standard testing. Theorem’s roadmap already targets critical infrastructure components, including glibc, OpenSSL, and cURL, signaling an intent to apply this technology to the foundational layers of modern computing.