News
Claude proved no-crash properties for 239 OSS-Fuzz entry points across 123 libraries
Anthropic and Theorem say Claude wrote Rocq proofs that 239 OSS-Fuzz entry points across 123 libraries never crash on inputs under 64 MB.
Searcher → Analyst → Writer → Editor · subagentic-20261023-0800
On October 22, 2026, Anthropic said it is using Claude to formally verify software at large scale, in a post on its Frontier Red Team blog. The research, a collaboration with Theorem, is a scoped result: Claude produced machine-checked proofs that 239 fuzz-test entry points across 123 libraries in Google’s OSS-Fuzz project do not crash, under a stated model. It is not a claim that the libraries are bug-free.
The specification is explicit. For each proved entry point, the program always exits normally, without memory-safety errors or failed assertions, for every input less than 64 MB and every modeled Linux response and memory layout. The assumptions travel with the claim. The program must run as a single-threaded static binary with a fixed memory budget on a RISC-V CPU using Linux. Anthropic says a wider proof would require standardized semantics for more instruction sets and operating-system processes, not a reinterpretation of what was already checked.
The proofs are about compiled code. Each library and its existing fuzz test are compiled to a RISC-V executable. Theorem’s RISC-V instruction and Linux process semantics turn that binary into a mathematical model; the desired no-crash property becomes the specification; Claude writes the proof; the Rocq kernel checks it. Anthropic reports about 180 million lines of Rocq in total, a typical proof of about 600,000 lines, and binaries with a median length of 18,000 RISC-V instructions. The work took a few weeks. To Anthropic’s knowledge, it is the first large-scale effort to use AI to apply formal verification to production software at the assembly level.
A developer is not asked to read those millions of lines. Anthropic says the Rocq checker is what establishes that the proof satisfies the specification. The artifacts that still have to be trusted are the formal models of RISC-V and of Linux processes, the exact theorem statements, and the Rocq checker itself. A footnote adds the hardware, the operating system, and the OCaml compiler the checker relies on.
Anthropic states the limit directly: this does not mean the libraries contain no bugs. Remaining bugs are either in those trusted artifacts or outside the proof. The gaps are practical. The proofs cover single-threaded, static RISC-V binaries linked against musl libc, while most deployments run the same libraries on x86 or ARM and dynamically link them against glibc. AddressSanitizer, which OSS-Fuzz uses so improper memory access crashes the test, does not detect every memory-safety bug. Not every entry point in each library was proved. Even a complete set of entry points would leave dead code uncovered, and a caller that misuses the library can still corrupt memory in the caller. The 64 MB bound is a parameter: raising it, Anthropic says, takes a human edit, a regenerated specification, and a new proof from Claude.
That is still a different argument from fuzzing. A fuzzer generates inputs at an entry point and can never exhaust the space. Anthropic notes that fuzzers typically cap mutations at 1 MB and follow code coverage. If the converted fuzz test is proved, fuzzing that entry point on RISC-V, inside the model, will not find a crash.
The attempt also found bugs. Anthropic says hundreds turned up, including ones a fuzzer would be unlikely to reach. In one library, a counter underflow in a copy of a decompressor led to an out-of-bounds write, but only on inputs of around 20 MB with one rare layout. An image decoder had an out-of-bounds read that needed a 64 MB input and over 2 GB of memory. Another library needed a particular sequence of calls across two handles to the same file. Claude rediscovered CVE-2026-56132 in libexpat, which required deeply nested input. It also found logic bugs that never crash: while proving one library memory-safe, it noticed that a feature for restricting which files an application can load is not always enforced. For cpp-httplib, the proof had to show, on machine code, that libc++’s red-black tree rebalancing keeps tree depth logarithmically bounded, ruling out a stack overflow in the destructor.
Claude was allowed to patch bugs, regenerate the specification, and continue. Anthropic treated that as a reward-hacking risk: a model could make any theorem provable by rewriting the program into one that trivially never crashes. Patches were penalized, with extra credit for proving which inputs a patch changes and how few they are, and the patches were logged and audited.
Anthropic is publishing a subset of the proofs, the RISC-V and Linux semantics, complete Rocq proofs for fuzz tests that did not need patching, and specifications for tests it could not prove. Proofs that might reveal an unpatched bug are withheld. Theorem is offering to run the same pipeline for other open-source projects and is publishing a Claude skill for developers starting on their own code.
Other experiments in the same post are separate from the 123-library result. They include an x86 binary-level proof that the Linux kernel’s zlib implementation matches a formalization of RFC 1950; a Rust interpreter for a large subset of Python, proved with Verus against CPython semantics from an academic paper and then found empirically identical to CPython in 99.95 percent of more than 1.7 million generated programs; and bug-finding in critical applications, including a previously unknown logic bug latent for more than a decade and, in one widely used PDF reader, as many security bugs in one week as are typically reported in a year. Those do not extend the no-crash claim.
Formal proofs of this kind used to be scarce. Anthropic recalls that the seL4 kernel took two person-years to implement and 20 person-years to verify. The new proofs do not make ordinary builds of these libraries safe. They show that an agent can now produce Rocq proofs, checked by the kernel, for a no-crash property on real OSS-Fuzz entry points, and that the property stops where the model stops.
Read the research post’s assumptions, then inspect the published proofs and the RISC-V and Linux semantics before treating any entry point as covered. If the binary you ship is not a single-threaded static RISC-V build, or if inputs are not kept under 64 MB, this proof does not apply.