Anthropic proves 123 code libraries work using 180 million lines of math

Anthropic used its Claude model to mathematically verify that 123 open-source code libraries behave correctly. The model generated approximately 180 million lines of mathematical proof code in a matter of weeks.

Formal verification has historically required immense human effort. Experts spent 20 person-years to verify seL4, a small operating system kernel. Because of this cost, the technique was mostly reserved for critical systems like Airbus avionics.

Anthropic's Frontier Red Team partnered with Theorem to automate this process. Claude analyzed compiled machine code and converted crash tests into mathematical problems. A separate program called Rocq automatically checked the resulting proofs. The researchers described the proof generation as fully autonomous, noting that human reviewers were rarely needed.

The work uncovered hundreds of bugs that Claude was allowed to fix. Many of these errors would likely have escaped conventional testing because they only appear under narrow conditions, such as unusually large files or specific access sequences. In one week, the team found as many security bugs in a widely used PDF reader as are usually reported in a full year. Claude also identified a logical error that had gone unnoticed for over a decade.

Anthropic cautioned that formally verified does not mean error-free. The proofs hold only under specific conditions. They apply to a particular processor architecture, single-threaded programs, and inputs smaller than 64 megabytes. Real-world deployments often run on different hardware configurations.

Cost remains a constraint. Individual proofs consume hundreds of millions of tokens, and Anthropic has not published the total project cost. However, the company argues that AI verification could reduce the time developers spend reviewing code. A smaller test run showed that Opus 5.5 solves half the proofs using about 40 percent fewer tokens than Opus 5.

The project targets critical infrastructure next. Theorem's roadmap includes verifying glibc, OpenSSL, and cURL. Anthropic expects AI-driven formal verification to become as practical as standard testing.