180 Million Lines: The New Math Behind Automated Code Safety

A collaborative effort between Anthropic and Theorem has concluded with the generation of approximately 180 million lines of mathematical proof code. This output, produced in a matter of weeks, represents a significant shift in how software correctness is established. The model verified existing code from 123 open-source libraries, moving beyond simple testing to rigorous mathematical validation.

The primary objective of this initiative is to address the high expense and labor intensity of formal verification. Historically, proving that software runs without errors under all circumstances has been reserved for critical systems like aviation software. A notable example is the seL4 operating system kernel, which required 20 person-years of specialist work to verify. By automating this process, the team aims to make such rigorous checks more routine in the development lifecycle.

The methodology involved translating crash tests from Google's OSS-Fuzz project into mathematical problems. Claude analyzed the compiled machine code to produce extensive proofs, which were then checked by an independent program called Rocq. The researchers describe the process as fully autonomous, noting that it requires minimal human review. While the underlying formal foundations were built by humans at Theorem, the model handled the heavy lifting of proof generation.

The financial implications of this technology are substantial for the software industry. The compute costs are high, with individual proofs consuming hundreds of millions of tokens. However, the potential savings in developer time and reduced review costs could offset these expenses. Anthropic suggests that if AI can verify its own code, trust in AI-generated software will increase, streamlining the entire coding process.

During the verification process, the model identified hundreds of bugs that had escaped conventional testing. These defects often only appear under specific conditions, such as unusually large input files or particular access sequences. In one notable instance, the team found as many security bugs in a single week in a widely used PDF reader as are typically reported for that software in an entire year.

The ability to detect long-standing errors is a key advantage of this approach. Claude caught a logical error that had gone undetected for over a decade. Even when a complete proof fails, the process often surfaces real bugs. This suggests that the attempt to verify code has value in itself, regardless of the final outcome.

Despite these successes, there are strict limitations to what formal verification can achieve. The proofs are valid only under specific conditions, including a particular processor architecture, single-threaded execution, and inputs smaller than 64 MB. In practice, these libraries often run on diverse hardware and configurations, meaning the verification does not cover every possible scenario.

The efficiency of the model is also improving over time. A smaller test run demonstrated that proofs are reusable. Furthermore, newer models are becoming more token-efficient. Opus 5.5, for example, solves half the proofs with about 40 percent fewer tokens than its predecessor, Opus 5. This trend indicates that the cost of verification may decrease as model capabilities advance.

The project suggests a future where AI not only writes code but also guarantees its safety under defined conditions. This shift could move the industry focus from basic programming to rigorous proof of correctness. Anthropic expects that formal verification with AI will soon become as practical as standard testing.

Theorem's roadmap already targets critical infrastructure components like glibc, OpenSSL, and cURL. If these efforts succeed, the consequences could extend well beyond current coding tools. The ability to mathematically prove software safety at scale could transform how critical systems are developed and maintained.