On October 22, Anthropic's Frontier Red Team and the verification company Theorem reported that Claude had written about 180 million lines of machine-checked proof showing that 239 fuzzing entry points, across 123 open-source libraries, never crash on any input under 64 MB. The proofs concern compiled RISC-V binaries, not source code, and writing them surfaced hundreds of bugs. The line count is the headline; the consequential number is the price of a proof, now quoted in tokens rather than person-years.
What "never crashes" means, precisely
Each specification comes from a Google OSS-Fuzz harness: for every input under 64 MB, and for every modeled Linux response and memory layout, the harness exits normally, with no failed assertion and none of the memory errors AddressSanitizer would flag (Anthropic). Theorem's formal semantics of RISC-V instructions and Linux processes turn each binary, a median of 18,000 instructions, into a mathematical object. Claude writes the proof, typically about 600,000 lines, and the kernel of Rocq, the prover formerly called Coq, checks it. Since a failed assertion counts as a crash, a harness that asserts an LZO round trip yields a correctness result for that round trip.
The fine print is most of the story. The proofs cover single-threaded, statically linked binaries built against musl, so concurrency and dynamic linking are out of scope, while most real deployments run x86 or ARM with dynamically linked glibc. AddressSanitizer misses some memory-safety bugs, so the proofs do too. Not every entry point was verified, dead code is untouched, and a caller can still misuse a library and corrupt its own memory. Logic bugs that never crash are invisible to a no-crash theorem, and inputs of 64 MB or more fall outside it entirely. Anthropic's own line: "formally verified" does not mean "bug-free."
One hazard is specific to machine provers: Claude could make a theorem provable by quietly rewriting the program so it never crashes. The team penalized patches and audited the ones it logged (Anthropic).
The bugs fuzzing walked past
Anthropic says Claude found bugs that had survived years of fuzzing and trillions of test runs, then patched them (Anthropic). The examples are a tour of fuzzing's blind spots: a counter underflow in a decompressor that becomes an out-of-bounds write only with a roughly 20 MB input and one rare memory layout; an out-of-bounds read in an image decoder that needs a 64 MB input and more than 2 GB of memory; a rediscovery of CVE-2026-56132 in libexpat, triggered by deeply nested input. In one PDF reader, a week of proof work turned up as many security bugs as are typically reported in a year, and a logic bug in another widely used program had sat unnoticed for more than a decade. A subset of the proofs is being published; proofs that could expose unpatched bugs are withheld.
From person-years to a token bill
Verification used to be priced in careers. Anthropic's post says seL4, the verified microkernel, took two person-years to build and 20 to verify. The seL4 team's own accounting differs: about 25 person-years for the whole project, design and implementation included, producing 200,000 lines of Isabelle proof for 7,500 lines of verified C, with about 12 of those years spent on the kernel proof itself, at a cost Gerwin Klein put at about $700 per line of code.
Claude's corpus is about 900 times seL4's original proof, one typical proof alone is three times larger, and the whole set took a few weeks, Anthropic says.
The bill now comes in tokens. A single proof can consume hundreds of millions of them, and the total cost was not disclosed. On Anthropic's own 36-task benchmark, Opus 5.5 proved half the tasks with about 40% fewer tokens than Opus 5, and agents sharing a workspace used 17% fewer tokens than agents working alone (Anthropic). Those are vendor-run numbers on a small set, but the direction is the argument. When the scarce input was a proof engineer's decade, verification was reserved for kernels, compilers and avionics. When it is a compute line that shrinks with each model generation, the question becomes which code is worth the tokens.
Why prove the binary, not the source
A proof about source code leaves a gap between what was proved and what runs. Klein's seL4 paper was explicit about the toolchain: "we need to assume correctness of the C compiler and linker." In 2013, Sewell, Myreen and Klein used translation validation to carry seL4's proof down to binaries from an unmodified gcc 4.5.1. CompCert, about three person-years and 42,000 lines of Coq, attacked from the other side by proving that the compiler itself preserves the semantics of the source program; in a 2011 study it was the only compiler tested in which the Csmith random tester found no wrong-code errors.
Anthropic sidesteps the compiler question by proving the machine code. Whatever the compiler did with undefined behavior or an aggressive optimization is already inside the artifact under proof. The trust does not vanish; it moves into the RISC-V and Linux process models, the exact theorem statements and the Rocq checker, plus the hardware, operating system and OCaml compiler that Rocq runs on (Anthropic). In a side study, Claude proved the Linux kernel's zlib against an RFC 1950 specification at the x86 binary level, using x86 semantics it generated itself and tested heavily: a reasonable bet, and a new entry in the trusted base.
Outside reaction is thin so far. Interesting Engineering and The Decoder relayed the figures without independent evaluation, and The Decoder noted that humans at Theorem built the tooling and formal foundations. The developer Fabio Akita, writing two days later, put the limits in one line: "Formal proof is a scoping tool, not a coverage tool." Proofs, he adds, break when code changes, so maintenance is the next bill.
The 30,000-foot read
The old objection to formal verification was never that it failed; it was the two dozen person-years per kernel. That objection has become an invoice, and invoices shrink. What does not shrink on its own is the cost of stating the right theorem: a model of a machine, a 64 MB bound somebody chose, a harness that asserts the right things. Those remain human work, and Anthropic lists them rather than burying them.
Watch for proofs on x86 and ARM with dynamic glibc, and on threaded code; an independent audit of Theorem's semantics; a dollar cost per proof; Theorem's next targets, which The Decoder reports as glibc, OpenSSL and cURL; and whether maintainers will keep proofs green, like tests. Verification is no longer a question of whether we can afford it. It is becoming a question of what we bother to specify.
Sources: Anthropic research post (primary: all project figures, the property with its assumptions and limits, bug examples, reward-hacking safeguards, 36-task benchmark, trusted base, zlib study, the two-versus-20 person-year seL4 comparison, release plans); The Decoder (undisclosed total cost, Theorem's role and roadmap); Interesting Engineering (independent restatement of figures and scope); Trustworthy Systems, seL4 numbers (about 25 person-years, 200,000 lines of proof, 7,500 lines of verified C); Klein, From a Verified Kernel Towards Verified Systems (about 12 person-years for the kernel proof, about $700 per line, trusted compiler and linker); Sewell, Myreen and Klein, PLDI 2013 (binary-level translation validation of seL4); Leroy, Formal verification of a realistic compiler (CompCert effort and size); AbsInt, CompCert (semantic preservation guarantee, 2011 Csmith study); Rocq 9.0 release notes (Coq renamed Rocq); Fabio Akita (outside reaction). CAVEATs: all project figures, bug examples and benchmark results are company-reported by Anthropic and Theorem and have not been independently replicated; the 36-task benchmark is vendor-run, and the bug count is given only as hundreds, with no exact number. No dollar cost was disclosed. Sources disagree on seL4's effort (Anthropic: two person-years to build, 20 to verify; the seL4 team: about 25 for the whole project, about 12 for the kernel proof), and both are given. The chart compares line counts across different provers (Isabelle, Rocq), authors (human, machine) and properties (functional correctness, no-crash), so it measures bulk, not difficulty. We found no named formal-methods academic reacting in reputable outlets by publication time; the outside reaction cited is a practitioner's blog. The Decoder's headline describes Claude writing code; the work verified existing library code. Anthropic's appendix PDF, the released proof repositories, Theorem's site, LWN's coverage and the seL4 journal paper could not be opened by our fetcher, so claims about them rest on Anthropic's post and the seL4 team's own pages above. The assignment's leads all checked out against the primary source; the one addition is that the property also holds across every modeled OS response and memory layout.