180 Million Lines: How AI Automated the Proving of Software Safety

For decades, proving that software is mathematically error-free was a luxury reserved for high-stakes industries like aviation. The core tension in modern software development is that while coding has become faster, verifying correctness remains prohibitively slow and expensive. However, a recent collaboration between Anthropic and Theorem has demonstrated that artificial intelligence can now bridge this gap, producing roughly 180 million lines of proof code in a matter of weeks. This development suggests a fundamental shift in how the industry might approach software safety, moving from manual auditing to automated mathematical validation.

The historical context explains why this breakthrough matters. Formal verification, the process of mathematically proving code works as intended under all conditions, is notoriously resource-intensive. A previous effort to verify the seL4 operating system kernel required 20 person-years of specialist work. Consequently, such rigorous checks were typically limited to critical systems like Airbus avionics. By leveraging Claude, Anthropic’s model, to handle the heavy lifting, the team has compressed what used to be years of human labor into a few weeks of automated processing.

The methodology did not involve writing new software from scratch. Instead, the model verified existing code by translating crash tests from 123 open-source libraries in Google’s OSS-Fuzz project into mathematical problems. Claude analyzed the compiled machine code and generated extensive proofs to confirm correctness. These proofs are then automatically checked by an independent verification program called Rocq. According to Anthropic, the process is nearly autonomous, requiring minimal human review, although the underlying formal foundations and tools were constructed by human experts at Theorem.

One of the most significant outcomes of this automation was the discovery of latent flaws. While generating proofs, Claude identified hundreds of bugs that conventional testing methods had overlooked. These errors often only manifested under highly specific conditions, such as unusually large input files or particular sequences of memory accesses. The model was permitted to fix these issues itself, demonstrating its ability to act as both a verifier and a remediation tool.

The efficiency of this bug-hunting capability was particularly evident in the verification of a widely used PDF reader. In that specific instance, the team discovered as many security vulnerabilities in one week as are typically reported for that software over an entire year. In another case, Claude identified a logical error that had remained undetected for more than a decade. Anthropic notes that even when a complete proof ultimately fails, the attempt itself surfaces these critical defects, making the process valuable regardless of the final verification status.

Despite these successes, the approach has strict practical limitations. Anthropic clarifies that the label 'formally verified' does not equate to 'error-free' in all real-world scenarios. The mathematical proofs hold only under specific conditions, including a defined processor architecture, single-threaded execution, and input sizes under 64 megabytes. In practical deployment, these libraries often run on diverse hardware and configurations that may fall outside these strict parameters.

The computational cost of this process remains high, with individual proofs requiring hundreds of millions of tokens. While Anthropic has not disclosed the total project costs, the efficiency gains are becoming apparent. Smaller test runs indicate that proofs are reusable and that newer models are significantly more efficient. For example, Opus 5.5 solved half of the proofs using approximately 40 percent fewer tokens than its predecessor, Opus 5. This trend suggests that the economic barrier to entry for formal verification may continue to drop.

If AI can write code and then guarantee its correctness under defined conditions, the industry's focus shifts from questioning whether AI can program to whether it can prove its work is safe. This transition could have consequences that extend well beyond standard coding tools, potentially allowing developers to trust AI-generated software more and spend less time on manual reviews. The potential for cost savings applies not just to verification, but to the entire development lifecycle.

Looking ahead, Anthropic expects formal verification with AI to become as routine as standard testing. Theorem’s roadmap already targets critical infrastructure components, including glibc, OpenSSL, and cURL. If this trajectory holds, the automation of software safety could become a standard part of the development stack, fundamentally altering how reliability is assured in the digital economy.