Anthropic Claude Generates 180 Million Lines of Code Proofs to Verify Software Safety

180 million lines of mathematical proof code were generated in just a few weeks, marking a significant shift in how software safety is established. This massive output was produced by Anthropic's Claude model, which worked to verify the correctness of existing software rather than creating new applications from scratch. The effort represents a major step toward automating one of the most complex tasks in computer science: proving that code behaves as intended under all possible conditions.

Traditionally, formal verification has been reserved for high-stakes systems because of the immense human effort required. For instance, a team of specialists needed 20 person-years to formally verify the seL4 operating system kernel. Because of this cost, the method was largely limited to critical areas like avionics software for aircraft. By leveraging AI, Anthropic and its partner Theorem have made this process significantly faster and more accessible, allowing for the verification of a much wider range of software components.

The core of this new approach involves translating existing crash tests into mathematical problems. Claude analyzes the compiled machine code of 123 open-source libraries from Google's OSS-Fuzz security project. Instead of writing new logic, the model produces extensive proofs that demonstrate the code's integrity. An independent program named Rocq then checks these proofs automatically, a process that Anthropic describes as needing almost no human reviewers. While the underlying tools and formal foundations were built by humans at Theorem, the actual generation of the proofs is fully autonomous.

One of the most striking outcomes of this project is the discovery of numerous bugs that had eluded conventional testing for years. During the verification process, Claude identified hundreds of errors and was permitted to fix them. Many of these issues only appear under very specific circumstances, such as when processing unusually large input files or during particular sequences of memory access. In one notable case involving a widely used PDF reader, the team found as many security bugs in a single week as are typically reported for that software in an entire year.

The ability to catch subtle logical errors has proven valuable even in cases where a complete proof is not achieved. In one application, Claude detected a logical error that had remained undetected for over a decade. Anthropic notes that even when a full proof ultimately fails, the attempt still surfaces real bugs. This suggests that the verification process adds a layer of safety net that traditional testing methods do not provide, potentially reducing the risk of undetected vulnerabilities in critical software.

However, the term formally verified does not mean the software is entirely error-free. The proofs only hold under strict conditions, including a specific processor architecture, single-threaded programs, and inputs under 64 MB. In real-world scenarios, these libraries often run on different hardware and configurations, which means the verification has practical limits. Additionally, the compute cost remains high, with individual proofs consuming hundreds of millions of tokens. While Anthropic has not disclosed the total project costs, the efficiency gains are becoming apparent as newer models solve problems with fewer resources.

The project also highlights improving efficiency in AI-driven verification. A smaller test run showed that proofs are reusable, and newer models are becoming more efficient. For example, Opus 5.5 solves half the proofs with about 40 percent fewer tokens than its predecessor, Opus 5. This trend suggests that as models improve, the cost and time required for formal verification will decrease, making the process more viable for broader adoption in the software industry.

Looking ahead, this work strengthens the argument for greater software automation. If AI can write code and guarantee its correctness under defined conditions, the industry can shift focus from simply asking if AI can program to asking if it can prove its work is safe. Anthropic expects formal verification with AI to become as routine as standard testing in the near future. Theorem's roadmap already targets critical infrastructure components such as glibc, OpenSSL, and cURL, indicating a clear path toward integrating this technology into the core of the software ecosystem.