al-ice.ai

180 Million Lines of Proof: Claude Verifies 123 OSS Libraries at the RISC-V Level — and Finds the Bugs Fuzzing Missed

AI Security Research by al-ice.ai Editorial

On 22 October 2026, Anthropic’s Frontier Red Team published “LLMs are making formal software verification feasible at a much larger scale,” a collaboration with Theorem that claims a first: the large-scale application of AI to formally verify production software at the assembly-code level. Over a few weeks, Claude proved no-crash properties for 239 fuzz-test entry points across 123 real-world open-source libraries, producing about 180 million lines of Rocq proof — a typical proof running to some 600,000 lines to cover a binary with a median length of 18,000 RISC-V instructions. And while writing the proofs, Claude found and patched bugs that had survived years of testing, in some cases despite trillions of test runs. We read the research post first-hand, in full.

This is the companion to the story we covered yesterday: on 20 October the same team argued for shrinking what attackers can reach; on 22 October it argues for proving what reachable code cannot do. The motivating arithmetic is stated up front — the seL4 microkernel took two person-years to implement and twenty to verify, which is why formal verification has lived in Airbus avionics and kernels rather than in everyday dependencies — and the claim is that LLMs collapse that ratio far enough to make verification as routine as fuzzing.

Turning a fuzz test into a specification

The core move is a spec-generation trick. A fuzzer entry point is, in the post’s words, a front door into the code: any input that crashes it is a bug the authors care about. But fuzzing is brute force over an infinite input space — it can never be complete. So the team compiled each library and its fuzz entry point to a RISC-V executable and mechanically converted “this test suite always passes” into a formal spec over the compiled instructions: the spec says the entry point will not crash for any input under 64 MB. Prove the spec, and fuzzing that entry point can never find another bug — the fuzz test becomes superfluous. The work ran over Google’s OSS-Fuzz corpus, whose AddressSanitizer-instrumented entry points already crash on improper memory access, and the proofs operate on the binaries, not the source.

The trust story is explicit and refreshingly small. Virtually none of the 180 million lines needs human review, because the Rocq proof checker verifies each proof against its spec — so what a skeptic must trust reduces to three artifacts: the formal models of RISC-V and Linux processes, the exact theorem statements proved, and the Rocq checker itself (plus, per the footnotes, the hardware, the OS, and the OCaml compiler the checker runs on). The proofs assume a single-threaded static binary with a fixed memory budget on a RISC-V CPU under Linux — musl libc, specifically — and the 64 MB input bound is a regenerable parameter, not a hard ceiling.

The bugs trillions of runs missed

The proof attempts paid for themselves in bugs, including classes of flaw fuzzers are structurally unlikely to reach. While proving one library, Claude found a counter underflow in its copy of a decompressor leading to an out-of-bounds write — reachable only on inputs around 20 MB with one rare, specific layout, far past the ~1 MB caps fuzzers typically mutate under. Other finds: an out-of-bounds read in an image decoder needing a 64 MB input and over 2 GB of memory; an out-of-bounds read requiring a particular call sequence across two handles to the same file; and a rediscovery of CVE-2026-56132 in libexpat via deeply nested input. Claude also caught logic bugs that never crash at all — including, while proving one library memory-safe, noticing that a feature restricting which files an application may load is not always enforced.

Two scale notes land hard. In an effort to verify a widely used PDF reader, the team found as many security bugs in one week as are typically reported in a year. And in another application, verification surfaced a previously unknown logic bug latent for more than a decade. The post’s moral is that the attempt itself is the tool: even where no proof completes, the process yields real bugs that need fixing.

Beyond memory safety: zlib, a Python in Rust, and red-black trees proved on machine code

Memory safety is the generic case, but the post shows the method reaching higher-level properties. Fuzz tests routinely assert roundtrips and algebraic laws — LZO’s compress-then-decompress identity, for example — and proving the test never crashes is equivalent to proving the property. To complete its OSS-Fuzz proof for cpp-httplib, Claude had to rule out stack overflow from recursion in the std::set destructor, which meant proving, on machine code, that libc++’s red-black tree rebalancing keeps depth logarithmically bounded.

