239 Proved, 60 in Public, and the Statement Was a Fuzz Test

Anthropic’s post of 22 October says in its opening paragraph that “we need ways to prove that code is free of bugs,” a phrase I would have cut. The work under it, done with the verification company Theorem, is more careful than that sentence. Claude, the post says, “proved that there are no crashes on any input (up to 64 MB) for 239 entry points across 123 different OSS-Fuzz libraries,” over a few weeks, at the level of compiled RISC-V instructions, with every proof checked by the Rocq proof checker. The same post has a section headed “‘Formally verified’ does not mean ‘bug-free.’” Both statements are in the same document, and the second one is right.

In September I wrote about Anthropic’s 13 million lines of Lean for Fermat’s Last Theorem and argued that a proof checker checks a proof against a statement and says nothing about whether the statement is the one you wanted. The software project raises the same question with a better answer than I expected, and it also has a second gap that mathematics doesn’t have: the gap between the binary the theorem is about and the binary anyone runs. Before either of those, though, there is the count.

Three counts of one result

The post’s number is 239 entry points in 123 libraries. The proofs repository Theorem published with the post, theorem-labs/oss-verify-proofs (release 2026.10.0, 22 October), says, as of 23 October, “60 entry points in 25 libraries have proofs.” These two numbers do not contradict each other. The post says it is publishing “Claude’s complete Rocq proofs for fuzz tests that did not require patching,” and that it is not releasing proofs “that may reveal an unpatched bug.” So at least part of the gap of 179 entry points is by design. Still, the result anyone outside the two companies can check today is about a quarter of the headline.

The repository has a third count, and it is the most useful thing in the release. Theorem wrote formal statements for a large slice of OSS-Fuzz, Google’s continuous fuzzing service for open-source code, whether or not anyone has proved them. Of the 1,381 projects in OSS-Fuzz, it can build the fuzz targets of 427. Of those projects’ 5,290 fuzz targets, 2,148 have statements. Across them the release carries 20,164 statements: “138 proved, 0 known false,” 229 “blocked by the model,” and 19,797 open. That ratio, 138 of 20,164, is about 0.7%, and it is a better measure of the job than the headline, because the statements are already written down and anyone can take one.

Counts of projects, fuzz targets and theorem statements, from OSS-Fuzz to proved and public Three rows of dots on a logarithmic axis from 10 to 100,000. Projects and libraries: 1,381 projects in OSS-Fuzz, 427 whose fuzz targets Theorem can build, 123 libraries proved according to Anthropic's post, and 25 libraries with proofs in the public repository. Fuzz targets and entry points: 5,290 fuzz targets in the 427 buildable projects, 2,148 with theorem statements, 239 entry points proved according to the post, and 60 with public proofs. Theorem statements: 20,164 stated in the release, 138 proved. Hollow dots are things that exist or are stated; filled dots are proved. The counts come from two documents and are not a strict funnel. FROM OSS-FUZZ TO PROVED · LOG SCALE · ANTHROPIC POST AND THEOREM-LABS/OSS-VERIFY-PROOFS, 22 TO 23 OCT 2026 Projects, libraries Fuzz targets, entry points Theorem statements 1,381 projects in OSS-Fuzz — oss-verify-proofs README, 23 Oct 2026 427 projects whose fuzz targets build — oss-verify-proofs README 5,290 fuzz targets in the 427 buildable projects — oss-verify-proofs README 2,148 fuzz targets with statements — oss-verify-proofs README 20,164 statements — oss-verify-proofs README 123 libraries proved — Anthropic post, 22 Oct 2026 25 libraries with public proofs — oss-verify-proofs README 239 entry points proved — Anthropic post, 22 Oct 2026 60 entry points with public proofs — oss-verify-proofs README 138 statements proved — oss-verify-proofs README 25 123 427 1,381 60 239 2,148 5,290 138 20,164 public proofs proved, per post buildable in OSS-Fuzz public proofs proved, per post with statements in buildable projects proved stated 10 100 1,000 10,000 100,000 Hollow: exists or stated. Filled: proved. Two documents, so not a strict funnel; the 239 include proofs not in the public release.
The headline, 239 entry points, sits between two other numbers: the 60 anyone can check today and the 20,164 statements written down, of which 138 are proved.

There is a fourth count in the appendix, and I think it is the cost figure the post doesn’t print. “Claude ended up writing around one billion lines of Rocq proofs in this project in its attempt to prove a few hundred OSS Fuzz entry points,” it says, and “about 180 million of these ended up being part of proofs that successfully passed the proof checker.” About 18% of what was written survived. The post’s own phrasing for the cost is that proofs “can take hundreds of millions of tokens to produce.” No total is given.

Who wrote the statement

