🔍 Read the full analysis: How Claude’s Verification Work Relates To Fuzz Testing on ThorstenMeyerAI.com
Get audio and creator gear delivered free with Prime
- Fast, free delivery on millions of items
- Prime Video, Amazon Music and more included
- Member-only deals all year
TL;DR
Anthropic’s Frontier Red Team and Theorem say Claude generated Rocq proofs for 239 fuzz-test entry points in 123 open-source libraries. The proofs establish a defined no-crash property for specific compiled RISC-V programs under stated assumptions; the work also exposed bugs that fuzzing had missed. The results do not show that the libraries are bug-free across the versions and platforms people use.
Anthropic’s Frontier Red Team and collaborator Theorem reported on October 22 that Claude had produced machine-checked proofs for 239 entry points in 123 open-source libraries, establishing that specific compiled programs do not crash on inputs under 64 MB under the project’s stated assumptions. The effort also found bugs that years of fuzz testing had not uncovered, but its results apply to particular RISC-V builds and modeled conditions, not every version or platform in use.
The team used each library’s existing fuzz test as the basis for a formal specification. Fuzz tests normally feed a program many generated or mutated inputs and flag crashes; the researchers instead asked whether the compiled program could be proved not to crash for any input below 64 MB at the selected entry point. The property covered AddressSanitizer memory errors and failed assertions, within the system represented by their models.
According to Anthropic’s account, the libraries and tests were compiled as RISC-V executables and instrumented with AddressSanitizer. Claude generated proofs in Rocq, a proof assistant whose checker validates whether a proof follows from the specification. If proof work exposed a possible bug, Claude could patch the code, after which the specification was regenerated and the new program had to be proved.
The reported scale was substantial: about 180 million lines of Rocq proof across the effort, with a typical proof around 600,000 lines. Anthropic says the work took a few weeks and describes it, to its knowledge, as the first large-scale application of AI to formal verification of production software at the assembly-code level. The company says it is releasing unpatched proofs, certain trusted components and specifications for fuzz tests it could not prove.
Infographic 01 · From test to proof
Existing fuzz tests became specifications. Claude proved them.
Over a few weeks, Claude proved at the machine-code level that hundreds of real fuzz entry points can no longer crash, after patching the bugs it found.
The pipeline
From an existing test to a checked proof
- Compile. The library and its existing fuzz test become a RISC-V executable, instrumented with AddressSanitizer.
- Specify. Theorem’s RISC-V and Linux process semantics plus the no-crash property mechanically yield the specification.
- Prove. Claude writes the proof in Rocq. A failed attempt points at a possible bug; Claude patches it and proves the new spec.
- Check. The Rocq proof checker verifies the proof. Virtually none of the proof needs human review.
Fuzzing vs. proof
Same entry point, different guarantee
| Fuzzing | Proof | |
|---|---|---|
| Inputs | Fuzzing: Generated samples, typically capped at 1 MB | Proof: Every input under 64 MB |
| Paths | Fuzzing: Guided by code coverage, no guarantee | Proof: Every path reachable from the entry point |
| Result | Fuzzing: Bugs found so far | Proof: No crash left to find on the modelled system |
Typical proof: about 600,000 lines for a binary with a median length of 18,000 RISC-V instructions.
“If Claude can prove this spec, the fuzz test on RISC-V becomes superfluous.”Anthropic, 22 Oct 2026
Source: Anthropic, “LLMs are making formal software verification feasible at a much larger scale” (22 Oct 2026).
Powered by Thorsten Meyer AI
Where Proofs Add to Fuzzing
Fuzzing tests a large number of inputs, but it cannot by itself show that every possible path has been exercised. A proof of the stated property, if its assumptions and models hold, can cover all inputs within the defined scope. That makes the approach potentially useful for finding hard-to-reach failures and for checking specific safety properties more broadly than a finite set of test runs.
Anthropic says the process found hundreds of bugs. Examples in its report include an out-of-bounds write requiring an input of about 20 MB with a rare layout, and an image-decoder read error requiring a 64 MB input and more than 2 GB of memory. Another reported issue depended on a sequence of calls involving two handles to the same file. These examples illustrate why test coverage can miss particular input sizes or call sequences; they are the company’s account of the findings, not evidence that every such bug is exploitable.
The work also highlights a possible shift in the cost of formal verification. Traditional verification projects can require extensive human effort; Anthropic cites seL4 as taking two person-years to build and 20 person-years to verify. AI-generated proofs may reduce some of that labor, although the reported token demands and engineering effort remain significant constraints.
As an affiliate, we earn on qualifying purchases.
From Existing Tests to Rocq Proofs
The method starts from a narrow, existing test rather than attempting to define correctness for an entire software library. A fuzz-test entry point specifies how a library handles inputs, while the team’s formalization turns the test’s crash behavior into a property about a compiled program. This limits the claim: proving that a test entry point does not crash is not the same as proving that the complete library behaves correctly in every use.
The pipeline depends on formal models of RISC-V instructions and Linux processes, as well as the theorem statements and Rocq’s proof checker. Anthropic says the proof checker verifies the generated work, so reviewers do not need to inspect all 180 million lines individually. The report also identifies hardware, the operating system and the OCaml compiler used by Rocq among components that ultimately form part of the trust basis.
Some of the reported findings go beyond ordinary memory-safety crashes. Anthropic describes a logic flaw in a feature intended to restrict which files an application could load. It also says a proof for cpp-httplib required ruling out a stack overflow caused by deep recursion in a destructor. The source material cuts off before describing that proof in full, so further details about that case are not available here.
“To its knowledge, this is the first large-scale use of AI to apply formal verification to production software at the assembly code level.”
— Anthropic, describing the study’s contribution
Limits of the Verified Builds
The no-crash result is limited to the specific programs and conditions modeled. The reported proofs concern single-threaded, static RISC-V binaries linked against musl. They do not establish the same property for the x86 or ARM builds linked against glibc that are more commonly used, nor do they prove that the libraries are free of all defects.
The result also depends on the accuracy of the formal models, the theorem statements and the trusted computing components identified by the researchers. The source account does not give a complete independent audit of those components, the total financial cost, or a detailed per-library record of which bugs were confirmed and fixed. It says proof runs can consume hundreds of millions of tokens, while newer models and shared proofs can reduce the burden; the practical cost across broader projects remains unclear.
A no-crash proof does not automatically rule out incorrect output, security weaknesses that do not trigger the modeled failure conditions, or problems in code paths outside the selected entry point. Some higher-level properties can be included when a fuzz test asserts them, but the scope still depends on what the test and specification encode.
Releases and Broader Testing
Anthropic says it is publishing proofs that did not require code patches, selected trusted components that were not already public, and specifications for fuzz tests it could not prove. Those materials may let other researchers inspect the assumptions and attempt to reproduce or extend the work.
The next practical test is whether the technique can be applied to more libraries, platforms and real-world build configurations without costs becoming prohibitive. The report points to newer models and reuse of proofs as ways to reduce token use, but it does not set out a schedule or announce a wider deployment plan. Independent examination of the released artifacts and the patched bugs will help clarify how much of the reported benefit carries over to software people run.
Key Questions
What did Claude prove?
According to Anthropic and Theorem, Claude generated Rocq proofs that 239 selected fuzz-test entry points in 123 libraries did not crash on inputs under 64 MB, for specific compiled programs and under stated assumptions. The proofs cover the defined property, not every possible software defect.
How is this different from fuzz testing?
Fuzzing runs a program on many generated inputs and checks for failures. A formal proof aims to establish the specified property for all inputs within its modeled scope, rather than only the inputs actually tried during testing.
Does this show the libraries are bug-free?
No. The results concern selected entry points, particular RISC-V binaries and a no-crash property under stated assumptions. They do not establish that all library versions, platforms or behaviors are free of bugs.
What bugs did the project report finding?
Anthropic says the work found hundreds, including memory errors requiring unusually large or specially structured inputs, a bug dependent on a particular sequence of file-handle calls, and a logic flaw involving file restrictions. These examples are reported by the project team.
What remains to be tested?
Researchers and developers can examine the released proofs and specifications, check the underlying models and trust assumptions, and test whether the approach works economically on other libraries and common x86 or ARM builds. The source report does not give a timeline for that wider work.
Source: ThorstenMeyerAI.com
Halloween Picks
halloween
As an affiliate, we earn on qualifying purchases.
