What they did
Anthropic's Frontier Red Team worked with the verification company Theorem to see whether Claude could do formal verification, a job that normally takes specialists years per project. Instead of writing new code, Claude took existing C libraries from Google's OSS-Fuzz project, 123 of them, and turned their crash tests into mathematical statements about the compiled machine code. It then wrote the proofs that the code meets them. A separate checker, the Rocq proof assistant, accepted or rejected every proof, so almost no human review was needed. When a proof failed because the code was actually wrong, Claude was allowed to fix the bug itself. Theorem's people built the tooling and the formal groundwork the agent ran on.
How it went
Over a few weeks Claude produced roughly 180 million lines of proof code. It ran into hundreds of bugs, many of which only appear with unusual inputs such as very large files or a particular order of calls. On one widely used PDF reader the team found as many security bugs in a week as are usually reported for it in a year, and in another program Claude found a logic error that had gone unnoticed for over ten years. Even proofs that never completed still turned up real bugs. A smaller run found Opus 5.5 solved half the proofs with about 40 percent fewer tokens than Opus 5.
Worth knowing
The proofs only hold for one processor architecture, single-threaded code and inputs under 64 MB, so verified does not mean bug-free in real deployments. Individual proofs used hundreds of millions of tokens and no total cost was published. The account is a press write-up of Anthropic's own report, and it does not say which harness ran Claude.