AI model generates massive safety proofs for existing software

A major shift in software reliability is underway as an AI model has begun to mathematically prove the safety of existing code without human intervention.

Anthropic collaborated with partner Theorem to deploy its Claude model on a large-scale verification task. The objective was to use artificial intelligence to generate formal proofs of correctness for a significant portion of the open-source ecosystem. This approach addresses a long-standing challenge in the tech industry, where ensuring software runs error-free under all possible conditions has traditionally been prohibitively expensive and time-consuming.

The scale of this automated effort is substantial. In just a few weeks, Claude produced approximately 180 million lines of mathematical proof code. This work covered 123 open-source libraries from Google's OSS-Fuzz security project. Rather than writing new software from scratch, the model focused on validating existing code. It translated crash tests into mathematical problems and analyzed compiled machine code to create these extensive proofs. An independent program called Rocq automatically checks the validity of these proofs, a process that Anthropic says requires almost no human review.

The project has already yielded significant results in bug detection. While generating proofs, Claude identified hundreds of bugs that conventional testing methods had missed. These flaws often only appear under very 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 within a widely used PDF reader as are typically reported for that software in an entire year. The model even caught a logical error that had gone undetected for over a decade.

Despite these successes, the method has strict practical limits. Anthropic notes that formal verification does not guarantee that software is completely error-free in every possible scenario. The proofs only hold under specific conditions, including a defined processor architecture, single-threaded programs, and inputs smaller than 64 MB. In real-world applications, these libraries often run on different hardware and configurations, which may not be covered by the current proofs.

The computational cost remains a significant factor. Individual proofs can consume hundreds of millions of tokens, though Anthropic has not disclosed the total project costs. However, the efficiency is improving with newer models. Opus 5.5, for example, solves half of the proofs using about 40 percent fewer tokens than its predecessor, Opus 5. A smaller test run also indicated that these proofs are reusable, which could lower long-term costs.

This development suggests a future where AI can not only write code but also guarantee its correctness under defined conditions. If this capability becomes standard, the focus will shift from whether AI can program to whether it can prove its code 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 libraries such as glibc, OpenSSL, and cURL, signaling a broader push to secure the foundations of modern software.