180 Million Lines: AI Proves Software Safety at Scale

Formal verification has long been a niche, high-cost process reserved for critical systems like aviation software, but recent developments suggest it may soon become a standard line item in software development budgets. Anthropic has demonstrated that its Claude model can mathematically prove the correctness of existing code at a scale previously thought impossible for AI systems.

The initiative, conducted by Anthropic's Frontier Red Team in partnership with Theorem, involved using Claude to generate formal proofs for 123 open-source libraries. Over the course of a few weeks, the model produced approximately 180 million lines of proof code. This volume of work represents a significant shift in how software reliability might be assured, moving away from manual inspection toward automated mathematical validation.

The approach does not involve writing new applications from scratch. Instead, Claude translates crash tests from the Google OSS-Fuzz security project into mathematical problems. It then analyzes the compiled machine code and generates extensive proofs to verify correctness. An independent verification program called Rocq automatically checks these proofs. Anthropic describes the process as fully autonomous, meaning it requires almost no human reviewers, although the underlying formal foundations and tools were built by humans at Theorem.

The financial and operational implications are significant for developers and enterprises. By automating the proof generation process, the need for specialized human experts is reduced. Historically, formally verifying a small operating system kernel like seL4 required 20 person-years of specialist work. The AI-driven method compresses this timeline dramatically, potentially lowering the cost of ensuring software safety for a wider range of applications.

The system also proved effective at identifying defects that traditional testing methods missed. During the verification process, Claude detected hundreds of bugs and was authorized to fix them. Many of these errors only manifested under specific conditions, such as unusually large input files or particular sequences of data access. In one instance, the team found as many security bugs in a widely used PDF reader in one week as are typically reported for that software in an entire year.

However, the technology comes with strict practical limitations that businesses must consider. Anthropic notes that formal verification does not guarantee a program is error-free in all scenarios. The proofs are valid only under specific conditions, including a specific processor architecture, single-threaded execution, and input files smaller than 64 MB. Since real-world libraries often run on diverse hardware and configurations, the proofs provide a strong baseline but not universal coverage.

The compute costs for this process are substantial. Individual proofs can consume hundreds of millions of tokens. While Anthropic has not disclosed the total project costs, the efficiency gains are evident in model performance. Newer iterations, such as Opus 5.5, solve half of the proofs with about 40 percent fewer tokens than Opus 5, indicating that the process is becoming more cost-effective over time.

The project suggests a shift in the market's focus from whether AI can write code to whether it can prove that code is safe. Anthropic expects formal verification to become as routine as standard testing. Theorem's roadmap already targets critical infrastructure components like glibc, OpenSSL, and cURL, signaling that this technology is moving from experimental to operational in the software supply chain.