Claude Generates 180 Million Lines of Proof to Verify Code Safety

Anthropic has demonstrated that its Claude model can autonomously generate mathematical proofs to verify the correctness of existing software, marking a significant shift in how code safety is assured. By partnering with Theorem, the company utilized Claude to analyze and prove the integrity of 123 open-source libraries, a task that historically required extensive human expertise and time. This development suggests that the high cost of formal verification, once reserved for critical systems like aircraft avionics, is becoming accessible for broader software applications.

The scale of the operation is substantial. In a matter of weeks, Claude produced approximately 180 million lines of proof code. This output was derived from test programs associated with Google’s OSS-Fuzz security project. For context, previous efforts to formally verify even small operating system components, such as the seL4 kernel, consumed 20 person-years of specialist labor. By automating this process, the team significantly compressed the timeline required to achieve similar levels of mathematical rigor.

The methodology involves translating crash tests into mathematical problems and analyzing compiled machine code rather than writing new code from scratch. An independent verification program named Rocq automatically checks the generated proofs, reducing the need for human reviewers. While the researchers describe the process as "fully autonomous," the underlying formal foundations and tools were developed by human experts at Theorem. This hybrid approach allows for continuous verification without the bottleneck of manual code review.

Beyond generating proofs, the system identified hundreds of bugs that conventional testing methods had missed. These defects often remained hidden because they only manifested under specific conditions, such as unusually large input files or particular sequences of data access. In one notable instance, the team found as many security bugs in a single week while verifying a widely used PDF reader as are typically reported for that software over an entire year. In another case, Claude detected a logical error that had persisted undetected for more than a decade.

The project does come with strict practical limitations. Anthropic clarifies that "formally verified" does not equate to "error-free" in all contexts. The proofs hold only under specific conditions, including a particular processor architecture, single-threaded programs, and inputs smaller than 64 MB. Since these libraries often run on diverse hardware and configurations in real-world scenarios, the verification provides a strong but conditional guarantee of safety.

The computational cost remains a factor, with individual proofs requiring hundreds of millions of tokens. However, efficiency is improving. Smaller test runs indicate that proofs are reusable, and newer models are becoming more efficient. Specifically, Opus 5.5 solves half the proofs using about 40 percent fewer tokens than its predecessor, Opus 5. This trend suggests that the cost barrier for formal verification will continue to decrease as model efficiency improves.

The broader implication is a shift in the focus of AI software development. The question is no longer just whether AI can write code, but whether it can prove that the code is safe. If AI can guarantee correctness under defined conditions, developers can place greater trust in automated systems. Anthropic expects formal verification to become as routine as standard testing, with Theorem’s roadmap already targeting critical infrastructure libraries such as glibc, OpenSSL, and cURL.