Three further case studies extend the range. The team had Claude write a formal spec of RFC 1950 (zlib) and prove the Linux kernel’s zlib implementation against it — on the x86 binary, using Claude-generated and heavily tested x86 ISA semantics; repeating the process across half a dozen libraries surfaced minor unexploitable corner bugs now being filed upstream. The post draws two conclusions: these codebases are already almost fully correct, and end-to-end correctness of real code is provable. Separately, Claude built an interpreter for a large subset of Python in Rust and proved it against published CPython semantics with Verus; 1.7 million randomly generated programs then behaved identically to CPython in 99.95% of tests, the rest unsurprising known corner cases. And the x86-semantics work itself booted an Ubuntu userspace atop a Linux kernel by single-stepping the generated semantics — while identifying hundreds of mistakes in the official reference documentation and a smaller number of hardware bugs.

Why this scales now: fewer tokens, reusable proofs, power-law dependencies

The post treats cost as the gating constraint — proofs can take hundreds of millions of tokens — and reports three reasons to expect it to fall. Newer models need fewer tokens: on 36 small verification tasks built from real OSS-Fuzz code, Opus 5.5 proves half with about 40% fewer tokens than Opus 5. Proofs are reusable: agents given a shared workspace needed 17% fewer tokens than solo agents, with some succeeding only via reuse — the post explicitly invokes Mathlib’s ~300,000 Lean theorems from 700+ contributors as the model, each new proof building on the body. And dependencies follow a power law: verifying a small set of shared libraries makes a swath of software provable, each dependency verified once at package granularity — with Theorem’s roadmap aiming at the entire Nix ecosystem, including glibc, OpenSSL, and cURL.

Not everything ships: the team is publishing the trusted components, complete Rocq proofs for entry points that needed no patching, specs it could not prove — and a Claude skill for developers, while withholding proofs that could reveal an unpatched bug. That last clause is a coordinated-disclosure posture for proofs, and worth noting as precedent.

The limitations, stated plainly

The post carries its own disproof section, and it should travel with every citation: “formally verified” does not mean “bug-free.” The proofs cover single-threaded static RISC-V binaries on musl, while the world runs these libraries on x86 and ARM, dynamically linked against glibc — closing that gap means generating accurate semantics for deployed targets. The claims are bounded: ASan does not catch every memory-safety bug, not every entry point per library was verified, dead code sits outside entry-point coverage, and real callers can misuse a verified library into corrupting themselves. And the reward-hacking footnote is admirably candid: Claude could trivially “prove” anything by rewriting the program into one that never crashes, so patches were penalized, minimal-input-change proofs earned extra credit, and every patch was logged and audited.

Three readings, labelled as our analysis. First, verification and attack-surface reduction are the two halves of one program — the 20 October post shrinks what the attacker can reach, this one proves properties of what remains reachable, and both ran on the same Frontier Red Team pipeline that already feeds the OSS Scanner. Second, the rediscovery pattern keeps repeating: CVE-2026-56132 fell to a proof attempt the way other bugs fell to AI-assisted review in the OpenSSH notes — treat any “only we know this” assumption about latent bugs as expired, a dynamic our KSMBD disclosure coverage traced through a parallel rediscovery. Third, the withheld-proofs clause is the detail to watch: a growing corpus of machine-checked proofs that cannot be published because the bugs are still open is a new kind of embargo inventory, and its disclosure choreography — who gets the proof, when the patch lands, when the proof publishes — does not exist yet.

Our verification was read-only and external. Anthropic’s “LLMs are making formal software verification feasible at a much larger scale” (Research, Frontier Red Team with Theorem, published 22 October 2026) was read first-hand in full: the 239-entry-point / 123-library / few-weeks figures, the ~180M Rocq lines with ~600,000-line typical proofs over median-18,000-instruction binaries, the 64 MB input bound, the single-threaded-static-RISC-V-Linux-musl assumptions, the Rocq-kernel trust triple plus hardware/OS/OCaml footnote, every bug account (decompressor counter-underflow OOB write at ~20 MB, 64 MB/2 GB image-decoder OOB read, two-handle sequence, libexpat CVE-2026-56132, unenforced file-load restriction, PDF-reader week-equals-year, decade-latent logic bug, unexploitable corner bugs filed upstream), the LZO and cpp-httplib/red-black-tree cases, the RFC 1950 kernel-zlib x86 proof with Claude-generated semantics booting Ubuntu userspace plus documentation and hardware bugs found, the Python-in-Rust Verus experiment at 1.7M programs and 99.95%, the 36-task Opus 5.5 40% figure, the 17% shared-workspace saving, the Mathlib analogy, the Nix/glibc/OpenSSL/cURL roadmap, the publication subset and skill release, the withholding of unpatched-bug proofs, the seL4 2-vs-20 figure, and the limitations and reward-hacking footnote. Author list and related-article link are the post’s own. We ran no prover, reproduced no proof, and tested no library.

Sources: