AI Now Verifies Its Own Code With Mathematical Certainty
A new partnership allows an AI model to automatically generate formal proofs for software, identifying hidden bugs that traditional testing methods often miss.
By Malik Salazar ·
For decades, proving that software is mathematically error-free was a task so costly that it was reserved for critical systems like aircraft avionics. That barrier is now crumbling as artificial intelligence begins to handle the heavy lifting of formal verification.
The shift traces back to a fundamental limitation in computer science. Until now, formally verifying a small operating system kernel required approximately twenty person-years of specialist labor. This expense made the method impractical for most commercial software. To solve this, Anthropic collaborated with Theorem to deploy Claude, their large language model, to automate the process. The goal was to move beyond simple code generation and into a realm where the AI could also prove the correctness of the code it produced.
The recent effort involved verifying 123 open-source libraries from Google's OSS-Fuzz security project. In just a few weeks, Claude generated roughly 180 million lines of mathematical proof code. The model did not write new applications but instead translated existing crash tests into mathematical problems. It analyzed the compiled machine code and produced extensive proofs that were then checked by an independent verification program called Rocq. Anthropic describes this workflow as fully autonomous, meaning it required very little human review, although the underlying formal foundations were built by human experts at Theorem.
A significant benefit of this approach is the discovery of latent bugs. While generating proofs, Claude identified hundreds of errors that conventional testing had missed. These defects often only appeared under extreme conditions, such as unusually large input files or specific access sequences. In one notable instance, the team found as many security flaws in a single week for a widely used PDF reader as are typically reported in an entire year. In another case, the model caught a logical error that had remained undetected for over a decade.
However, the technology comes with strict practical limits. Formal verification does not guarantee that software is error-free in every possible scenario. The proofs are valid only under specific conditions, including a particular processor architecture, single-threaded execution, and inputs under 64 MB. Since many libraries run on diverse hardware and configurations, the scope of the verification is narrower than real-world usage.
The compute costs for this process are also substantial, with individual proofs consuming hundreds of millions of tokens. Despite this, the efficiency gains are significant. Newer models are proving to be more efficient, with recent versions solving half the proofs using about 40 percent fewer tokens than previous iterations. This efficiency suggests that the cost of verification could drop significantly over time.
The next steps for this technology involve expanding its reach to critical infrastructure. Theorem's roadmap targets major systems libraries such as glibc, OpenSSL, and cURL. If AI can reliably verify its own code under defined conditions, the industry may shift its focus from asking if AI can program to asking if it can prove its work is safe. This could make formal verification as routine as standard testing, fundamentally changing how software is built and trusted.
