A guarantee with a checker attached

Most AI security announcements ask to be believed. This one asks to be checked. Anthropic and the startup Theorem turned existing fuzz tests from Google's OSS-Fuzz project into formal specifications: the test entry point will not crash on any input under 64 MB. Claude then wrote proofs of those specifications against the compiled RISC-V machine code, using Theorem's formal models of the RISC-V chip and of a Linux process. The Rocq proof checker verifies each proof mechanically. Over a few weeks, the team reports, Claude completed proofs for 239 entry points across 123 libraries, patching the bugs that blocked it as it went.

That structure is the substance of the announcement. A fuzzer can run for years and still miss an input. A proof, if its models are right, covers every input inside its stated bounds at once. Anthropic puts the volume at about 180 million lines of Rocq, with a typical proof near 600,000 lines for a binary of about 18,000 instructions; the appendix adds that Claude wrote about a billion lines in total, of which roughly 180 million passed the checker. Nobody is expected to read that. The point is that nobody has to: the checker does the reading, and the list of things a reader must trust shrinks to three items, the machine models, the theorem statements, and the checker itself. Anthropic's footnote on the checker adds the practical dependencies underneath it: the hardware and operating system the checker runs on, and the OCaml compiler Rocq itself is implemented in.

Where the guarantee stops

Anthropic's own limitations section is the most useful part of the post, and it deserves as much circulation as the headline number. The proved programs are single-threaded static RISC-V binaries linked against musl. Most production systems run these libraries on x86 or ARM, dynamically linked against glibc. The proved property covers crashes the AddressSanitizer setup would catch; Anthropic notes that ASan does not detect every memory-safety bug, that not every entry point in each library was verified, and that a caller misusing a library can still corrupt memory outside the proof's reach. The public proofs also do not establish that a program terminates: an execution that runs forever without an error does not violate the proved statements, as an independent analysis of the release documentation points out.

None of that makes the work small. It makes it specific. “Formally verified” in this post means a defined property, on a modelled machine, within a stated input bound. Readers who repeat the claim without the conditions are upgrading it into something Anthropic did not say, and Anthropic, to its credit, said the quiet part in its own text: this does not mean these libraries contain no bugs.

The bugs are the second result

The proof process doubled as a bug hunt, because a proof cannot be completed while a reachable crash remains. Anthropic says Claude found hundreds of bugs in code that had survived extensive fuzzing. The examples it names are the kind fuzzers are structurally poor at reaching: an out-of-bounds write that needs a roughly 20 MB input in one rare layout, while fuzzers typically work with inputs capped near 1 MB; an out-of-bounds read that needs a particular sequence of calls across two handles to the same file; a logic bug in which a file-access restriction feature is not always enforced, which never crashes at all.

Treat the count with care. “Hundreds” is Anthropic's word and the post gives no exact total, no per-library breakdown in the main text, and no independent audit in the sources available at publication. Bugs found during proving are not the same thing as an audited count of vulnerabilities, and the aggregate number is not yet checkable against public material.

Anthropic says Claude was allowed to patch crash-producing bugs and then prove the modified binary. That introduces a separate risk: a system could make a theorem easier to prove by changing the program's intended behaviour — a decoder that rejects every input would be easy to prove safe and useless in practice. The team says it discouraged that shortcut through patch penalties, incentives for minimal behavioural changes, and patch audits, logging the patches it made. The post does not establish that all fixes were independently reviewed or accepted upstream. So the proofs describe the binaries as patched inside this project, which is not necessarily the code a user downloads today.

The cost line decides who gets to use this

Anthropic cites the seL4 kernel, which required two person-years to implement and 20 person-years to verify, as an illustration of how labour-intensive formal verification can be. The new price is measured in tokens, and it is not trivial. The post states that a proof can take hundreds of millions of tokens to produce.

