180 million lines of proof verify 123 legacy libraries

Formal verification has historically been too expensive for most software developers. The process, which proves code runs without error in all circumstances, requires intense specialist effort. The seL4 operating system kernel, for example, took 20 person-years to verify. This cost limited the practice to high-stakes environments like Airbus avionics. Anthropic and Theorem aim to change that dynamic by using AI to automate the work.

The Frontier Red Team at Anthropic partnered with Theorem to apply Claude to this task. Over a period of weeks, the model generated approximately 180 million lines of mathematical proof code. The system analyzed compiled machine code from 123 open-source libraries within Google’s OSS-Fuzz security project. Rather than writing new software, Claude converted existing crash tests into mathematical problems. A separate tool called Rocq automatically checked the validity of these proofs.

The autonomous process uncovered hundreds of bugs that the team was permitted to fix. Many of these errors likely escaped conventional testing because they only appear under narrow conditions, such as unusually large input files or specific access sequences. In one test, the team found as many security bugs in a widely used PDF reader in one week as are typically reported for that software in a full year. In another case, Claude identified a logical error that had remained unnoticed for more than a decade.

The findings suggest that AI can detect defects that are difficult for humans to find manually. The researchers describe the proof generation as fully autonomous, though human experts at Theorem built the underlying formal foundations and tools. The work shifts the focus from whether AI can program to whether it can prove that its code is safe. This approach could allow developers to trust AI-generated software more and reduce manual review time.

The company emphasizes that formal verification does not guarantee a product is error-free. The proofs hold only under specific conditions, including a particular processor architecture, single-threaded execution, and inputs smaller than 64 MB. Real-world deployments often use different hardware and configurations. Cost remains a constraint, as individual proofs consume hundreds of millions of tokens, though total project costs have not been published.

Efficiency is improving as models evolve. A smaller test run showed that Opus 5.5 solves half the proofs using about 40 percent fewer tokens than Opus 5. Theorem’s roadmap now targets critical infrastructure components, including glibc, OpenSSL, and cURL. The project indicates that AI-driven verification could become as practical as standard testing.