The Fermat formalization needed someone to state the theorem, and the risk in my September piece was that a model would state it slightly wrong and then prove the wrong thing perfectly. Here the statement is generated, not written. The pipeline compiles a library and its existing fuzz test to a RISC-V executable, combines it with Theorem’s model of RISC-V and of a Linux process, and mechanically produces a theorem that says, in the README’s words, that “on every input on which the plain build stays within its memory budget, neither build reaches an error,” where one build carries AddressSanitizer and the other does not, and the two behave the same. AddressSanitizer is the compiler instrumentation that crashes a program the moment it touches memory it should not.

So the specification comes from the fuzz test itself, which the post calls a “developer-authored entry point” and which existed before the proof, plus whatever AddressSanitizer catches and the requirement that the sanitizer build behave like the plain one. That answers the worry several commenters raised on Hacker News, where one asked whether “the models lie to make a spec they can verify.” For the no-crash theorems, the model inherits its spec from a person.

It also inherits the spec’s reach, and the README is plain about where that ends. A proof “does not say that the library is correct,” because “errors that the sanitizers cannot detect are not excluded: for example, a wrong result or a memory leak.” It “is about the code that one entry point reaches, not about the whole library.” The appendix puts a number on that: the proofs “cover around 20–50%” of the code in the median program, “as exercised by the fuzz driver.” Where a fuzz test asserts something, the proof carries it. The LZO harness compresses its input, decompresses the result, and asserts that both steps succeed and that it gets back exactly as many bytes as it started with; the appendix prints the code, and says that proving those assertions meant proving the compressor and decompressor round-trip correctly. The main post describes the check more strongly, as getting “the original” back, than the asserted line does, which compares lengths. Where the harness only feeds bytes to a parser and checks nothing, the theorem says the parser does not trip AddressSanitizer on any input under the limit. That is still worth having, and it is narrower than “free of bugs.”

Which binary

The second gap is the one the post states most clearly, in its own limitations section. “Our proofs are about single-threaded, static RISC-V binaries linked against musl libc. However, most people run these libraries on x86 or ARM and dynamically link them against glibc.” The README adds that the proofs are “not about the source code, and not about the x86-64 builds of OSS-Fuzz,” that the plain build’s memory budget is a premise (2 GiB for the AddressSanitizer statements), and that “no proof in this release proves a halts statement, so none of them rules out a run that never ends.” The model of Linux itself, which Theorem calls LPS, is described in the same README as “best effort and not complete,” and a proof “is only as good as LPS.” (The release also covers UndefinedBehaviorSanitizer builds, with a 16 GiB budget; I stick to AddressSanitizer here.)

The binary the proofs are about, next to the builds that run elsewhere A six-row comparison. Instruction set: the proved binary is riscv64; OSS-Fuzz builds x86-64, and most users run x86 or ARM. C library and linking: musl, static, against glibc, usually dynamic. Threads: one, against as many as the program starts. Inputs: under 64 MB with the plain build inside a 2 GiB memory budget, against any size. Code: patched where Claude found a bug, against the upstream release until fixes land. Runs that never end: not ruled out, since no halts statement is proved in the release, while a hang is still a failure for a user. PROVED BUILD VS RUNNING BUILDS · ANTHROPIC POST AND OSS-VERIFY-PROOFS README, 22 TO 23 OCT 2026 The binary the proof is about What runs elsewhere Instruction set C library, linking Threads Inputs covered Code Runs that never end riscv64 musl, static one under 64 MB, plain build within 2 GiB patched where Claude found a bug not ruled out: no halts proof yet x86-64 in OSS-Fuzz; x86 or ARM for users glibc, usually dynamic as many as the program starts any size upstream release until fixes land a hang is still a failure Left column from the post's limitations section and the proofs README; right column is the deployment context they name.
Every row on the left is stated by the authors themselves. The work is honest about its scope; the opening sentence of the post is not.

The AddressSanitizer in the proved builds isn’t the standard one either. Clang’s documentation lists “Static linking of executables is not supported” among its limitations, and the README pins a Theorem build called static-asan for every AddressSanitizer binary in the release. That is a reasonable engineering choice for a static RISC-V target. It also means the sanitizer in the theorem is a cousin of the one OSS-Fuzz runs.

None of this makes the proofs less real. A proof that a given binary never trips its sanitizer or an assertion on any input under 64 MB, within its memory budget, is, if LPS is right, a stronger statement than any number of fuzzing runs on that binary, and the proof checker does not care how many lines it was asked to read. The point is narrower: the theorem is exactly as wide as its hypotheses, and every hypothesis on the left of that table is a place where a bug in the shipped build can live without contradicting the proof.

What a line of proof is worth

