Anthropic and Theorem claim AI can now mathematically certify code safety

In a development that challenges long-standing assumptions about software reliability, Anthropic has announced that its Claude model can now generate mathematical proofs to verify the correctness of existing code. Working in partnership with Theorem, the company claims the system operates with minimal human intervention, effectively automating a process that previously required armies of specialized engineers. The announcement lands as the industry grapples with the risks of AI-generated software, offering a potential solution to the trust gap between code creation and code validation.

The core of the project involves using Claude to formally verify software from the Google OSS-Fuzz security project, a repository of 123 open-source libraries. Rather than writing new applications, the model translated crash tests into mathematical problems and analyzed compiled machine code to produce extensive proofs. According to Anthropic, the system generated approximately 180 million lines of proof code over a few weeks. An independent verification program called Rocq then checks these proofs, a process the researchers describe as "fully autonomous," although they acknowledge that the underlying formal foundations and tools were built by human experts at Theorem.

The practical impact of this automation is already visible in the number of defects identified. During the verification process, Claude encountered and fixed hundreds of bugs that had eluded conventional testing methods. The researchers note that many of these issues only manifested under specific conditions, such as unusually large input files or particular sequences of data access. In one notable instance, while verifying a widely used PDF reader, the team discovered as many security vulnerabilities in a single week as are typically reported for that software in an entire year. In another case, a logical error that had persisted for over a decade was finally caught.

Despite these findings, the term "formally verified" carries specific caveats that do not equate to absolute error-free performance. Anthropic acknowledges that the proofs are valid only under strict conditions, including a specific processor architecture, single-threaded execution, and input sizes under 64 megabytes. In real-world scenarios, these libraries often run on diverse hardware and in more complex configurations. This discrepancy between the theoretical proof and the practical deployment environment remains a significant open question for developers considering the adoption of this technology.

The computational cost of this process is also a point of scrutiny. Individual proofs can consume hundreds of millions of tokens, representing a substantial resource expenditure. While Anthropic has not disclosed the total project costs, the company highlights that newer models are becoming more efficient. For example, Opus 5.5 reportedly solves half the required proofs using about 40 percent fewer tokens than its predecessor, Opus 5. Additionally, a smaller test run indicated that the generated proofs are reusable, suggesting that the initial high cost might be amortized over time.

Historically, formal verification was reserved for extreme cases due to its prohibitive cost. A team of specialists once required 20 person-years to verify the small operating system kernel seL4, a task that was typically limited to critical systems like Airbus avionics. By leveraging AI, Anthropic aims to make this level of rigor as routine as standard testing. The company’s Frontier Red Team believes that if AI can write code and guarantee its correctness under defined conditions, the industry can shift its focus from merely generating code to certifying its safety.

The implications of this shift extend beyond current coding tools. If AI-generated software can be mathematically certified, developers may spend less time on manual review, reducing costs across the entire coding process. Theorem’s roadmap already targets critical infrastructure components such as glibc, OpenSSL, and cURL, signaling an intent to apply this method to the foundational layers of the internet. However, until the practical limits of hardware and input constraints are addressed, the method remains a powerful but specialized tool rather than a universal fix for software bugs.

For now, the project stands as a strong argument for the future of software automation. It suggests that the question is no longer whether AI can program, but whether it can prove that its work is safe. As the industry watches these results, the balance between computational efficiency and mathematical certainty will likely define the next phase of AI-driven development.