Anthropic published a research note on 23 October with the formal-methods firm Theorem. Claude produced proofs for 239 fuzz-test entry points across 123 open-source libraries, establishing that the compiled RISC-V binaries always exit normally, with no memory-safety errors and no failed assertions, for every input below 64 MB. Read carelessly, that sounds like 123 libraries are now proven secure. It is not that. The useful question is what the proof chain substitutes for, and where those substitutions leave room.
Formal verification has never been bottlenecked by the proof checker; it is bottlenecked by the specification. To prove a program correct you first have to say what correct means, and for most software nobody can. The project’s move is to manufacture a spec out of something developers already wrote, the fuzz-test entry point. The library and its existing fuzz test are compiled to RISC-V, instrumented with AddressSanitizer so that improper memory access registers as a crash, and the property is defined as the statement that this test never crashes on any input under 64 MB. Proving that over the compiled instructions is equivalent to proving the test can never fail again, and by construction equivalent to whatever higher-level property the test asserts. A test that checks LZO round-tripping yields a proof of round-tripping; a test that checks only for crashes yields only that.
The artifacts are enormous and almost entirely unreviewed. The 239 proofs total roughly 180 million lines of Rocq, with a typical proof around 600,000 lines covering binaries whose median length is 18,000 RISC-V instructions, a proof-to-code ratio in the tens. The claim rests on a small trusted base instead: Theorem’s models of the RISC-V instruction set and of Linux process behaviour, the exact theorem statements, and the Rocq kernel that checks them, plus the hardware, operating system and OCaml compiler the checker runs on. That is the right shape for this kind of work, a checker trusted once rather than proofs trusted many times, but it relocates risk rather than removing it. A bug in the semantics model would be invisible to every downstream proof.
The bug haul is the most falsifiable part of the report. While attempting proofs, Claude found a counter underflow in one library’s bundled decompressor that becomes an out-of-bounds write only on inputs around 20 MB with one rare internal layout; an out-of-bounds read in an image decoder that needs a 64 MB input and more than 2 GB of memory; a rediscovery of CVE-2026-56132 in libexpat through deeply nested input; and logic bugs that never crash at all, including a file-access restriction feature that is not always enforced. The pattern is the shape of fuzzing’s blind spots: large inputs, state accumulated across calls, pathological nesting, and errors that produce wrong behaviour rather than a signal. Note the last case. The proof was about crash-freedom, and the valuable finding was a behaviour the spec never mentioned. One obligation also went further than intended: to close the cpp-httplib proof, Claude had to show at machine-code level that libc++ red-black tree rebalancing keeps depth logarithmically bounded, because a stack overflow in the std::set destructor had to be ruled out.
Cost is the binding constraint, and the report is candid that proofs can consume hundreds of millions of tokens. The efficiency evidence is a 36-task benchmark: each task got three independent single-agent attempts at a 5-million-token budget, counted as proven if any attempt finished. Anthropic reports that Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5. That is a vendor-run measurement on a small, self-selected task set, so the direction is plausible and the magnitude should be read as indicative.
More interesting is reuse. Proofs, like code, are built from smaller proofs. Given a shared workspace where agents could copy each other’s work, the 36-task run needed 17% fewer tokens and 30 of the 34 completed proofs got cheaper; some tasks that had failed solo succeeded. At OSS-Fuzz scale the effect was structural: much of any proof concerns code every program contains, notably C runtime initialisation and AddressSanitizer setup, so unrelated programs ended up with heavily overlapping proofs and later teams adapted earlier work. This is the Mathlib mechanism applied to binaries, and its consequence is that verification cost can be amortised per dependency rather than per application, which matters because dependencies follow a power law. The caveat is that the dividend is largest where programs are most alike; as coverage moves into program-specific logic, the overlap shrinks.
Reproducibility is partial by design. The release includes a subset of the proofs, the RISC-V and Linux semantics, and specifications for entry points the system could not prove. Proofs that might expose an unpatched bug upstream are withheld. An outside reviewer can re-check the successes and audit the semantics, but cannot examine the strongest evidence, the bugs, until fixes land upstream. Theorem is publishing a Claude skill and offering to run the pipeline for other projects, the practical path to third-party replication.
The methodological hazard is acknowledged in a footnote. Because the pipeline patches code and then proves the patched code, an agent could make any theorem provable by rewriting the program into one that trivially cannot crash. The mitigations are penalties for patching, extra credit for characterising which inputs a patch changes and how few they are, and auditing of patches. That is sensible, but it shifts the weight of the claim onto review of patch diffs: a proof that code is crash-free says nothing about whether the code still does its job. For any prove-and-patch loop, the diff is the artifact that needs review, not the proof.
What the result does not establish is stated plainly. The proofs cover single-threaded, statically linked RISC-V binaries against musl, while most deployments are x86 or ARM binaries dynamically linked against glibc; closing that gap needs models that resemble real deployments. AddressSanitizer does not detect every memory-safety bug. Not every entry point was verified, and verifying all of them would still not cover dead code or a caller that misuses the API. The 64 MB input bound is a parameter that can be raised trivially; the single-threaded assumption cannot.
Three side experiments are worth flagging. Claude wrote a formal specification of RFC 1950 and proved the Linux kernel’s zlib implementation against it at the x86 binary level, using semantics Claude generated itself, and that generation reportedly surfaced hundreds of errors in official instruction-set documentation plus a few hardware bugs. A Python interpreter written in Rust and verified with Verus matched CPython on 99.95% of 1.7 million randomly generated programs.
Our take: the load-bearing result is not the library count. It is that proof-writing has become cheap enough, and proofs reusable enough, that verifying a shared dependency once and inheriting the guarantee looks like an engineering plan rather than a research aspiration. The questions worth measuring next are narrower than token savings: whether the semantics models can be maintained and trusted by more than one organisation, whether patch rewriting can be kept from hollowing out the property being proved, and how much of what users care about survives the translation from test to spec.
Sources
Anthropic Research, LLMs are making formal software verification feasible at a much larger scale — https://www.anthropic.com/research/formal-verification
Theorem, the formal-methods collaborator; the RISC-V and Linux process semantics and a subset of the proofs were released with the paper.
Google OSS-Fuzz — https://github.com/google/oss-fuzz