Anthropic and Theorem use Claude to mathematically verify open-source code

The high cost of proving that software works correctly has long kept formal verification out of reach for most developers, typically reserving the technique for critical systems like aircraft avionics. Now, Anthropic claims its Claude model has bridged that gap. By using AI to generate mathematical proofs of existing code, the company suggests a path toward making AI-generated software significantly easier to trust for everyday users.

Traditionally, this level of rigor requires immense human effort. Specialists spent 20 person-years verifying the seL4 operating system kernel, a small piece of software. To reduce this burden, Anthropic’s Frontier Red Team partnered with Theorem to assign the task to Claude. In just a few weeks, the model produced approximately 180 million lines of proof code. It analyzed test programs from 123 open-source libraries within Google’s OSS-Fuzz security project, focusing on verifying existing code rather than writing new applications.

The process involved converting crash tests into mathematical problems and analyzing compiled machine code. Claude constructed these proofs, which were then checked automatically by a separate program called Rocq. The researchers describe the generation as fully autonomous, although they note that the underlying tools and formal foundations were built by human experts at Theorem. This automation allows the system to operate with minimal human review.

During the verification process, Claude detected hundreds of bugs and was authorized to fix them. Many of these errors likely would have escaped conventional testing because they only appear under narrow conditions, such as unusually large input files or specific access sequences. In one notable instance, the team found as many security bugs in a single week on a widely used PDF reader as are typically reported in a full year. In another case, the system identified a logical error that had remained unnoticed for over a decade.

Despite these successes, Anthropic emphasizes that formal verification does not mean the software is error-free. The proofs are valid 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, meaning the guarantees have limits.

Cost remains a significant constraint, as individual proofs consume hundreds of millions of tokens, and total project costs have not been published. However, the company argues that if AI can verify its own code, developers can trust it more and spend less time on manual review. A smaller test run showed that proofs can be reused, with Opus 5.5 solving half the proofs using about 40 percent fewer tokens than Opus 5.

The project shifts the focus from whether AI can program to whether it can prove its code is safe. Anthropic expects this method to become as practical as standard testing. Theorem’s roadmap already targets critical infrastructure libraries, including glibc, OpenSSL, and cURL, aiming to extend these verification capabilities to essential software components.