Glonce

Claude writes formal no-crash proofs for 123 open-source libraries

researchThe Glonce editorsHacker News🔥89Glonce rating89Impact80Novelty80Relevance100Surprise65Players90Credibility85
Claude writes formal no-crash proofs for 123 open-source libraries

Anthropic, working with a collaborator called Theorem, says Claude can now write formal software proofs at a scale that used to be out of reach. The post's argument starts from a problem: AI makes bugs easy to find and exploit, so the standard defenses are no longer enough, and the authors want ways to prove code is free of bugs. Formal verification can give that guarantee, but it has historically needed years of expert effort. They cite the seL4 operating system kernel, which took two person-years to implement and 20 person-years to formally verify. As a result it has been practical mostly in mission-critical settings such as Airbus's avionics code.

The project turned existing fuzz tests into specifications. A fuzz test is an entry point into a library where any input that causes a crash counts as a bug; a fuzzer then throws huge numbers of semirandom and mutated inputs at it. The team converted such tests, taken from Google's OSS-Fuzz initiative, into a spec over the compiled RISC-V instructions: the fuzz test will not crash for any input less than 64 MB. If Claude can prove that, fuzzing that entry point on RISC-V becomes superfluous, because it can never find a bug. OSS-Fuzz instruments C and C++ programs with AddressSanitizer, so a crash includes improper memory access, a leading cause of software vulnerabilities.

Over a few weeks, Claude patched the bugs it found and then proved there are no crashes on any input up to 64 MB for 239 entry points across 123 OSS-Fuzz libraries. The proofs are written in Rocq and operate on executable binaries with a median length of 18,000 RISC-V instructions. Together they comprise about 180 million lines of Rocq, with a typical proof running to about 600,000 lines. They rest on Theorem's RISC-V instruction and Linux process semantics. Specifically, Claude proved the programs always exit normally without memory-safety errors or failing assertions, for every input under 64 MB and every modeled Linux response and memory layout. This holds only under assumptions: a single-threaded static binary with a fixed memory budget, on a RISC-V CPU, running Linux.

The authors say almost none of the proof code needs human review, because the Rocq proof checker confirms the proofs satisfy the spec. What a developer must trust is three things: the formal models of RISC-V and Linux processes, the exact theorem statements, and the Rocq checker. They stress that this does not mean the libraries are bug-free; remaining bugs would sit in those trusted components or outside the proof's scope. They also say this is still far from fixing all possible bugs.

The process of attempting the proofs uncovered hundreds of bugs. So that a human did not have to step in each time, Claude was allowed to fix what it found: it patched the code, the spec was regenerated from the patched code, and Claude then proved the new spec. The post says many of these bugs are ones a fuzzer would be unlikely to find, since fuzzers mutate small inputs, typically capped at 1 MB. Examples: a counter underflow in a library's copy of a decompressor that led to an out-of-bounds write, but only on inputs of around 20 MB with one rare layout; an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory; an out-of-bounds read in another library that needed a particular sequence of calls across two handles to the same file; and a rediscovery of CVE-2026-56132 in libexpat, which needed deeply nested input. Claude also found logic bugs that never crash. While proving one library memory-safe, it noticed that a feature restricting which files an application can load is not always enforced. The summary claims some of these bugs had eluded detection for years despite trillions of test runs.

Anthropic is publishing a subset of the proofs, the RISC-V and OS semantics, the trusted components not already public, Claude's complete proofs for fuzz tests that did not need patching, and specifications for fuzz tests it could not prove. Theorem offers to run the same pipeline on other open-source projects and is publishing a Claude skill to help developers verify their own code. The post also says it describes early work with other verification methods, on the zlib compression algorithm, on behavioral equivalence of a Python interpreter written in Rust, and on long-standing bugs in critical software. It closes the introduction by saying the cost of writing proofs is falling as models improve, and that proof reuse across codebases should amortize costs further.

Key facts

  • Claude proved, in Rocq and at the RISC-V assembly level, that 239 entry points across 123 OSS-Fuzz libraries do not crash on any input under 64 MB, under stated assumptions.
  • The proofs total about 180 million lines of Rocq, a typical one about 600,000 lines, covering binaries with a median of 18,000 RISC-V instructions.
  • Attempting the proofs surfaced hundreds of bugs, which Claude sometimes patched; examples include bugs needing a 20 MB input or a 64 MB input with over 2 GB of memory, and a rediscovery of CVE-2026-56132 in libexpat.
  • The result holds only for single-threaded static binaries with a fixed memory budget on a RISC-V CPU under Linux; the authors say it is not a claim that all bugs are fixed.
  • Anthropic is publishing a subset of the proofs and the trusted models; Theorem offers to run the pipeline for other open-source projects and is releasing a Claude skill.

Why it matters

The authors argue that AI makes bugs easy to find and exploit, so defenders need guarantees rather than more testing. They note the Linux kernel recently had over 1,000 vulnerabilities disclosed. Formal verification gives such a guarantee but has needed years of expert work; seL4 took 20 person-years to verify against two to implement. Here Claude did the proof work autonomously across 123 libraries in a few weeks. The authors say that, to their knowledge, this is the first large-scale effort to use AI to apply formal verification to production software at the assembly code level. They expect formal verification to become an essential part of secure software development as models improve.

Who it affects

Maintainers of C and C++ open-source libraries that already have fuzz tests, especially those in Google's OSS-Fuzz, are the direct audience, since the method starts from existing fuzz tests. Security teams who depend on those libraries are affected too. The post encourages all developers to explore formal verification with LLMs, in particular those who tried it with less capable models and found it did not work.

How to use it

Theorem offers to run the same pipeline for other open-source projects and is publishing a Claude skill to help developers start verifying their own code. Anthropic is releasing a subset of the proofs, the RISC-V and OS semantics, the trusted components not already public, complete proofs for fuzz tests that needed no patching, and specifications for fuzz tests it could not prove, so others can verify and reuse them. The method itself: turn an existing fuzz test into a spec over the compiled RISC-V binary, let Claude patch any bugs it hits, and have it prove the regenerated spec. The post gives no pricing or cost figures.

How solid is it

This is a first-party Anthropic post written with Theorem, giving concrete figures: 239 entry points, 123 libraries, about 180 million lines of Rocq. The proofs are checked by the Rocq proof checker, so the authors say virtually none of the proof code needs manual review. They welcome independent verification and publish materials to allow it. The headline claims are the authors' own, and the independent check they invite has not yet been described in the portion of the post covered here. The summary says 'over 100' libraries while the body gives 123.

Risks and caveats

The guarantee is narrow. It covers single-threaded static binaries with a fixed memory budget, on a RISC-V CPU under Linux, and inputs under 64 MB. It says the program exits normally without memory-safety errors or failing assertions; it does not mean the libraries have no bugs. Remaining bugs could lie in the trusted pieces (the RISC-V and Linux models, the theorem statements, or Rocq itself) or outside the proof's scope. The authors say this is still far from fixing all possible bugs. Extending to other architectures and operating systems is described as well within reach, not as done. Specifications for some fuzz tests could not be proved.

“Frontier models can now produce correctness proofs for real-world software fully autonomously.”

— Anthropic, research post on formal verification