Its efficiency evidence is a set of 36 small tasks the team built itself from real OSS-Fuzz code. Each task received three independent attempts at a 5-million-token budget, and counted as proven when the first attempt finished. On that set, Opus 5.5 proved half the tasks with about 40% fewer tokens than Opus 5. A separate experiment gave agents a shared workspace in which they could copy each other's finished proofs, and measured 17% fewer tokens than agents working alone. Those are two separate experiments, not two parts of one saving.

That is a falling cost curve described by the seller, on the seller's own test set. It is directionally plausible and worth watching. The research suggests AI-assisted proof generation could substantially reduce the specialist effort required for some verification tasks, but its total cost and reproducibility outside the research team remain unmeasured publicly. It is not yet a price list an open-source maintainer can budget against. Theorem offering to run the pipeline for other projects, and publishing a Claude skill for developers, is the first test of whether this becomes a service with a knowable price or stays a demonstration run by the lab that built the model.

What to watch

Two things will settle what this announcement is worth. The first is independent use: whether teams outside Anthropic and Theorem can take the published proofs, semantics and skill, and verify a library Anthropic did not choose. The second is scope: whether the machine models move closer to the systems people actually run, x86 or ARM, dynamically linked, multithreaded, before the claims made about the work move first.

The same post describes two side experiments that are separate from the 239-entry-point result. In one, Claude proved that the zlib implementation in the Linux kernel correctly implements the RFC 1950 specification, at the x86 binary level, using Claude-generated formal semantics of the x86 instruction set; minor, unexploitable corner-case bugs found along the way are being filed upstream. In the other, Claude built an interpreter for a large subset of Python in Rust and proved, using the Verus verification tool, that it implements published CPython semantics, with identical behaviour to CPython in 99.95% of 1.7 million randomly generated test programs. Neither experiment carries the RISC-V no-crash guarantee, and neither should be quoted as part of it.

A related but distinct strand of Claude-assisted security research from the same week is [Anthropic's attack-surface reduction work](https://alfw.ai/article/claude-attack-surface-493-issues-openssh/), in which Claude mapped code reachable before authentication across 25 open-source projects and OpenSSH shipped a fix. That work finds exposure to reduce; this work proves a property to keep. They are different methods answering different questions, and nothing proved here carries over to the findings reported there.

Until the tests arrive, the accurate summary is a strong one, stated at its actual size. A frontier model produced machine-checked proofs about real, widely used code, at a scale formal verification has not previously operated at, and found real bugs in the process. The conditions are not fine print to be embarrassed by. They are the difference between a proof and a slogan.

Sources

  1. [1] Anthropic, “LLMs are making formal software verification feasible at a much larger scale” (Frontier Red Team, with Theorem), October 22, 2026 — primary source, read in full first-hand: the 239 entry points across 123 libraries, the under-64 MB bound, about 180 million lines of Rocq, the trusted components, the assumptions and limitations, the named bug examples, the patching workflow and its safeguards, the 36-task efficiency experiment and the shared-workspace experiment, and the subset releaseRead source
  2. [2] Anthropic, Appendix to the formal verification post (October 22, 2026) — read first-hand: about one billion lines of Rocq produced in total with about 180 million in accepted proofs, finished-proof sizes (about 600,000 lines, ranging roughly 330,000–900,000), the statement that proofs which may reveal an unpatched bug are not being released, and the construction of the 36 comparison tasksRead source
  3. [3] Kingy AI, “Anthropic Formal Verification: Claude's Proofs and Their Limits” (October 22, 2026) — independent analysis that inspected the public proof index and release documentation: the released index lists 60 entry points across 25 libraries with 138 proved statements, the release's proofs do not establish termination, and Anthropic's patch penalties and patch audits are discussed as safeguards against behaviour-changing patchesRead source
  4. [4] Unite.AI, “Anthropic Says Claude Proved Security Properties Across 123 Libraries”, October 22, 2026 (secondary summary, used only as a cross-check of the headline figures against the primary post)Read source