Anthropic reports that Claude proved security properties for 239 fuzzing entry points across 123 open-source libraries, working on compiled RISC-V binaries rather than source-level models. That is a meaningful increase in proof-writing scale. It is also easy to compress into a dangerous label: formally verified.
The label hides the engineering decision. A proof closes a precisely stated claim about a particular representation under explicit premises and a particular model. Production may sit before or after an unverified transformation, or run with a different architecture, linker, caller, workload, or concurrency model. A security lead therefore needs a deployment proof-coverage contract before treating the proof as a release control.
Here, proof coverage means an assurance manifest for deploying a proved result. It is broader than the proof-coverage metrics used by hardware and formal-methods tools to detect vacuity or structural gaps.
The nine fields of a deployment proof-coverage contract
| Field | Question the release owner must answer | Anthropic OSS-Fuzz example |
|---|---|---|
| Subject and transformation boundary | Which exact representation, version, or hash is proved, and which transformations sit before or after it? | Static riscv64 binaries built with a pinned toolchain and musl |
| Theorem | What statement ID, quantifiers, observables, error taxonomy, safety property, liveness property, and behavior relation did the checker accept? | Agreement and error-freedom statements; the public release has no halts proof |
| Domain and completeness | Which entry points, call sequences, valid inputs, and reachable paths are quantified, and what denominator remains open? | Selected OSS-Fuzz harnesses and their reachable code; 138 of 20,164 public statements are proved |
| Premises | Which memory, initial-state, system-call failure, caller, concurrency, and external-interference conditions must hold? | Statement-specific memory budgets and refusal policies; a single thread and no outside process changing modeled files |
| Model fidelity | Which real systems does the model represent, what is unmodeled, and what evidence validates the model? | A pinned LPS revision for riscv64 Linux/QEMU, with documented incomplete and imprecise cases |
| Trusted computing base | Which kernel, axioms, semantics, importers, wrappers, compiler stages, hardware, or operating system must be correct? | Rocq kernel, allowed axioms, LPS, ELF snapshot tooling, checker wrapper, and execution stack |
| Evidence and provenance | Which proof hash, checker output, allowed-assumption report, CI result, independent reproduction, and check date exist? | Pinned checker image, binary SHA-256, build record, proof files, CI, and reproducible check command |
| Deployment delta | Which ISA, ABI, assembler, linker, libc, OS, configuration, caller, concurrency, and resource differences remain? | A bridge or compensating control is required for x86/ARM, glibc, dynamic linking, threads, callers, or a new build |
| Revalidation policy | Which change makes the evidence stale, who owns rechecking, and what old claim remains valid? | Artifact, theorem, model, premise, checker, or deployment changes trigger a new comparison |
This contract changes the acceptance question from “Is the library formally verified?” to “Which production risk can this exact proof close?”
What Anthropic and Theorem actually proved
The study turns existing OSS-Fuzz harnesses into specifications. A harness is an author-provided entry point where a crash represents a property violation the maintainer cares about. The target is compiled to a RISC-V executable. Claude produces Rocq proof code, and the Rocq kernel checks whether that proof inhabits the exact theorem generated for the binary.
Anthropic reports successful proofs after patching discovered bugs for 239 entry points in 123 libraries. The proofs total about 180 million lines of Rocq. A typical proof is about 600,000 lines for a binary with a median 18,000 RISC-V instructions. The scale comes from machine checking: humans do not review every proof line. They review the theorem, model, provenance, assumptions, and residual gaps.
The appendix states the core result more narrowly. For its research theorem, it considers inputs under 64 MiB and memory layouts on modeled RISC-V Linux: the relevant binaries do not encounter a fault, abort, or unmodeled behavior; the plain and sanitizer builds also agree on specified read and write events, exit behavior, and final file-system state. The public release expresses its formal statements over LPS-valid process inputs and statement-specific premises. Its agreement statements use memory budgets and system-call refusal policies that must be read from the exact theorem. The proof says nothing about performance, and agreement alone does not rule out silent nontermination unless a halting property is separately proved.
The public proof repository makes this boundary concrete. Its current release publishes a subset: 60 entry points in 25 libraries. At statement level, the release lists 20,164 statements and 138 proved statements; no published proof establishes a halts statement. It pins Rocq 9.2.0, a checker image digest, the Linux Process Semantics commit, compiler and sanitizer versions, upstream commits, binary hashes, and allowed axioms. It also says directly that the result concerns those binaries and reachable entry-point code, not the whole library or its source code.
That provenance is part of the security result. A proof without artifact identity is a detached certificate.
Coverage has three independent boundaries
Teams often discuss proof coverage as if it were one percentage. In this experiment it has at least three dimensions, none of which is interchangeable with a tool's structural proof-coverage score.
1. Specification coverage
The main property is no modeled crash, including faults, aborts, failed assertions, and sanitizer-detected errors. That can include useful high-level invariants when the fuzz harness deliberately aborts on an invariant violation. A compression round trip, for example, can become a theorem if the harness checks that decompression reproduces the original input.
It still does not imply functional correctness in general. AddressSanitizer misses some memory-safety failures. A program can return the wrong result, leak memory, violate authorization logic, or remain stuck without violating the proved no-crash theorem. The specification defines the ceiling of the conclusion.
2. Reachability coverage
A proof quantifies over paths reachable from a selected harness. It does not automatically cover every public function, every call sequence, dead code, or misuse by a caller. Anthropic explicitly notes that even proving all current fuzzing entry points would not establish whole-library correctness.
The repository's enrollment skill therefore asks maintainers to choose entry points, attacker-controlled inputs, input sizes, expected failures, allocation behavior, call sequences, and domain properties. It also requires coverage witnesses and mutants that demonstrate each property can actually fail. A vacuous harness produces a valid but weak theorem.
3. Deployment-equivalence coverage
The published proofs concern single-threaded static RISC-V binaries linked with musl under a formal Linux-process model. Most production systems instead use x86-64 or ARM, dynamic linking, glibc, multiple threads, different compiler flags, and larger application-level call graphs.
This gap is not a footnote. It is the difference between proof evidence and deployment evidence. A release owner can respond in three ways:
- ship the exact proved artifact in the modeled environment;
- prove or test an equivalence bridge from the proved artifact to the deployed one;
- preserve the proof as strong component evidence while keeping runtime tests, fuzzing, review, and monitoring for the uncovered boundary.
The first two can support a claim about deployment equivalence. Component evidence can still close a bounded production claim when its premises hold, but it cannot justify a whole-deployment or general-release claim.
The trusted base becomes the review surface
Formal verification compresses a large review problem into a smaller one. Anthropic identifies the theorem statements, RISC-V and Linux models, and Rocq proof checker as core trusted artifacts. The public repository adds the allowed axioms, ELF snapshot and file-reading tools, checker wrapper, pinned images, and hardware and operating-system stack on which the checker executes.
That trusted base is separate from an assumption register. Each premise needs an owner, a validation method, and a current state. The pinned LPS revision is explicitly best effort and incomplete. Its scope document lists unchecked assumptions and known precision gaps, including cases where a behavior-set equivalence can hold in LPS while failing on a supported real system. Model revision and model-to-reality evidence therefore belong beside the proof result.
This is still valuable. Reviewing a stable trusted base can be far more tractable than manually reviewing 180 million lines of generated proof or repeatedly fuzzing an unbounded input space. But the residual risk should be named, versioned, and owned.
A deployment record should therefore bind:
- upstream source commit and build recipe;
- compiler, linker, libc, sanitizer, and flags;
- proved representation identity, such as a binary SHA-256 or source/intermediate-language revision, plus the verified transformation boundary;
- theorem identifier, quantifiers, observables, error taxonomy, liveness status, input restrictions, memory premises, and system-call failure policy;
- model and checker commits or image digests;
- permitted axioms and unmodeled system behavior;
- entry-point and caller preconditions, plus external-interference assumptions;
- independent check result, allowed-assumption report, check date, and production-delta decision.
If any identity changes, the proof moves from current evidence to historical evidence until the bridge is re-established.
Patching inside the proof loop needs a second gate
Anthropic allowed Claude to patch bugs that blocked a proof, regenerate the specification, and continue. This produced real findings, including rare large-input memory errors and logic bugs. It also creates an optimization hazard: an agent could make a theorem easy to prove by deleting behavior or narrowing the program.
The study acknowledges this reward-hacking risk. It penalized patches, rewarded proofs of behavioral impact, and logged patches for audit. A production workflow should make the separation explicit:
| Gate | Evidence |
|---|---|
| Proof gate | The patched binary satisfies the stated theorem |
| Behavior-preservation gate | The patch changes only intended behavior, with diff review, regression tests, compatibility checks, and where practical an equivalence or change-classification proof |
Passing the proof gate cannot silently waive the behavior gate.
A release decision that preserves the evidence level
Use four outcomes instead of a binary verified or unverified label:
- Exact-match acceptance: the deployed subject, configuration, premises, model, theorem, checker, and trusted-base identities match the proof package, with no unresolved deployment delta.
- Bridged acceptance: independently reviewed evidence connects every material deployment delta to the proved subject and premises.
- Component evidence: the proof reduces risk for a bounded entry point, while uncovered architecture, caller, concurrency, or functional behavior stays under conventional controls.
- Research-only evidence: the theorem or model is informative, but artifact identity or independent reproduction is missing.
Anthropic's publication provides primary research, a technical appendix, formal semantics, and a reproducible subset of proof artifacts. That is stronger than a benchmark claim. It is still not the same evidence state as independently checking every proof and deploying the same binaries.
Frequently asked questions
Did Claude prove 123 libraries bug-free?
No. Anthropic reports proving specified no-crash properties for 239 entry points across 123 libraries under stated assumptions, after patching bugs found during the process. Remaining bugs can sit outside the entry points, theorem, model, sanitizers, callers, or trusted base.
Why prove compiled RISC-V binaries instead of source code?
Binary-level proof avoids a gap between a source model and the behavior of one compiled artifact. It also makes artifact identity essential: a proof about one riscv64 binary does not automatically transfer to another build or architecture.
Does a proof replace fuzzing?
Within a statement's premises, further fuzzing cannot discover a counterexample to the modeled error property that was proved. Fuzzing remains useful for timeouts, resource behavior, uncovered entry points, architectures, environments, callers, properties, and future builds. Proof attempts also used fuzz harnesses as the source of the specification.
What should a maintainer verify first?
Start with the proved representation and transformation boundary, theorem ID, quantifiers, entry point, valid input domain, memory and failure premises, liveness status, model scope, caller assumptions, trusted-base versions, and proof-check result. Then compare every field with the deployment.
Conclusion
LLMs change the economics of proof construction. They do not change the semantics of proof: a checker certifies a theorem about a modeled artifact, not a marketing adjective about an entire product.
The operational advance is to package each result as a deployment proof-coverage contract. When subject, theorem, domain, premises, model fidelity, trusted base, provenance, deployment delta, and revalidation policy are explicit, formal verification can become a reliable release control. When those fields are absent, formally verified remains an ambiguous label with a very strong result hidden inside it.
References
- Anthropic: LLMs are making formal software verification feasible at a much larger scale
- Anthropic technical appendix
- Theorem Labs: published OSS Verify proofs
- Theorem Labs: Linux Process Semantics for Rocq
- Theorem Labs: LPS scope, assumptions, and known gaps
- Theorem Labs: maintainer enrollment skill
- Google OSS-Fuzz
- seL4 verification assumptions
- CompCert manual: verified transformation boundary
- Related: A dual-loop verification protocol for mathematical agents
- Related: Turn AI vulnerability reports into a maintainer-controlled queue