Anthropic and Theorem use AI to mathematically verify open source software
A new partnership allows Claude to generate massive formal proofs that check for errors in existing code, a task that previously required decades of human labor.
By Thomas Reynolds ·
Anthropic and its partner Theorem have demonstrated that an artificial intelligence model can mathematically prove the correctness of existing software with a level of speed that human specialists could not match. The collaboration represents a significant shift in how developers might approach code verification, moving the process from a manual, labor intensive task to an automated routine.
Historically, formal verification has been reserved for critical systems due to its high cost. A team of experts previously required twenty person years to verify the seL4 operating system kernel. Because of this expense, the method was largely limited to high stakes environments such as aircraft avionics. The new approach aims to change that dynamic by using AI to handle the heavy lifting.
The project focused on verifying code from 123 open source libraries included in Google's OSS-Fuzz security project. Over a period of just a few weeks, the Claude model generated approximately 180 million lines of mathematical proof code. Instead of writing new applications, the system analyzed existing compiled machine code and translated crash tests into mathematical problems to ensure the software behaved as intended.
An independent verification program called Rocq automatically checks the proofs generated by the AI. According to Anthropic, the process requires almost no human reviewers. The researchers describe the workflow as fully autonomous, although the underlying formal foundations and tools were developed by humans at Theorem. This independence from manual review is a key component of the new methodology.
During the verification process, the model identified hundreds of bugs that conventional testing methods had missed. These errors often only appeared under specific conditions, such as unusually large input files or specific sequences of memory access. In one instance, the team found as many security bugs in a single week for a popular PDF reader as are typically reported for that software in an entire year. The system also detected a logical error that had remained undetected for more than ten years.
Anthropic notes that formal verification does not guarantee that software is completely error free. The proofs are valid only under strict conditions, including a specific processor architecture, single threaded execution, and input sizes under 64 megabytes. Real world applications often run on different hardware and configurations, so the verification is conditional rather than absolute.
The computational cost of the process is substantial, with individual proofs consuming hundreds of millions of tokens. However, the team observed that newer models are becoming more efficient. Opus 5.5 solved half of the proofs with about 40 percent fewer tokens than its predecessor. This efficiency gain suggests that the cost of verification may decrease as model technology improves.
The success of this project strengthens the argument for broader software automation. If AI can write code and prove its safety under defined conditions, developers may trust AI generated software more and spend less time on manual review. Anthropic expects this type of verification to become as routine as standard testing. Theorem's roadmap already targets critical infrastructure libraries such as glibc, OpenSSL, and cURL for similar treatment.
Source: The Decoder
