If a vendor or maintainer tells you a library is now "formally verified," your first question is which binary was proved. On October 22, Anthropic's Frontier Red Team and the verification company Theorem published machine-checked proofs that 239 fuzz-test entry points across 123 open-source libraries cannot crash on any input under 64 MB. The proofs cover single-threaded, statically linked RISC-V executables built against musl libc. Most of your fleet runs x86 or ARM with dynamically linked glibc, and Anthropic says so itself.
This quarter, use the proofs for dependency triage and sharper vendor questions, and run one pilot on code you own. Nothing on the proved list should move to "patched" in your risk register because of them.
What Anthropic and Theorem Actually Proved
Formal verification is a mathematical proof, checked by a program, that code meets a written specification for every input in scope. Here the specification came from the libraries' existing OSS-Fuzz harnesses: each fuzz test became a theorem that the program "will always exit normally without triggering memory-safety errors or failing assertions" for every input under 64 MB, every modeled Linux response and every memory layout.
The scale is the news. Anthropic reports that Claude produced about 180 million lines of proof in the Rocq proof assistant over "a few weeks," with a typical proof running about 600,000 lines for a binary with a median of 18,000 RISC-V instructions. The Rocq checker, a small and separately trusted program, verifies each proof against its statement, so nobody has to read 600,000 lines to trust the result.
Theorem's public repository is a subset. As of October 31, its README lists proofs for 61 entry points in 26 libraries, including zlib, zstd, bzip2, cJSON, OpenSSL, mbedtls, libpcap and simdjson. Across the wider OSS-Fuzz corpus it tracks 20,164 theorem statements: 336 proved, 5 known false, 229 blocked by the model and 19,594 still open. Anthropic says it withheld proofs that "may reveal an unpatched bug".
How Much of the Guarantee Reaches Your Builds
Very little of it reaches your production binaries directly. The repository README is blunt: the proofs are about compiled binaries, specifically static riscv64 builds made with clang 20.1.8 against musl, and not the x86-64 builds OSS-Fuzz itself runs. A different compiler, libc, architecture or linking mode is a different binary, and the theorem says nothing about it.
Anthropic lists the other boundaries in its own post. AddressSanitizer does not detect every memory-safety bug. Not every entry point was verified, and proving all of them would still leave dead code uncovered. A caller can misuse a proven library and corrupt its own memory. Logic bugs that do not crash fall outside a no-crash property entirely. The README adds that the theorems exclude wrong results and memory leaks, and that each proof assumes fixed memory budgets (2 GiB or 16 GiB, depending on the build).
The trusted base is also explicit: the formal models of RISC-V and Linux processes, the exact theorem statements and the Rocq checker, which in turn relies on the hardware, OS and OCaml compiler. Theorem calls its Linux process model "best effort and not complete."
There is one partial exception. In a separate case study Claude generated x86 semantics and proved the x86-compiled Linux kernel zlib binary against a specification of RFC 1950. Theorem's stated roadmap is the entire Nix ecosystem, including glibc, OpenSSL and cURL. Neither is in the released set today.
Why the 64 MB Bound Beats Another Year of Fuzzing
The proofs found bugs that fuzzing structurally could not reach. Fuzzers, Anthropic notes, mutate small inputs "typically capped at 1 MB" and never cover every path. A proof has to account for every input under the bound, so the bugs it surfaced cluster just past where fuzzers stop:
- A counter underflow in a decompressor that causes an out-of-bounds write, triggered only by inputs around 20 MB with one rare layout.
- An out-of-bounds read in an image decoder that needs a 64 MB input and over 2 GB of memory.
- A rediscovery of CVE-2026-56132 in libexpat, which requires deeply nested input.
Anthropic reports "hundreds of bugs" in total, a logic bug latent for more than a decade, and a PDF reader effort that found as many security bugs in one week "as are typically reported in a year."
Set that against what fuzzing has already done. Google says OSS-Fuzz had helped identify and fix over 10,000 vulnerabilities and 36,000 bugs across 1,000 projects as of August 2023. The libraries in this study are OSS-Fuzz projects, and the proofs still found bugs in them. Earlier this year we covered how AI bug-finding was outrunning patch capacity; proofs push the same pressure onto maintainers from the other side, by finding what fuzzing missed.
What It Costs Now, and What It Cost Last Time
The cost moved from person-decades to tokens, and no one has published a dollar figure yet. The last landmark in this field was the seL4 microkernel: 8,700 lines of C, 200,000 lines of Isabelle proof, and about 25 person-years for design, implementation and verification together. The seL4 project's own FAQ puts today's verified 64-bit RISC-V kernel at about 10,000 lines. Proof at that price was a choice made for one small, critical component.
Anthropic's only cost statement is that proofs "can take hundreds of millions of tokens to produce". On a 36-task benchmark, Claude Opus 5.5 proved half the tasks with about 40% fewer tokens than Opus 5, and agents sharing a proof workspace needed 17% fewer tokens than agents working alone. Both figures are Anthropic's own, from its own benchmark.
For open-source maintainers the price is zero. Theorem's OSS Verify program is free for qualifying projects. Core maintainers enroll by pull request, and established, widely used OSI-licensed projects on a security boundary (parsers, compression, crypto, decoders) get priority. Proofs can take multiple days. Theorem notes that findings and patches are AI-generated, with no promise of human review before they are sent. For closed-source code the page offers only "Not open source? Talk to us," with no published price. The enrollment repository also says Python and Go projects are paused, and that C projects whose static binaries carry under 1 MB of code get faster responses.
Where the Skeptics Have a Point
The strongest objection is maintenance. Fabio Akita, who walked through the results on October 24, argues that proofs break when code changes, so they fit slow-moving, high-stakes components better than fast-moving products. He also points out that using fuzz tests as the specification is an admission of how hard specifications are to write. A theorem is only as useful as the property it states, and "doesn't crash" says nothing about whether the output is right. Early coverage, including Interesting Engineering's report, quoted no outside experts, so practitioners like Akita are supplying the critique.
Reward hacking is the second concern. Anthropic concedes Claude could make any theorem provable by rewriting the program into one that trivially never crashes. Its controls were to penalise patches, give extra credit for proving how few inputs a patch changes, and log and audit every patch. An independent write-up on aicybr reports the patch audit as Anthropic's own account, and notes that the release does not show every upstream fix has shipped.
The third concern is scope. A proof about a parser does nothing about a poisoned release. The LiteLLM 1.107.0 backdoor and the npm worm that got past SLSA were supply-chain compromises, and no crash-freedom theorem would have caught either.
What to Do With It
Use the proofs to rank risk in your dependency tree, keep every existing control, and run one scoped pilot.
This Week:
- Match your SBOM against the proved list. Pull the index from the oss-verify-proofs repository, tag which of the 26 libraries you ship, and record the commit each proof covers, because a proof applies to that version only.
- Have AppSec write down the build gap: for each tagged library, the architecture, libc and linking mode you actually ship. Expect none to match static RISC-V on musl. Put that note next to the library in your risk register so nobody marks it "mitigated."
This Month:
- If your company employs or funds core maintainers of an OSI-licensed parser or decoder with an OSS-Fuzz harness, ask them to open the OSS Verify enrollment pull request. Only core maintainers can.
- Pick one internal pilot target: a C or C++ parser you own that already has a fuzz harness and under 1 MB of code. Ask Theorem for a quote and compare it with a year of your fuzzing and pentest findings on that component.
Before Your Next Vendor Security Review:
- Add one question to the questionnaire: "Which components carry machine-checked proofs, against what specification, for which architecture, libc and binary hash?" Accept an answer that names a hash and a target.
- Keep the fuzzers and sanitizers in CI. The proofs rely on the same ASan oracle and cover only reachable entry points. Where you already run AI code review such as Claude Security, keep it too; it looks for different bugs.
The Bottom Line
Until now, the reference price for formal verification was seL4: about 25 person-years for under 9,000 lines of C. Anthropic and Theorem proved properties of 239 entry points in weeks, each one checked by Rocq. The guarantee is narrow, tied to one architecture and one libc, and limited to "does not crash." Teams that have worked through the gap between trusting AI code scanning and having clean production code will recognise the pattern: a strong result on a defined target, and a long tail of builds it does not cover.
The C-to-Rust migration problem asked whether AI could rewrite unsafe C into Rust. This work proves properties of the C you already depend on, which is closer to what sits in your SBOM today. Until x86 and glibc proofs exist, leave your patch priorities where they are and use the proved list to decide which maintainers and vendors to question first.
Continue Reading
- Anthropic Glasswing: Why AI Found Bugs Humans Missed for Decades
- Anthropic's Claude Security Goes Public Beta
- LiteLLM's October 21 Compromise Puts Provider Keys at Risk
- vLLM 0.30.0 Can Run Code Through Ghostscript Images
- Canonical Funds a PhD Because C-to-Rust Translation Is Unsolved
- Cloudsmith $72M: AI Supply Chain Is a Board Problem
