October 23, 2026 — Anthropic’s Frontier Red Team, working with the startup Theorem, used Claude to mathematically prove that 239 test entry points across 123 open-source libraries will not crash — producing roughly 180 million lines of machine-checked proof in a few weeks, and uncovering hundreds of bugs along the way. Why it matters: formal verification has historically been so expensive that it was reserved for things like aircraft software. If an AI can do it at scale, “the AI wrote it” stops being the end of the safety conversation.
What did Claude actually prove?
The team took existing crash tests from Google’s OSS-Fuzz security project — programs that feed libraries hostile inputs to see if they break — and converted them into formal specifications. Claude then analyzed the compiled machine code at the RISC-V assembly level and produced proofs that, under the stated conditions, each program exits cleanly with no memory-safety violations or assertion failures for any input up to 64 MB. The proofs, written in the Rocq proof assistant, total about 180 million lines and are checked automatically by the Rocq kernel, which Anthropic says means the process needs almost no human reviewers. The researchers call it “fully autonomous” proof generation, while noting that the tools and formal foundations underneath were built by humans at Theorem.
How does this compare with how verification used to work?
Slowly, and at great expense. The small seL4 operating-system kernel — one of the most famous formally verified systems — took a specialist team about 20 person-years to verify, which is why the method has mostly been reserved for extreme cases such as Airbus avionics software. Anthropic’s run covered 123 real-world libraries in a few weeks. That is the step-change: not a better proof for one showcase system, but proofs across a broad slice of the open-source code that production software actually depends on.
What bugs did it find?
Hundreds, according to the researchers — and the interesting part is why ordinary testing missed them. Many of the bugs only appear under very specific conditions, such as unusually large input files or a particular sequence of accesses, so years of fuzzing never triggered them. While verifying a widely used PDF reader, the team found as many security bugs in one week as are typically reported for that software in an entire year. In another application, Claude caught a logical error that had gone undetected for more than a decade. Claude was allowed to fix the bugs it hit and then prove the fixes. Anthropic also notes that even when a complete proof ultimately fails, the attempt still tends to surface real bugs — the proof work doubles as an unusually deep audit.
What are the limits?
They are strict, and Anthropic states them plainly. “Formally verified” does not mean bug-free: the proofs hold only for single-threaded programs, on a specific processor architecture (RISC-V), running against the musl C library, with inputs under 64 MB. In practice, these libraries run on different hardware and in different configurations, where the proofs do not directly apply. The compute cost is also steep — individual proofs run into hundreds of millions of tokens, and Anthropic does not report the total cost of the project. There are signs the economics are improving: in a smaller benchmark, Opus 5.5 proved half of 36 tasks using about 40% fewer tokens than Opus 5, and Anthropic says proofs are reusable. Theorem’s roadmap already targets critical infrastructure code such as glibc, OpenSSL and cURL.
Why it matters
The standard objection to AI-written code is that nobody can check it all. This research points at the other side of that trade: the same class of model that writes code quickly can also check it with a rigor no human review team could afford — provided the checking happens inside narrow, honestly stated conditions. For readers of Tested Intelligence, the takeaway is to treat “formally verified” claims the way you would treat any benchmark: ask what exactly was proved, under which assumptions, and what sits outside them. Within those lines, though, this is one of the most concrete defensive wins AI has produced for open-source security — hundreds of real bugs, including one that hid for over a decade, found not by testing harder but by proving.
Frequently asked questions
Does “formally verified” mean these libraries have no bugs?
No. The proofs cover specific properties — clean exits with no memory-safety violations — under narrow conditions: single-threaded RISC-V binaries with inputs under 64 MB. Bugs outside that scope can and do remain.
Which libraries were verified?
Anthropic tested 239 entry points across 123 open-source libraries drawn from Google’s OSS-Fuzz project. The report highlights a widely used PDF reader as an example but the headline figure is the breadth across the OSS-Fuzz set.
Who checked the proofs?
The Rocq proof assistant’s kernel checks them automatically. Anthropic describes the generation as fully autonomous, with almost no human reviewers, while the underlying tools and foundations were built by its partner, Theorem.
How much did it cost?
Anthropic does not disclose a total. It says individual proofs can consume hundreds of millions of tokens, though newer models are getting more efficient — Opus 5.5 used about 40% fewer tokens than Opus 5 on a 36-task benchmark.
Sources: Anthropic Frontier Red Team and Theorem (research report, October 22, 2026), The Decoder
Related reading