--- title: "Claude Wrote 180 Million Lines of Rocq to Verify 123 Libraries" pubDatetime: 2026-10-23T02:04:00.000Z description: "Anthropic and Theorem used Claude to produce assembly-level formal proofs for 239 fuzz-test entry points across 123 OSS-Fuzz libraries. The scale is real; what the proofs guarantee is narrower than the headline suggests." tags: [anthropic, ai-security, vulnerability, formal-verification, ai-agents, open-source, 2026, 2026-q4, 2026-10] --- > [!tldr] TL;DR > Anthropic's Frontier Red Team and the verification startup Theorem used Claude to produce machine-checked proofs at the RISC-V assembly level for 239 fuzz-test entry points across 123 open-source libraries from Google's OSS-Fuzz corpus, roughly 180 million lines of Rocq in total. Each proof shows that the sanitizer-instrumented and plain builds of a binary behave identically, and that the sanitizer never fires on any input up to a stated size cap such as 64 MB. Claude also surfaced bugs fuzzing had missed for years, though the one checkable example, a libexpat heap overflow, was already published as CVE-2026-56132 four months before. The proofs assume a single-threaded static binary with a fixed memory budget on RISC-V Linux, and the public proof repo covers 25 libraries rather than 123. Treat this as a jump in verification throughput, not a guarantee that 123 libraries are safe. The interesting choice in [Anthropic's formal verification write-up](https://www.anthropic.com/research/formal-verification) is where the proofs live. Claude did not verify C source code. It verified compiled RISC-V assembly, against a model of the instruction set and of Linux process semantics, which means the proofs hold for the binary you actually run. Compiler bugs and undefined-behaviour surprises sit inside the thing being proved rather than outside it. The individual numbers are the headline. A typical single proof runs around 600,000 lines of Rocq. Multiply across 239 entry points and you get roughly 180 million lines, written by an agent and checked by a proof assistant. Nobody was producing verification artifacts at that volume by hand. ## What the Proofs Say Each proof encodes two claims. First, that the sanitizer-instrumented build and the plain build of the same binary behave the same way. Second, that the sanitizer never fires on any input up to a size limit, 64 MB in the stated example. Together those cover the memory-safety and crash-freedom properties the sanitizer was watching for, over a bounded input space. The method starts from fuzz tests. OSS-Fuzz entry points already define an input and a harness, so Anthropic converted those harnesses into specifications and asked Claude to prove the sanitizer unreachable instead of hunting for an input that trips it. That reuse is what makes the scale possible: 123 libraries worth of specs that somebody else already wrote. Anthropic's own caveats bound the result tightly, and they are worth reading before the number sinks in. The proofs assume a single-threaded static binary with a fixed memory budget on RISC-V Linux. Verifying every fuzz-test entry point in a library still leaves most of the library unverified, since the entry points cover only the paths a fuzzer was pointed at. And "formally verified" describes the relationship between code and specification, nothing wider. ## The libexpat CVE Is a Rediscovery Claude found bugs along the way, which Anthropic frames as having eluded detection for years. One of them is checkable from outside: a heap-based buffer overflow in libexpat's `doProlog` in `xmlparse.c`. That is [CVE-2026-56132](https://nvd.nist.gov/vuln/detail/CVE-2026-56132), published on 19 June 2026, 126 days ago. Anthropic says Claude rediscovered it, and the post is straight about the word. Rediscovery is still a real signal. A proof attempt that fails at exactly the point where a human researcher independently found an overflow tells you the method has teeth, and it does so on a case where ground truth exists. It is a weaker claim than finding something new, and the other bugs Anthropic describes as previously unreported cannot be checked from here. ## Did Claude Prove the Right Thing? The gap between a proof and a guarantee is the specification, and Claude wrote the specifications too. Anthropic says this plainly. The sharpest version of the worry came up in the [Hacker News discussion](https://news.ycombinator.com/item?id=50202217): > [!quote] > "I found that even with LLMs making sure the formal specification covers what you actually want is challenging. How do you actually know what the LLM proved is what you want?" For this project the answer is better than usual, because the specs derive from existing OSS-Fuzz harnesses and sanitizer behaviour rather than from free-form prose about intent. Sanitizer-never-fires is a narrow, mechanical property. The spec-reality gap bites hardest when somebody extends this to functional correctness, where "what you actually want" stops being expressible as an assertion the compiler already inserted. A second caveat sits in Anthropic's appendix, which a commenter surfaced because the main post does not foreground it. The appendix says it remains to be seen whether agents can scale this verbose proof style to more complex programs, and points at other agent-based verification work, MachCSL, where agents hit a complexity wall and scaling up required proofs structured around modular abstractions. Six-hundred-thousand-line proofs of small fuzz harnesses may be the easy end of the curve. ## Who Verifies the Verifier Leonardo de Moura, writing in February, made a structural argument that lands on this project without naming it: > "If the same vendor provides both the AI and the verification, there is a conflict of interest. Independent verification is not a philosophical preference. It is a security architecture requirement." His [post on verifying AI-written software](https://leodemoura.github.io/blog/2026-2-28-when-ai-writes-the-worlds-software-who-verifies-it/) predates the announcement by eight months, so read it as applicable framing rather than a rebuttal. It applies anyway: Anthropic makes the model, partners with a verification startup, and together they generate the proofs and vouch for them. The mitigation is built into the technology. A Rocq proof is checkable by anyone with Rocq and the semantics model, with no trust in Claude or Theorem required. That is the point of machine-checked proof, and it makes this structure far more defensible than a vendor publishing its own benchmark scores. Which makes the inspectable surface the thing to watch. The public [oss-verify-proofs repo](https://github.com/theorem-labs/oss-verify-proofs) describes 60 entry points across 25 libraries and 2,148 theorem statements, of which 138 are proved and the remainder open or blocked. The headline claims 239 entry points across 123 libraries. The repo may be a partial release, an earlier snapshot, or a different unit of count; the reason for the gap is stated nowhere I can find. Until it closes, a fifth of the libraries are independently checkable and the rest stand on Anthropic's description. The [Linux process semantics model](https://github.com/theorem-labs/rocq-linux-process-semantics) is public too, which matters, since every proof in the set inherits whatever that model gets wrong. --- *Sources: [LLMs are making formal software verification feasible at a much larger scale](https://www.anthropic.com/research/formal-verification) • [theorem-labs/oss-verify-proofs](https://github.com/theorem-labs/oss-verify-proofs) • [theorem-labs/rocq-linux-process-semantics](https://github.com/theorem-labs/rocq-linux-process-semantics) • [CVE-2026-56132](https://nvd.nist.gov/vuln/detail/CVE-2026-56132)* *Coverage: [When AI Writes the World's Software, Who Verifies It?](https://leodemoura.github.io/blog/2026-2-28-when-ai-writes-the-worlds-software-who-verifies-it/) • [Hacker News discussion](https://news.ycombinator.com/item?id=50202217)* *Related on this blog: [[AUTO] Anthropic's automated vulnerability scanner reaches 85% accuracy. Can it scale?](/posts/auto-oss-scanner) • [[AUTO] Vulnerability discovery hits the patch ceiling](/posts/auto-vulnerability-patch-gap) • [[AUTO] AI's Predictable Hallucinations Become Supply-Chain Weapons](/posts/auto-hallucinated-packages)*