The post’s comparison point is seL4, the verified microkernel: “it took two person-years to implement the seL4 operating system kernel, but 20 person-years to formally verify it.” Those figures round the 2009 SOSP paper, which gives 2.2 person-years for development and “about 20 py” for the proof, and also the size: 8,700 lines of C and 600 of assembler, and a proof of “200,000 lines of Isabelle script,” roughly 23 lines of proof per line of C.

The ratio for the new proofs depends entirely on what you divide by. The appendix gives two examples. “cJSON’s 391-line parser entrypoint got a 630,000-line proof,” about 1,600 lines of proof per line of entry point. But “in cJSON’s proof only about one-tenth of the lines concern cJSON at all”; the rest re-proves C start-up, the allocator, printf, the sanitizer runtime and the fuzz driver, “from scratch rather than importing it.” The fftw3 library, “with 51,000 lines linked in, received a 480,000-line proof,” under ten lines per line linked in. Over half of each proof, the appendix adds, “is machine-emitted by tools Claude wrote for itself.”

Lines of proof per line of code, depending on what is counted Four lollipops on a logarithmic axis from 1 to 10,000. fftw3: 480,000 lines of proof over 51,000 lines linked in, about 9.4 per line. seL4 in 2009: 200,000 lines of Isabelle over 8,700 lines of C, about 23 per line. cJSON, counting only the tenth of the proof about cJSON: about 63,000 lines over a 391-line entry point, about 160 per line. cJSON, whole proof: 630,000 lines over the same 391 lines, about 1,600 per line. Ratios are the writer's arithmetic from the published figures. LINES OF PROOF PER LINE OF CODE · LOG SCALE · KLEIN ET AL. 2009; ANTHROPIC APPENDIX, 22 OCT 2026 fftw3 seL4, 2009 cJSON, the cJSON part cJSON, whole proof 480,000 lines over 51,000 linked in 200,000 Isabelle lines, 8,700 of C ~63,000 lines, 391-line entry point 630,000 lines, same 391 lines about 9.4 lines of proof per line linked in — Anthropic appendix, 22 Oct 2026 about 23 lines of proof per line of C — Klein et al., SOSP 2009 about 160 lines per entry-point line, cJSON share only — writer's arithmetic from the appendix about 1,600 lines per entry-point line — writer's arithmetic from the appendix 9.4 23 160 1,600 1 10 100 1,000 10,000 Ratios are my arithmetic from the published figures; the denominators differ (whole kernel, code linked in, one entry point).
The same project gives 9 or 1,600 lines of proof per line of code depending on the denominator. Most of the proof is about the runtime underneath the library, which is why proof reuse matters more than the headline size.

That is why the reuse result in the post may matter more than the token result, though both come from the same small benchmark described below. Agents allowed to copy each other’s proofs “needed 17% fewer tokens than when they worked alone,” and the post shows teams adapting another team’s finished proof because “most of a proof concerns code that every program contains.” If nine-tenths of the cJSON proof is about musl, the allocator and the sanitizer, then proving that layer once and importing it is where the cost falls. The token claim, that “Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5,” also comes from 36 small tasks whose inputs the appendix limits to 64 bytes, with libc replaced and a “mini-ASan” of about 100 instructions standing in for a real runtime of “over 100,000.” The 17% comes from a shared workspace of those same tasks; for the real OSS-Fuzz proofs the post shows copied and adapted proofs but gives no token saving. It is a fair benchmark for comparing models with each other, and it measures something other than the cost of a proof in the release.

Theorem’s own roadmap, dated 29 September and edited on 19 October, goes further: 95% of the machine code in nixpkgs “could be verified for about $134M” by the end of 2027, if “models can be made to improve at verification much faster than they improve overall.” The edit adds an evaluation showing performance “doubled every two months between May and September.” That is a company’s projection resting on an extrapolated doubling time, and I would treat the $134 million the way I treat any cost curve fitted to four months of data.

For scale against the published research, the 2026 papers I could find work at the source level or on curated benchmarks. He and colleagues report a framework that proves “up to 77.6% of the theorems” in an seL4 benchmark (arXiv:2603.19715, March), and Li and colleagues’ CCV builds machine-checked memory-safety and leak-freedom arguments for all 299 function definitions across six C benchmarks, with, they report, “less than one person-day” of human effort per benchmark (arXiv:2609.40119, September). As far as I could find, as of today, no 2026 paper proves crash-freedom of real binaries at anything like 239 entry points. The new work is ahead of the literature, which is also why the literature has not checked it yet.

What the attempt found

The part of the post I would put first is the bug list. Trying to prove the theorems “discovered hundreds of bugs,” the post says, without a count, and the examples are the kind a fuzzer is badly placed to find: an out-of-bounds write in a decompressor “only on inputs of around 20 MB that had one rare, specific layout,” an out-of-bounds read in an image decoder “that needed a 64 MB input and over 2 GB of memory,” and a rediscovery of CVE-2026-56132, a heap overflow in libexpat fixed in version 2.8.2 and published in June. Fuzzers, the post notes, typically cap inputs at 1 MB; AFL++’s config.h sets MAX_FILE to 1 MB by default. A proof that has to cover every input up to 64 MB has to look at the 20 MB case, and AFL++ at its default settings cannot even generate it.

