AI Model Proves Math Behind 123 Code Libraries in Weeks

Claude generated 180 million lines of mathematical proof code in a few weeks.

Anthropic announced that its Frontier Red Team, working with partner Theorem, used the model to verify existing software. The goal was to mathematically prove that code behaves as expected without running every possible test.

Formal verification has historically been slow and expensive. It took specialists 20 person-years to verify seL4, a small operating system kernel. Because of that cost, the technique was mostly reserved for high-stakes systems like Airbus avionics software.

Instead of writing new software, Claude analyzed compiled machine code from 123 open-source libraries in Google's OSS-Fuzz security project. The model turned crash tests into mathematical problems and constructed proofs to show the code was correct. A separate program called Rocq automatically checks these proofs. Anthropic said the process required almost no human reviewers, though humans built the underlying tools and foundations.

Claude found hundreds of bugs during the process. The team allowed the model to fix them. Many of these errors would likely have been missed by standard testing because they only appear under specific conditions, such as unusually large input files or specific access sequences.

In one instance, the team verified a widely used PDF reader. They found as many security bugs in one week as are usually reported for that software in a full year. In another case, Claude identified a logical error that had gone unnoticed for more than a decade. Anthropic noted that even failed proof attempts can reveal real bugs.

The company clarified that formal verification does not mean the software is error-free. The proofs only hold under specific conditions: a particular processor architecture, single-threaded programs, and inputs smaller than 64 MB. Real-world deployments often use different hardware and configurations, so the proofs may not apply in every situation.

Cost remains a factor. Individual proofs use hundreds of millions of tokens, and Anthropic has not released total project costs. However, a smaller test run showed that proofs can be reused. Opus 5.5 solved half the proofs using about 40 percent fewer tokens than Opus 5.

The project aims to make AI-generated software more trustworthy. Anthropic expects formal verification to become as practical as standard testing. Theorem's roadmap targets critical infrastructure libraries, including glibc, OpenSSL, and cURL.