Anthropic has just demonstrated the most consequential shift in how we guarantee software correctness: Claude can now write formal proofs of real production code at scale. In a collaboration with Theorem, the company proved security properties at the assembly level (RISC-V) for 100+ real-world open-source libraries — the first large-scale effort to apply AI-driven formal verification to production software at the machine-code level. The process also unearthed hundreds of real bugs that evaded OSS-Fuzz's trillions of test runs for years. This isn't a demo. It's a working pipeline with 180 million lines of machine-checkable proof, and it points at a future where "proven safe" stops being a buzzword and starts being a shipping artifact.
Why This Matters Now
The premise is uncomfortable: AI is getting very good at breaking software, faster than we're getting good at proving it's safe. The Linux kernel — arguably the most heavily tested software on Earth — recently had over 1,000 vulnerabilities disclosed. Frontier models are increasingly capable of chaining seemingly benign bugs into critical exploits. The standard defenses — fuzzing, code review, type checkers — are all *sampling* methods. They make bugs less likely but can't rule them out. As the exploit side of the equation gets automated, the gap between "tested hard" and "provably correct" becomes a security hole, not an academic curiosity.
Formal verification is the classical answer to that gap: translate code into a mathematical model, then prove it satisfies a set of security properties under all possible inputs. If the proof holds, the bug class is gone — not "unlikely," but impossible within the model. But formal verification has always been brutally expensive. The seL4 microkernel took 2 person-years to build and 20 person-years to verify. Airbus's verified avionics is a one-of-a-kind case. That cost structure means formal methods stayed locked inside the most safety-critical corner of software: flight control, some chip verification, cryptographic protocol proofs. For the rest of the software world — the 10 million open-source libraries your apps depend on — it was simply not a thing you did.
Anthropic and Theorem's work attacks that cost structure directly: let the model write the proofs, and let a machine check them. The human trust burden shrinks to a handful of components, and the rest is automated. The result is the headline: 123 OSS-Fuzz libraries, 239 fuzz entry points, proven crash-free on every input under 64 MB, with the proofs checked by an independent proof checker (Rocq), and the whole thing runnable at the compiled-binary level — no need to rewrite anything in a proof-friendly language.
The Mechanism: Turning Fuzz Tests Into Proofs
The key insight is not "let the AI write a formal spec from scratch." Writing a spec is the hard part of formal verification — what does it even mean for a web browser to be "correct"? Instead, they reuse the tests that already exist. Every OSS-Fuzz library ships with fuzz entry points: functions the developers wrote specifically to be fed random input, where a crash = a bug. That's already a spec, in executable form: "this entry point never crashes."
The pipeline encodes that rule as a formal theorem over the compiled RISC-V instructions — the actual machine code — using formal semantics of the RISC-V ISA and Linux process behavior. The theorem says: for any input under 64 MB, given any modeled Linux response and memory layout, this program will not crash (no memory-safety violation, no failed assertion). Claude then writes the proof in Rocq (the successor to Coq), and the Rocq proof checker independently verifies every logical step. If the proof doesn't type-check, it's wrong. There's no "the model thinks it's correct" — the checker is the arbiter, and it's a small, auditable program, not a 100-billion-parameter black box.
| Scale metric | Value |
|---|---|
| Libraries proven | 123 OSS-Fuzz projects |
| Fuzz entry points proven crash-free | 239 |
| Total proof code | ~180 million lines of Rocq |
| Typical proof size | ~600,000 lines |
| Typical binary being proved | median 18,000 RISC-V instructions |
| Input coverage | every input < 64 MB |
| Models used | Claude (Opus family), Theorem's RISC-V + Linux semantics |
The proof-to-code ratio is the number to internalize: ~33 lines of proof per instruction of binary. That's why this was infeasible before — no human team could ever write, let alone maintain, that volume of proof. It's also why the old "formal verification is a 20-person-year project" framing dies here: the volume of proof is no longer the bottleneck, because the thing producing it doesn't sleep and doesn't need to be reviewed line-by-line.
What a developer actually has to trust is a short list: (1) the formal models of RISC-V and Linux processes, (2) the exact theorem statements (i.e., what property was actually claimed), and (3) the Rocq proof checker itself. Everything else — 180 million lines of it — is machine-verified. Any remaining bug is either in those three trusted components or outside the scope of the proof. That's the same structure as all formal verification, but the trusted component count is now small enough to actually audit, and the coverage is large enough to matter. They've published the proofs, the RISC-V and Linux semantics, and a Claude skill so other teams can run the same pipeline on their own code.
The Bonus: Proofs That Find Bugs Fuzzers Miss
The proof attempt itself is a powerful bug-finding engine, even when the ultimate proof doesn't come. When Claude hit a crash it couldn't prove away, it was allowed to patch the bug, regenerate the spec against the patched code, and continue proving. In total, the process surfaced hundreds of real bugs across the 123 libraries — many of them the kind a fuzzer would statistically never find:
- A counter underflow in a decompressor leading to an out-of-bounds write — but only triggered by an input around 20 MB with one rare, specific layout. Fuzzers typically mutate inputs capped near 1 MB and follow coverage signals; a bug that needs a precisely-shaped 20 MB input is almost invisible to that process.
- An out-of-bounds read in an image decoder that required a 64 MB input and over 2 GB of memory to trigger.
- An out-of-bounds read that needed a specific sequence of calls across two file handles — a cross-call interaction, not a single-input crash.
- A rediscovery of CVE-2026-56132 in libexpat (the XML parser), which needed deeply nested input — demonstrating the method can find known vulnerabilities from first principles.
- Logic bugs that never crash at all — e.g., a file-restriction feature that isn't always enforced, found while proving memory safety. These are invisible to fuzzing by definition: fuzzing only sees crashes, not misbehavior.
This matters because it reframes what verification is. The value isn't only the end-state ("we proved it safe"); it's the search process. A proof obligation is a structured, exhaustive query into a program's behavior — every path, every input class, every interaction — which is exactly the space where latent bugs hide. Attempting the proof is already a better security audit than the trillion fuzz runs these libraries have accumulated, and you get the proof as a bonus if the code turns out to be sound.
Proofs of properties, not just "no crash"
Fuzz tests in real codebases often assert meaningful high-level properties, not just crash-freedom: compress-then-decompress roundtrips, idempotence, equivalence to a reference implementation. Proving the test never crashes is then equivalent to proving the property itself. The post's most striking example: to complete the proof for cpp-httplib, Claude had to rule out stack overflow from recursive tree destruction — which required proving, at the machine-code level, that libc++'s red-black tree rebalancing actually keeps tree depth logarithmically bounded. That's a non-trivial data-structure theorem about optimized production compiler output, proved over assembly. The old "formal methods only work on toy programs" objection just lost one more pillar.
Beyond Fuzz Tests: The Wider Experiments
The OSS-Fuzz result is the headline, but the post documents a family of related experiments, each showing a different shape of LLM-assisted verification:
- zlib's RFC, proved against the kernel — on x86. Claude wrote a formal spec of RFC 1950 (the zlib format) and proved that the zlib implementation in the Linux kernel correctly implements it — this time at the x86 binary level, using Claude-generated (and heavily tested) formal semantics of the x86 ISA. The same loop was repeated for half a dozen other widely used libraries. Two conclusions: these extremely well-tested codebases are already almost fully correct (they found only minor, unexploitable corner-case bugs, being filed upstream), and end-to-end correctness properties about real, existing codebases are now provable.
- A Rust Python interpreter, proved against CPython semantics. Claude built an interpreter for a large subset of Python in Rust and used Verus to prove it adheres to CPython's semantics as outlined in an academic paper. Empirical check: 1.7 million randomly generated Python programs, identical behavior to CPython in 99.95% of tests, with the rest as known corner cases. That's a proof doing what it does best — converting a 99.95% empirical confidence into a guarantee about the class of behaviors the spec covers.
- Rooting out a decade-old bug in a PDF reader. While verifying simple security properties in a widely used PDF reader, the team found as many security bugs in one week as are typically reported in a year — including a previously unknown logic bug latent for more than a decade. This is the "attempting the proof is the audit" point again, applied to a critical application rather than a library.
The Economics: Why the Cost Curve Bends Now
The obvious objection to all of this is cost: these proofs consume hundreds of millions of tokens. If that's the price, it's another "impressive but unaffordable" research result. The post makes the strongest case I've seen for why that price is falling for structural reasons, not just model-vendor reasons:
| Efficiency lever | Measured effect |
|---|---|
| Newer models — 36 real OSS-Fuzz verification tasks | Opus 5.5 finishes half of them with ~40% fewer tokens than Opus 5; share of proofs completed per token budget keeps rising per generation |
| Proof reuse — agents sharing a proof workspace | 17% fewer tokens than working alone; some agents that failed solo succeeded with the shared library |
| Structural overlap — libc init, ASan boilerplate | Most of a proof covers code every program shares; different libraries' proofs overlap heavily and can be copied-and-adapted |
| Package-level granularity — verify a dependency once | Dependencies follow a power law: proving a small set of shared libraries (glibc, OpenSSL, cURL) makes a huge swath of software verify-for-free |
These levers compound in a way that's worth sitting with. Model generations reduce the per-proof cost (40% this cycle, and the trend is a trained-in capability). Proof libraries amortize the cost across projects — the same dynamic that let Mathlib grow to ~300,000 theorems across 700+ contributors, with every new proof standing on prior work. And the dependency power law means the first verifications are also the highest-leverage: verify the 500 libraries everything links against, and a large fraction of software inherits a verifiable foundation. Anthropic's collaborator Theorem has a public roadmap for the entire Nix ecosystem — glibc, OpenSSL, cURL and the critical infrastructure on top of them. That's not a research roadmap; that's a supply-chain-security roadmap.
The Honest Limits
The team is unusually careful about what "verified" does and doesn't buy, and the post's Limitations section is the part of the piece to read twice. Three gaps, stated plainly:
- "Formally verified" ≠ "bug-free." The proof checker verifies that the code satisfies the spec. It cannot verify that the spec matches reality. When bugs do appear in "verified" code, it's because the spec or the machine model is wrong or incomplete. The silver lining: this localizes where to look. The trusted surface (RISC-V/Linux semantics, the theorem statements, Rocq) is small and auditable, and hardening it is a bounded problem — unlike auditing billions of lines of unverified code.
- The model is a RISC-V single-threaded, static, musl-linked binary — not how most people run the code. Most deployments run x86 or ARM, dynamically linked against glibc, multi-threaded. The x86-ISA semantics work (used for zlib) is a step toward closing that gap; matching real deployed systems fully is future work. In other words: the proofs are real, but the machine in the theorem is not yet the machine on your server.
- Entry points ≠ whole libraries. ASan doesn't catch every memory-safety bug; not every entry point was proven; and even full entry-point coverage wouldn't cover dead code or caller misuse. The spec for "how callers must use this library" is the missing layer — the public-API contract — which is exactly the layer that would take the method from "library is crash-free" to "system built on the library is safe."
What's not yet proven (the scope to keep in your head)
Every guarantee in this post carries the same qualifier: under the assumptions — single-threaded, static binary, fixed memory budget, RISC-V on Linux, input < 64 MB, modeled OS responses. That's a genuine, huge, and well-defined region of behavior — far beyond anything fuzzing can claim — but it is not "this program can never be misused in any possible way." Anyone marketing "formally verified" as a bug-free stamp is misreading this. The correct read: the class of bugs — memory corruption reachable through these entry points on this hardware — is eliminated by proof, and the residual risk is now concentrated in a small, nameable, auditable set of components.
What This Changes
Set the details aside and three structural shifts follow from a working, scalable, machine-checked proof pipeline:
1. Verification goes from "bolted on" to "built in" — and the bottleneck moves from people to models
For 40 years, formal methods were limited by the scarce skill set: proof engineers who cost like architects and move like scribes. The seL4 ratio (20× the build cost) is the number that kept this out of production. When the proof writers are models and the proof checkers are software, the marginal cost of a proof approaches the marginal cost of compute. That's the same dynamic that turned code review from an expert art into a CI step, except the output isn't an opinion — it's a theorem. The authors' prediction is that verification becomes "as practical as fuzzing is today" for almost all production software, and the reuse/power-law economics above make that a plausible trajectory rather than aspiration.
2. The trust model inverts: small trusted cores, verified everything else
Notice the shape of the system: a small, auditable proof checker + small machine semantics + explicit theorem statements at the bottom; 180M lines of machine-generated proof above them; and downstream, an arbitrary number of verified libraries that add nothing to the trusted base. That's the same architecture as cryptography (small trusted primitives, everything else is construction), and it's the only shape in which "verified" can mean something at scale. The strategic implication for security teams: the audit question changes from "is this 50-million-line codebase correct?" (unanswerable) to "are these five small components correct, and does the spec match our deployment?" (answerable).
3. Exploit-side AI and verify-side AI are the same race, and this is the verify-side's first serious move
Anthropic's own exploit-evals work showed frontier models chaining benign bugs into critical exploits; Mozilla's work showed LLMs hardening Firefox. This post closes the loop: if AI can find and chain exploits, the defense that scales against it is AI-scaled proof, not AI-scaled testing — because an attacker doesn't need to find every bug, only one reachable one, while a defender needs to rule out the class. Fuzzing is a race you can't win on asymmetric stakes; proof is the first defense method that changes the stakes. The 1,000+ Linux kernel CVEs are exactly the population this pipeline is built to reduce to zero, class by class.
The three takeaways
Bottom Line
Anthropic and Theorem have shown the most important engineering fact about formal methods since they were invented: the thing that made verification expensive was proof-writing, and proof-writing is exactly the kind of large, tedious, well-checked work that LLMs do well. The result is not "AI can do formal verification" (small demos existed before) but "formal verification of production software at the binary level is now a scale process" — 123 libraries, 239 entry points, 180 million lines of machine-checked proof, plus hundreds of real bugs that four decades of continuous fuzzing missed. The limitations are real and stated honestly: the machine in the proof isn't yet your machine, entry points aren't whole libraries, and "verified" never meant "bug-free" to begin with. But the trajectory is unmistakable — per-proof costs falling ~40% per model generation, proof libraries amortizing across the dependency graph, and a power law that makes the first verifications the most valuable. In a world where AI attackers find one reachable bug and walk away, the first defense that can say "this class of bug does not exist in this code, and here is the machine-checked proof" is not a nice-to-have. It's the endpoint of the entire security tooling stack, and as of this month, it exists.
References
- Lucas, Lynch, Tong, Champine, Straznickas, Distefano, Agrawal, Ben Asher, Howell, Jawhar, Rohlf, Zeldovich, Carlini, R. Agrawal, Gross — "LLMs are making formal software verification feasible at a much larger scale," Anthropic Research [anthropic.com]
- Theorem — OSS-Fuzz proof repository (Claude's published Rocq proofs) [GitHub]
- Theorem — RISC-V & Linux process semantics [GitHub]
- Theorem — OSS-Verify service & Claude skill for verifying your own code [GitHub]
- Theorem — Roadmap for a verified software stack (Nix ecosystem, glibc, OpenSSL, cURL) [theorem.dev]
- Expert review of the Claude-written proofs (PDF) [PDF]
- Anthropic Research — Exploit Evals (bug-chaining into critical exploits) [anthropic.com]
- seL4 — 20 person-years of formal verification of the seL4 microkernel [PDF]
- Rocq Proof Checker [rocq-prover.org]
- Verus — verification tool for Rust [verus-lang.github.io]
- Mathlib — ~300,000 theorems across 700+ contributors [leanprover-community]
- Google — OSS-Fuzz: continuous fuzzing for open source [GitHub]
- LWN — Linux kernel vulnerability disclosures (1,000+) [LWN]
Results, scope assumptions, and limitation statements verified against the Anthropic Research post and linked artifacts as of October 23, 2026. Proof coverage is limited to the stated assumptions (single-threaded static RISC-V binaries on Linux, inputs < 64 MB, modeled OS semantics); "formally verified" in this post means "the stated property is machine-checked under those assumptions," not "bug-free."