Anthropic's Claude now verifies code with mathematical certainty

Software verification has long been a costly process reserved for high-stakes industries like aviation, but new developments suggest that could change. Anthropic has demonstrated that its AI model, Claude, can mathematically prove the correctness of existing software code with a level of autonomy that was previously thought impossible for general-purpose AI.

In collaboration with partner Theorem, Anthropic’s Frontier Red Team tasked Claude with verifying code from 123 open-source libraries included in Google’s OSS-Fuzz security project. Instead of writing new code, the model analyzed compiled machine code and translated crash tests into mathematical problems. Over a period of just a few weeks, Claude generated approximately 180 million lines of proof code. This output was then checked by an independent verification program called Rocq, a process that requires very little human intervention.

The impact of this workflow was immediate and significant. While generating these proofs, Claude identified hundreds of bugs that conventional testing had failed to catch. These errors often only appear under specific conditions, such as unusually large input files or particular memory access sequences. In one notable instance involving a widely used PDF reader, the team found as many security bugs in a single week as are typically reported for that software in an entire year. In another case, Claude detected a logical error that had remained undetected for more than a decade.

However, the process is not without limitations. Anthropic notes that formal verification does not guarantee a program is error-free in every possible scenario. The proofs are valid only under strict conditions, including specific processor architectures, single-threaded execution, and input sizes under 64 megabytes. Furthermore, the computational cost is substantial, with individual proofs consuming hundreds of millions of tokens. Despite this, the company argues that the efficiency gains from AI-verified code could offset these costs across the broader development cycle.

The project also highlights improvements in model efficiency. A smaller test run indicated that newer versions of the model, specifically Opus 5.5, can solve half the proofs using about 40 percent fewer tokens than the previous Opus 5 version. This suggests that the economic viability of AI-driven verification is improving as models become more efficient at handling complex mathematical tasks.

Looking ahead, Anthropic believes that formal verification with AI will become as routine as standard testing. Theorem has already outlined a roadmap to apply this technology to critical infrastructure libraries such as glibc, OpenSSL, and cURL. If AI can both write code and prove its safety under defined conditions, the focus of software engineering may shift from simple code generation to rigorous proof of correctness, potentially transforming how developers approach trust and security in automated systems.