Old software code checked for hidden flaws using AI-generated proofs

Software that has run quietly inside popular programs for years is now being put through a new kind of check, one that searches for flaws under exacting conditions rather than waiting for something to break. Anthropic says it used its Claude model to build mathematical arguments showing that existing code behaves as intended, a job that has traditionally required armies of specialists. The company is also clear about where the guarantees stop: the proofs apply only to a specific processor architecture, single-threaded programs, and inputs under 64 MB, conditions that do not match how these libraries often run in the field.

Proving software correct by hand has always carried a steep price tag. Verifying seL4, a small operating system kernel, took 20 person-years of expert work, which is why the practice has mostly appeared in areas like Airbus avionics software where failure is not an option.

Anthropic's Frontier Red Team partnered with a company called Theorem to move the proof work onto Claude. Within weeks, the model turned crash tests from Google's OSS-Fuzz security project into 180 million lines of proof code covering 123 open-source libraries. Claude did not write new software. It analyzed compiled machine code and constructed arguments for why that code runs without error. A separate program called Rocq then checks those arguments automatically, and Anthropic says almost no human reviewers are needed.

The run turned up hundreds of bugs, and Claude was allowed to fix them. The researchers say many would likely have slipped past conventional testing because they surface only under narrow conditions, such as unusually large input files or a particular sequence of memory accesses. While working to verify a widely used PDF reader, the team found as many security bugs in one week as that software normally receives reported in a year. On another application, Claude located a logic error that had gone unnoticed for more than a decade. Anthropic notes that even when a complete proof does not go through, the attempt can still surface real defects.

Anthropic describes the proof generation as fully autonomous, while stating that the tools and formal foundations behind it were built by people at Theorem. Individual proofs consume hundreds of millions of tokens, and the company has not published a total project cost. A smaller test run did show that proofs can be reused, and Anthropic reports that its Opus 5.5 model solves half the proofs using about 40 percent fewer tokens than Opus 5.

Theorem's roadmap targets glibc, OpenSSL and cURL next.