Claude rediscovered CVE-2026-56132 proving 123 libraries crash-free

Anthropic, working with a verification company called Theorem, ran Claude against 239 fuzzing entry points across 123 open-source libraries from Google’s OSS-Fuzz and produced proofs that none of those entry points crash on any input under 64 MB. The proofs come to about 180 million lines of Rocq, roughly 600,000 per target, written over compiled binaries with a median length of 18,000 RISC-V instructions. Along the way Claude found bugs that trillions of fuzzing runs had missed, including a rediscovery of CVE-2026-56132 in libexpat.

Formal verification has been able to do this for decades. The reason almost nobody did it is cost. Verifying the seL4 microkernel took 20 person-years against the two it took to write, which kept the technique confined to code like Airbus avionics. Proofs run many times larger than the program, and writing them is a specialised skill. What is new is that a model wrote the proofs autonomously, at a scale that would have been absurd to attempt by hand.

The hard part of any proof is the spec: you cannot prove code correct until you state what correct means, and for most programs that statement is elusive. The project avoided writing specs from scratch by reusing something developers already have. OSS-Fuzz instruments C and C++ with AddressSanitizer, so a fuzz run crashes whenever memory is accessed improperly. That gives a ready-made property: this entry point never crashes for any input under 64 MB. Stated over the RISC-V instructions the compiler emits and then proved, it makes fuzzing that entry point pointless, because no input will ever find a bug there again.

Attempting the proofs surfaced bugs a fuzzer would be unlikely to reach. Fuzzers mutate small inputs, usually capped around 1 MB, steered by coverage. While proving one library Claude found a counter underflow in its bundled decompressor that caused an out-of-bounds write, but only on inputs around 20 MB with one rare layout. Another bug needed a 64 MB input and over 2 GB of memory; another needed a particular sequence of calls across two handles to the same file. The libexpat rediscovery needed deeply nested input. Claude also found a logic bug that never crashes at all: a feature meant to restrict which files an application can load was not always enforced.

If you run this kind of software, the useful shift is in what you have to trust. The Rocq checker confirms that each proof satisfies its spec, so almost none of those 180 million lines need human review. What a developer has to trust collapses to three things: the formal models of RISC-V and the Linux process, the exact theorem statements that were proved, and the Rocq checker itself. Hardening those is real work, but it does not grow as you verify more code. The same trusted base covers one library or a thousand.

That is also where the limits sit. A verified program is not a bug-free program. The checker confirms the code matches the spec; it cannot confirm the spec matches the machine. These proofs assume a single-threaded static binary with a fixed memory budget, linked against musl libc, running on RISC-V under Linux. Most of this code runs in production on x86 or ARM, dynamically linked against glibc. ASan misses some memory-safety bugs, and proving every entry point in a library still leaves dead code and callers that misuse the API uncovered. When verified code does crash, the model and the real machine disagreed somewhere, which at least narrows the search.

Cost is the other limit. A single proof can run to hundreds of millions of tokens. Two forces cut against that. Newer models need fewer: Opus 5.5 cleared half of a 36-task benchmark with about 40% fewer tokens than Opus 5. And proofs compose. Most of any proof covers code every program carries, such as C runtime initialisation and ASan setup, so agents sharing a workspace and copying each other’s finished proofs needed 17% fewer tokens, with some succeeding after failing on their own. The same reuse grew Lean’s Mathlib to roughly 300,000 theorems from over 700 contributors. At package granularity a dependency only needs verifying once, and dependencies follow a power law, so proving a handful of shared libraries makes a large fraction of everything downstream tractable. Theorem’s stated target is the whole Nix ecosystem, starting with glibc, OpenSSL and cURL.

The fuzz-test method is one of several the team tried. Claude wrote a formal spec of RFC 1950 and proved the Linux kernel’s zlib implementation meets it, this time against the x86 binary. It built a Python interpreter in Rust, proved with Verus that it follows CPython’s documented semantics, then ran 1.7 million random programs and matched CPython on 99.95% of them. Formal verification attempts on several widely used, critical applications surfaced real issues, one of them a previously unknown logic bug that had sat latent for more than a decade. A separate effort verifying a widely used PDF reader turned up as many security bugs in a week as that reader normally sees reported in a year.

Theorem is publishing a Claude skill for developers to verify their own code and offering to run the pipeline on other open-source projects, and the trusted components, the semantics and a subset of the proofs are released for independent checking. Anthropic’s specific pitch is to the people who tried formal verification on weaker models, watched it fail, and wrote it off.

---

Contains a referral link.