Fuzzing never finishes. A proof that the fuzzer has nothing left to find is a different kind of claim.
On 22 October 2026, Anthropic's Frontier Red Team, working with Theorem, reported that Claude produced machine-checked no-crash proofs over compiled RISC-V for hundreds of real OSS-Fuzz entry points. The work sits one step past Anthropic's attack-surface reduction post: instead of shrinking reachable code, the team asks whether the remaining paths can be shown crash-free under an explicit model. The assumptions are narrow enough to read carefully and wide enough to matter for memory-unsafe C and C++ libraries that already ship AddressSanitizer fuzz targets.
Claude turns OSS-Fuzz harnesses into Rocq proofs over RISC-V binaries
Anthropic frames the novelty as scale at the assembly layer. Claude proved that selected programs always exit normally without memory-safety errors or failed assertions for every input under 64 MB and every modelled Linux response and memory layout, when the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU under Linux. The team counts 239 entry points across 123 OSS-Fuzz libraries, about 180 million lines of Rocq in total, and a typical proof near 600,000 lines against binaries with a median length of about 18,000 RISC-V instructions.
The method starts from developer-written fuzz harnesses rather than hand-authored high-level specs. The library and harness compile to RISC-V; Theorem's RISC-V and OS semantics plus the no-crash property mechanically yield a specification; Claude writes the proof; the Rocq kernel checks it. Anthropic says this is, to its knowledge, the first large-scale AI effort to apply formal verification to production software at the assembly-code level.
123 libraries, 239 entry points, and bugs found on the way to QED
Success is defined as a checked proof that the harness never crashes inside the stated bounds, after Claude patches any counterexample it hits while proving. Many of those bugs, Anthropic argues, sit outside ordinary fuzzer reach: a decompressor out-of-bounds write that needed roughly 20 MB inputs with a rare layout; an image-decoder read that needed a 64 MB input and more than 2 GB of memory; a rediscovery of CVE-2026-56132 in libexpat that needed deep nesting; and logic bugs that never crash at all, such as a file-load restriction that is not always enforced.
Proving "the test never crashes" also covers higher-level harness properties that fail by assertion: encode-decode round trips, idempotence, differential testing. In one cpp-httplib case, Claude had to prove on machine code that libc++ red-black tree rebalancing keeps destructor recursion logarithmic, or the no-crash proof could not close.
Trusted computing base shrinks to semantics, statements, and Rocq
Anthropic is explicit that the libraries are not proven bug-free in every sense. Remaining bugs must live in the trusted artifacts (RISC-V and Linux process models, the exact theorem statements, Rocq itself) or outside the proof's scope. That is a smaller audit surface than every line of every library, and it stays fixed as more projects reuse the same semantics.
Independent verification is invited: Anthropic is publishing trusted components that were not already public, complete Rocq proofs for fuzz tests that needed no patching, and specifications for harnesses it could not prove. Theorem offers to run the same pipeline on other open-source projects and is publishing a Claude skill for developers who want to start locally.
Multi-thread, dynamic linking, and non-RISC-V targets stay outside the claim
The proofs assume a single-threaded static binary, a fixed memory budget, RISC-V, and Linux. They do not cover concurrent execution, dynamically linked deployments, other ISAs in the main OSS-Fuzz corpus, or inputs larger than 64 MB. Expanding scope, Anthropic says, means standardising more architecture and OS semantics rather than rewriting each library.
Token cost is another limit. Proofs can consume hundreds of millions of tokens. Anthropic reports that on 36 small verification tasks, Opus 5.5 proved half with about 40% fewer tokens than Opus 5, and that agents sharing a proof workspace needed 17% fewer tokens than agents working alone. Those efficiency notes are Anthropic's internal measurements.
A subset of proofs, semantics, and a Theorem skill are on the table
The research post links the published subset of proofs and semantics and points readers to Theorem's collaboration notes and skill. Proofs that might reveal unpatched bugs are withheld. zlib-on-x86, a Rust Python interpreter checked with Verus against academic CPython semantics, and other case studies appear as related experiments rather than the main 123-library claim.
Treat no-crash RISC-V proofs as a new bar for critical fuzz targets
Security and library maintainers who already live in OSS-Fuzz should read the theorem statements before celebrating. Where a harness encodes a property you care about, a checked proof under these assumptions is stronger than another weekend of fuzzing on the same entry point. Platform teams should still ask whether their production binaries match the single-thread static RISC-V model. Procurement language that says "formally verified" needs the assumptions attached, or it overclaims.
Follow-on to Anthropic's attack-surface work, with Theorem on the proof stack
This post lands days after Anthropic's Frontier Red Team attack-surface reduction research. That earlier piece gated reachable code. This one tries to exhaust crash bugs on the remaining fuzz surface with machine-checked assembly proofs. Theorem supplies the RISC-V and Linux semantics and the collaboration path for other projects. seL4-style human proof effort remains the historical baseline Anthropic cites for why the cost curve had to change.