There is a catch in how the bugs were handled, and the post flags it in a footnote. When Claude found a bug, it patched the code, the spec was regenerated, and it proved the patched version. “Claude could make any theorem provable by rewriting the program into one that trivially never crashes,” the footnote says, so patches were penalised, extra credit was offered “for proving which inputs it changes and how few they are,” and the patches were logged and audited. That is the right control. Separately, the post publishes proofs only “for fuzz tests that did not require patching” and says it is “not releasing proofs that may reveal an unpatched bug in the open-source software,” so the proofs for patched entry points are not public, and the code in the “Code” row of the table is not the code in anyone’s package manager until the maintainers take the fix.

The earliest program proof I know of also had a termination clause. On 24 June 1949, at the Cambridge conference that marked the EDSAC computer coming into service, Alan Turing gave a three-page paper called “Checking a Large Routine.” He proposed that “the programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole programme easily follows,” worked an example on a factorial routine, and asked for “a quantity which is asserted to decrease continually and vanish when the machine stops,” a proof that it halts. Morris and Jones recovered the typescript and published it with corrections in 1984 (Apt and Olderog’s history of Hoare logic has the quotations). Seventy-seven years on, the assertions are generated from fuzz tests and checked by Rocq, and the release still proves no halts statement. Turing’s second clause is the one still open.

I think the accurate summary is plainer than the post’s opening and more impressive than the Hacker News doubters allow. For 239 entry points, a static RISC-V build was proved never to trip AddressSanitizer or its own assertions on any input under 64 MB, against a specification fixed by an existing OSS-Fuzz harness. Sixty entry points have public proofs, and anyone with half an hour to several CPU-hours and a machine with up to about 20 GiB of memory per proof can check them. The other 20,026 statements in the release are written down and unproved, which makes them the most concrete to-do list for software verification that has been published, and I mean that as praise. “Free of bugs” isn’t on the list. “The statement is still on you” was my summary for OpenAI’s math papers this month, and the software version is that the statement is on whoever wrote the fuzz test, and the binary is on whoever picked RISC-V.

References

  1. Lucas, K., Lynch, A., Tong, L. et al. (2026). LLMs are making formal software verification feasible at a much larger scale. Anthropic Frontier Red Team with Theorem, 22 October 2026.
  2. Anthropic (2026). Appendix to “LLMs are making formal software verification feasible at a much larger scale”. PDF, 22 October 2026.
  3. Theorem (2026). OSS Verify: proofs about OSS-Fuzz fuzz targets. GitHub repository README, release 2026.10.0, read 23 October 2026.
  4. Theorem (2026). static-asan. GitHub repository, read 23 October 2026.
  5. von Ebers, M., Hampton, I., Agrawal, H. et al. (2026). Bootstrapping the Verified Software Stack. Theorem, 29 September 2026, edited 19 October 2026.
  6. Hacker News (2026). LLMs are making formal software verification feasible at a much larger scale. Discussion thread, posted 22 October 2026.
  7. LLVM Project. AddressSanitizer. Clang documentation, read 23 October 2026.
  8. AFLplusplus. include/config.h. Stable branch, read 23 October 2026.
  9. National Vulnerability Database (2026). CVE-2026-56132. Published 19 June 2026.
  10. He, B., Li, Z. et al. (2026). Neuro-Symbolic Proof Generation for Scaling Systems Software Verification. arXiv:2603.19715, 20 March 2026.
  11. Li, H., Wang, Z. et al. (2026). Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements. arXiv:2609.40119, 30 September 2026.
  12. Klein, G., Elphinstone, K., Heiser, G. et al. (2009). seL4: Formal Verification of an OS Kernel. Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), October 2009.
  13. Turing, A. M. (1949). Checking a Large Routine. Report of a Conference on High Speed Automatic Calculating Machines, University Mathematical Laboratory, Cambridge, 24 June 1949.
  14. Morris, F. L. & Jones, C. B. (1984). An Early Program Proof by Alan Turing. Annals of the History of Computing 6(2), April 1984.
  15. Apt, K. R. & Olderog, E.-R. (2019). Fifty Years of Hoare’s Logic. arXiv:1904.03917, 8 April 2019.
  16. Gautam Parab (2026). 13 Million Lines of Lean in 11 Days. The Hard Part Was Never the Proof.. 4 September 2026.
  17. Gautam Parab (2026). OpenAI’s 722 Math Papers: The Proofs Can Be Machine-Checked. The Statements Are Still on Us.. 7 October 2026.