Anthropic Says Claude Formally Verified 123 Open-Source Libraries at the Assembly Level

Anthropic's Frontier Red Team published research on October 22 saying Claude produced machine-checked proofs of security properties for 239 fuzz-test entry points across 123 open-source libraries. Anthropic did the work with Theorem, a formal-methods startup. The proofs target compiled RISC-V binaries, not source code. They show that each program exits normally without a memory-safety error or a failed assertion for every input under 64 MB and for every modeled Linux system-call response and memory layout, according to Unite.AI's account of the post.

The workflow ran in a loop. When a proof attempt failed, Claude found the bug behind the failure, patched it, and then proved the patched binary. Interesting Engineering reports that some of these flaws had gone undetected for years despite the targets having been through trillions of automated fuzzing runs. The output is large. The proofs come to about 180 million lines of Rocq, the proof assistant formerly called Coq. A typical proof runs about 600,000 lines and covers a binary with a median length of 18,000 RISC-V instructions. Anthropic says the full effort took a few weeks. It describes the project as, to its knowledge, the first large-scale use of AI to apply formal verification to production software at the assembly level. That claim of a first comes from Anthropic, and no independent party has checked it.

The method's strengths and its limits are both worth noting. A Rocq proof checks itself, so the kernel does not have to trust the model that wrote it. That is a stronger guarantee than a vendor-reported score on any agentic coding benchmark. The guarantee is limited by the specification and the environment model, however. The proofs cover a fixed property (normal exit, no memory errors, no failed assertions), an input bound, and a modeled operating system. They do not prove functional correctness, and they say nothing about behavior the model of Linux leaves out. The entry points are fuzzing harnesses, so the verified surface is the surface the harnesses already exercised. Reviewers outside Anthropic have not yet audited the trusted base, meaning the RISC-V semantics and the system-call model.

The result changes the economics of a technique the industry has largely been unable to afford. Before this, formal verification at the binary level was limited to small, expensive projects with expert teams, such as seL4 and CompCert. Anthropic's claim is that the binding constraint is now tokens and compute, not proof engineers.