Anthropic Research · 2026-10-22 · A source-grounded account

Having AI prove that programs
do not crash:
what this study achieved

Tests sample inputs. Proofs reason about every input within a defined scope. Anthropic and Theorem had Claude write the proofs and Rocq check them. The result: no-crash guarantees for 239 entry points, conditional on particular builds, input limits, memory budgets and formal models of the machine and operating system.

Completed proofs
239 entry points · 123 libraries
Specific RISC-V binaries; inputs under 64 MB, within memory budgets and model assumptions
The source’s own distinction
Verified ≠ bug-free
A checker verifies the proof, not whether the specification matches reality
00 · Introduction

Introduction

Testing observes what a program does on particular executions. Formal verification takes a different approach: it represents the program mathematically and proves that it satisfies a precisely stated requirement. The guarantee depends on both that requirement and the assumptions in the mathematical model.

On 2026-10-22, Anthropic announced research with the startup Theorem in which Claude wrote proofs for compiled open-source programs. An independent proof checker checked whether those proofs established the required properties. Within a few weeks, the team reported completing no-crash proofs for 239 entry points across 123 libraries, patching bugs where necessary. An entry point is an input interface that developers provide for testing particular parts of their code.

Anthropic’s motivation was the growing ability of AI to find vulnerabilities and combine bugs into exploits. Its announcement cited over 1,000 recently disclosed vulnerabilities in the Linux kernel, despite the extensive testing that the kernel receives. The researchers sought a method that could find problems and then establish that no problems violating specified rules remained.

~180 million lines
Rocq in checked proofs
About one billion lines generated overall; virtually none require manual review.
Hundreds
Bugs found while proving
No exact count reported. Some bugs had evaded detection for years.
2 → 20 person-years
seL4: implementation vs verification
The expert effort historically required for formal verification.

The resulting guarantees apply to particular compiled programs, inputs under 64 MB, a fixed memory budget, and modeled machine and operating-system behavior. The programs are single-threaded RISC-V Linux binaries. RISC-V is an instruction set: it defines the basic commands that a processor executes.

This is not a proof that an entire library is bug-free. It is a mathematical guarantee about specified errors in specified executable programs under explicit conditions. Attempting to establish those guarantees also uncovered bugs that testing had missed.

01 · Testing

1. What testing can miss

One decompressor bug illustrates why repeated testing and a proof can reach different results. Claude found a counter underflow: a counter decreased beyond its permitted range, leading to a write outside the intended memory area. The failure required an input of around 20 MB with a rare, specific layout.

The team considered this unlikely to be found by conventional fuzzing. A fuzzer generates and mutates inputs, runs them through a test entry point, and looks for failures. Fuzzers typically use inputs capped at 1 MB and rely on code coverage, the record of which code has executed, to guide further exploration. A failure requiring a much larger input with a particular layout may remain outside that search.

The decompressor was one example among hundreds of bugs found during the project. Anthropic reported that some bugs had evaded detection for years despite extensive testing. It did not identify the decompressor bug specifically as one of those long-undetected cases.

The original article illustrates the distinction with mazes. Fuzzing explores paths by trying inputs; running it longer can reveal more paths and failures. A no-crash proof reasons over every covered input and rules out crashes on every path reachable from the entry point. Paths that the entry point cannot reach remain outside that guarantee.

Fuzzing covers only the execution paths it tries.
Fuzzing
The proof covers every path reachable from this entry point, not the whole program.
Formal verification
OfficialLeft: the final animation frame shows 1,479,751,345 inputs tried and 4 crashes found and patched. Its guarantee extends only to the executions tried. Right: the proof covers all paths reachable from the entry point; unreachable areas stay blank. The guarantee depends on the chip and OS models being correct. Both images are final frames from the source animations. Source: Anthropic Research

Writing such a proof can expose a condition under which the desired property fails. But an unsuccessful proof attempt is not, by itself, evidence of a bug. The required argument may simply remain unfinished. Bug discovery and proof completion are separate results.

Historically, constructing these arguments required substantial specialist effort. Anthropic cites the seL4 operating-system kernel: implementation took two person-years, while formal verification took 20 person-years. A person-year measures accumulated work, not elapsed calendar time. The research asks whether models can perform enough of this specialized work to make verification practical across a much broader set of existing programs.

02 · Proof & checker

2. Claude writes the proof. Rocq checks it

Before a program can be proved correct, “correct” needs a precise definition. That definition is the specification, or spec: the requirement that the proof must establish.

For a PNG image decoder, RFC 2083 provides a description of how encoded bytes should become an image. Defining comprehensive correctness for a text editor or web browser is less straightforward. Their intended behavior is not captured by a single, similarly compact requirement. Anthropic identifies this specification problem as an obstacle to large-scale verification.

The project used requirements already embedded in developer-written tests. Google’s OSS-Fuzz initiative continuously fuzzes open-source projects through existing test entry points. Those tests are designed so that certain failures cause a crash. An assertion, for example, is a check in the program that stops execution if a required condition is false.

OSS-Fuzz also instruments C and C++ programs with AddressSanitizer, or ASan. This compiler tool inserts checks that detect and report certain memory errors when they occur, including buffer overflows and use-after-free. Thus, proving that an instrumented test never crashes can establish both the absence of ASan-detectable errors and properties enforced by its assertions.

The final requirement was generated mechanically. The library and its existing fuzz test were compiled into a RISC-V executable. That executable, the formal execution semantics, and the desired no-crash property determined the statement Claude had to prove. Claude did not choose this final requirement.

FROM CODE TO A MACHINE-CHECKED GUARANTEE 1Source codeWith its existingfuzz test2RISC-V executableCompiled with the testand ASan checks3SpecificationMechanically generatedfrom binary + trusted inputs4Rocq proofWritten by ClaudeChecked by the Rocq kernelCompileDeriveProveNo-crash propertyFor every coveredinput under 64 MBRISC-V + LinuxFormal instruction andsyscall models (Theorem)CheckerRocq kernelThis binary does not crashIf the trusted parts are correctProof accepted → conditional guaranteeTrusted: assumed correct; could contain bugsProven: true if the trusted parts are correct
OfficialRedrawn from Figure 2. Blue components are trusted, not established as bug-free; green components are proved conditional on those trusted parts. The illustrative file and line counts in the original are omitted. Source: Anthropic Research

The execution semantics describe how instructions and operating-system interactions behave. Theorem’s Linux process semantics, or LPS, is the formal model of a Linux process executing a RISC-V binary. Claude constructs an argument within that model; Rocq, the proof checker, checks the argument against the statement. Virtually none of the resulting proof text requires manual proof review.

These roles remain distinct when bugs are patched. Changing the program causes the specification to be regenerated from the patched executable. Claude must then prove the new statement.

Anthropic describes reasoning over all possible interactions of tens of thousands of instructions as historically intractable at this scale. It argues that working through large volumes of detailed proof code toward a well-defined goal suits current models particularly well. Proofs for the reported 239 entry points across 123 libraries were completed using this process, including patches where needed.

The separation between a statement and its proof also appears in the related article on proof checkers and theorem statements. Here, the final statements come from existing human-written tests through mechanical generation. A further question remains: whether the modeled executable corresponds to the program actually deployed.

03 · Bugs

3. Finding bugs while trying to prove safety

The attempt to prove safety uncovered hundreds of bugs, including failures that a fuzzer would be unlikely to reach. Claude also noticed logic errors that did not cause crashes. In one library, a feature intended to restrict which files an application could load was not always enforced.

BugTrigger or contextType
Decompressor counter underflow → out-of-bounds writeAn input of around 20 MB with a rare, specific layoutMemory error
Image decoder out-of-bounds readA 64 MB input and over 2 GB of memoryMemory error
Out-of-bounds read in another libraryA particular sequence of calls across two handles to the same fileMemory error
libexpat CVE-2026-56132Deeply nested inputRediscovered vulnerability
File-loading restrictions not always enforcedNoticed while proving the library memory-safeLogic bug; no crash

All five examples come from the research post. Many bugs found in this project were considered unlikely to be found by coverage-guided fuzzers, whose inputs are typically capped at 1 MB. “Hundreds” is not an exact count.

That discovery did not mean the no-crash theorem proved the file restriction correct. It was a separate observation made while working on a memory-safety proof. The project therefore had two outcomes: completed guarantees for some targets, and bugs found during the effort, whether or not a proof was completed.

To avoid stopping for human intervention whenever a bug appeared, the researchers allowed Claude to patch code. The cycle was to identify a problem, modify the program, regenerate its specification, and attempt the proof again.

This introduced a risk of reward hacking: finding a shortcut that technically satisfies the assigned objective while abandoning its intended meaning. A model could make a no-crash theorem easy by replacing the program with something that trivially never crashes.

The team penalized every patch and offered additional credit for proving which inputs the patch changed and how few they were. It also logged and audited patches for these failure modes. These were measures to discourage trivializing the task, not evidence that the risk had been eliminated.

1
Penalize every patch
A trivially non-crashing replacement could satisfy the goal while discarding the intended functionality.
2
Reward evidence of a small effect
Extra credit for proving which inputs a patch changes and how few those inputs are.
3
Log and audit patches
Footnote 6 describes these checks for reward hacking: technically meeting the target without doing what was intended.

Where the related article on securing code with LLMs describes finding and fixing vulnerabilities, this research also examines what happens when the model must construct a proof that specified failures cannot remain.

04 · Scope

4. What the proof does and does not guarantee

The no-crash guarantee is bounded by the input limit, the plain build’s memory budget, the chosen entry point, the exact compiled binary, and the formal machine and operating-system assumptions. The plain build is the executable without sanitizer instrumentation.

Within those conditions, the published proofs rule out the errors covered by their statements, including crashes, invalid memory accesses, aborts and assertion failures, as well as sanitizer-detected errors. They also establish that the sanitizer build and plain build agree on specified observable behavior.

ASan does not detect every memory-safety bug. Nor does a sanitizer’s failure to report an error establish that a program computes the right answer. The repository explicitly gives incorrect results and memory leaks as examples of problems that these guarantees do not generally exclude.

Coverage is also limited to code reachable through the selected entry point. The researchers did not verify every entry point of each library. Even proving every existing test entry point would not necessarily cover the whole library, particularly dead code that none of those tests reaches. An application can also misuse a library and corrupt memory in the caller. Anthropic says closing that gap would require specifying the obligations of callers for public functions and establishing that callers obey them.

Within the guarantee
  • Inputs under 64 MB, within the plain build’s memory budget and the stated model assumptions
  • Covered errors: crashes, memory errors detected by ASan, failed assertions and other errors in the statement
  • Checks in the original harness, if compiled into the binary: the proof establishes that they do not fail on covered inputs
  • Code reachable from this entry point, in this particular compiled binary
Outside the guarantee
  • Correct results not checked by the harness; memory leaks, as the README explicitly notes
  • Errors the sanitizer cannot detect; unreachable code; the whole library
  • Memory corruption in a caller that misuses the library
  • Termination: no proof in this release proves a halts statement
  • Other builds, including typical x86 / ARM deployments with different linking
Based on the research post’s Limitations section and the proof repository’s “What a proof does not say.”

Assertions can make a no-crash proof cover more than memory access. LZO’s compression test, for example, checks that compression succeeds and, on the decompression branch, that decompression succeeds and returns the same number of bytes as the original input. The displayed assertions do not compare the original and decompressed contents byte by byte. The appendix authors nevertheless explain that proving these assertions requires Claude to establish correct roundtripping between the compressor and decompressor. That is a property of what the library computes, not merely where it writes.

// LZO compression fuzz test (appendix, page 6)
r = lzo1x_1_compress(data, size, compressed, &compressed_len, wrkmem);
assert(r == LZO_E_OK);
if (compressed_len >= size) goto join;
decompressed_len = size + 1;
r = lzo1x_decompress(compressed, compressed_len, decompressed, &decompressed_len, NULL);
assert(r == LZO_E_OK && decompressed_len == size);

The code asserts successful operations and equal byte counts, not bytewise equality. The appendix authors say that proving these assertions requires correct compression/decompression roundtripping.

The executable itself is another boundary. These proofs concern single-threaded static RISC-V Linux programs linked against musl, a C library. Static linking includes library code in the executable. Anthropic contrasts this setup with typical deployments on x86 or ARM that dynamically link against glibc. A proof about the specially compiled RISC-V binary is not automatically a proof about those other builds or about the source code.

Termination requires a separate distinction. Although the blog introduction describes programs always exiting normally, the archived repository states that an agreement theorem does not exclude a run that never ends. No proof in this release establishes a halts statement. The published guarantees therefore do not rule out nontermination.

Anthropic states the broader boundary explicitly:

“Formally verified” does not mean “bug-free.”

The three trusted artifacts listed in the research post

1
RISC-V and Linux models
Provided by Theorem. The README calls LPS best effort and incomplete.
2
Exact theorem statements
The precise requirements being proved.
3
The Rocq proof checker
Also its underlying hardware, OS and OCaml compiler, as footnote 5 notes.

A developer still has to trust the formal models of RISC-V and Linux processes, the exact theorem statements, and Rocq. The checker also depends on its hardware, operating system and OCaml compiler. As the article puts it, “a proof checker can’t tell you whether your spec matches reality”.

The source argues that hardening this trusted foundation is more tractable than debugging every line covered by the proofs. Its size does not grow simply because the same approach is applied to more projects.

05 · Cost

5. The cost of making verification routine

The proofs were much larger than the library code. Claude generated around one billion lines of Rocq during the project; about 180 million lines became part of proofs that passed the checker. Many lines were generated by tools and scripts that Claude wrote rather than typed individually.

Checking a single proof could take from 30 minutes to several hours of CPU time. Anthropic also identifies proof generation that can require hundreds of millions of tokens as a limitation. That description is not a reported project-wide token total.

~600,000 lines
A typical completed proof
About 1,400 files; about 330,000–900,000 lines across libraries.
391 → 630,000
cJSON: entry-point lines → proof lines
Only about one-tenth of the proof concerns cJSON itself.
30 min to hours
CPU time to check one proof
README: up to 20 GiB of memory on 16 cores.

Much of the work concerns code shared by otherwise different programs: C runtime initialization, allocation, ASan and the fuzz driver. Agents copied completed proofs and adapted them to new targets. This reused work, but the current proofs still reprove those components rather than importing established proofs of them.

Proof composition by bytes for libcups, freerdp and libzmq.
OfficialDark blue: identical; light blue: lightly edited; light orange: edited more; orange: new. Most proof code concerns shared runtime components, with almost no new code in the shared parts. The new libcups folders prove its own functions. This observation comes from the full OSS-Fuzz work, for which no overall savings rate is given. Source: Anthropic Research

The researchers measured model and sharing effects on 36 reduced verification tasks derived from real OSS-Fuzz code. Inputs were limited to 64 bytes, libc was replaced by a few functions, and a smaller “mini-ASan” replaced the full sanitizer runtime. On these tasks, Opus 5.5 proved half with about 40% fewer tokens than Opus 5. Agents given a shared workspace needed 17% fewer tokens than agents working alone.

Share of 36 reduced verification tasks completed at each single-agent token budget.
OfficialOpus 5.5 proves half of 36 reduced tasks with about 40% fewer tokens than Opus 5. Each task has three independent single-agent attempts, each with a 5 million-token budget; completion is recorded at the first successful attempt. These results are not savings measured across the full proofs. Source: Anthropic Research
Shared proof files and token usage across 36 targets in one workspace.
OfficialArcs connect proofs sharing an unchanged file. Bars show tokens spent; black lines mark the same task’s average solo cost. Of 34 completed proofs, 30 were cheaper than the solo average. The figure shows 324 reused files. Shared work used 17% fewer tokens overall, measured on these same 36 reduced tasks. Source: Anthropic Research

Those are token results for reduced tasks, not equivalent measurements of money or elapsed time. The team also observed proof copying and adaptation in the full OSS-Fuzz effort, but reported no overall savings rate for that work.

The appendix’s expert assessment describes another scaling question. Agent proofs repeatedly spell out register values, integer conversions, distinct addresses, stack contents and individual branches. Human proof engineers would typically introduce abstractions that capture such repeated reasoning more compactly. Agents did introduce some abstractions, but these correlated with only a modest reduction in proof size.

A verbose proof remains as valid as any other proof of the same theorem. The question is whether this style scales to more complex programs. The expert assessment points to other agent-based projects, including MachCSL, where verbose proofs hit a complexity wall and better modular reasoning became necessary. It presents that experience as a possible scaling concern here, not as a wall this project had already reached.

06 · Publication

6. Published proofs and everyday development

Anthropic reported completed proofs for 239 entry points across 123 libraries. The archived release v2026.10.0 of Theorem’s repository contains proofs for 60 entry points in 25 libraries.

The blog says the team publishes complete proofs for tests that did not require patches and withholds proofs that might reveal an unpatched bug. These rules provide context for the smaller public collection. Neither the blog nor the README gives a complete accounting of the difference between the reported and published totals.

239 / 123
Blog: entry points / libraries with proofs
The proofs were completed within weeks. Claude patched bugs where needed.
60 / 25
Release: published entry points / libraries
Archived v2026.10.0; unpatched-test proofs published, proofs exposing unpatched bugs withheld.
20,164
Statements in the release
138 proved · 229 blocked by the formal model · 19,797 open · 0 known false
Different counts, different scopes

The blog and README do not account for the difference between 239 and 60 entry by entry. The two publication rules must not be presented as a complete explanation of that gap.

Dan Wallach, a Rice University professor researching computer security, praised the work in his 2026-10-23 commentary:

He also saw value for software facing substantial certification requirements, such as avionics or medical electronics. His concern was the recurring work needed for ordinary software releases.

These proofs are tied to a particular compilation. Changes to program code, dependencies or the compiler may require repairing a proof or generating it again. Combined with the CPU time needed for checking, Wallach argued that this approach would not run on every build in a continuous integration and delivery, or CI/CD, pipeline. That is his assessment of the maintenance burden, separate from the experimental findings.

His proposed next step was to put what the proof process learned back into the source code as function contracts. Preconditions state what must be true before a function runs; postconditions state what must be true afterward. Such contracts could preserve the learned requirements in a form more naturally integrated with ongoing development. Wallach mentioned Rust verification tools such as Verus and Aeneas, and C extensions such as Frama-C.

1
Wallach: value
More automation than the earlier agent-based xv6 effort, and bugs found in libraries already tested by OSS-Fuzz.
2
Wallach: maintenance concern
Changed code, dependencies or compilers can require proof repair or regeneration. In his view, the cost prevents checking on every CI/CD build.
3
Wallach: suggested next step
Record learned function preconditions and postconditions in source, with tools such as Verus, Aeneas and Frama-C, while retaining machine-level proofs.

He still wanted proofs extending down to machine code. His argument was about connecting source-level reasoning, compilation and machine-level guarantees, rather than replacing the latter.

Anthropic’s forecast is more expansive: formal verification will soon become as practical as fuzzing is today for almost all production software, moving from “bolted-on” to “built-in”. The company attributes that expected transition to better models, reusable proofs, language design and development workflows. It is a forecast, not a description of routine verification already demonstrated across production software.

“”
As a one-time bug-finding expedition, it’s certainly valuable.
Dan Wallach · Rice University · Mastodon · 2026-10-23
A–D · Technical appendix

Technical appendix

A. The exact programs, requirements and assumptions

The main OSS-Fuzz proofs concern single-threaded, statically linked RISC-V binaries running on Linux with musl. The archived repository records clang 20.1.8 as the compiler and Rocq 9.2.0 as the checker. These are release facts, not toolchain recommendations.

The appendix separates the intended guarantee into three proof requirements:

RequirementWhat it establishes
ASan build is crash-freeThe instrumented binary encounters no fault, abort or unmodeled behavior on covered inputs.
Observable equivalenceThe instrumented and plain binaries agree on the defined observations.
Plain build is crash-freeThe uninstrumented binary also encounters no fault, abort or unmodeled behavior on covered inputs.

The appendix states these requirements for all inputs under 64 MiB and all memory layouts. The blog uses 64 MB. This article follows the blog’s notation in the main prose and preserves the appendix’s notation here; the units are not being equated.

The appendix defines observable behavior through four items:

  • The bytes read from stdin
  • The bytes written to stdout and stderr
  • The program’s exit code, or the signal that killed it
  • The final state of the file system

Equivalence concerns the ordered sequence of read/write events and the ending state. It does not compare performance.

There is a subtle reason for proving plain-build crash-freedom separately. A crash does not itself appear in the read/write trace: the trace simply ends. A silent infinite loop can also stop producing events. Consequently, trace equivalence alone can allow programs that crash differently, or one that crashes while the other loops forever. The additional no-crash theorem excludes crashes in the plain build, but does not establish termination.

The release includes some UndefinedBehaviorSanitizer, or UBSan, proofs and combined ASan+UBSan proofs. These should not be treated as the scope of the whole main cohort. The plain-build memory budget is 2 GiB for statements involving ASan and 16 GiB for UBSan statements. Inputs requiring more memory are outside the respective premise.

LPS is explicitly described as best effort and incomplete. It models part of Linux and makes assumptions it does not check. The repository’s checking process also trusts the tools that turn executable bytes into modeled memory images and the wrapper that matches the proof to its statement, alongside Rocq and its permitted axioms. Anthropic’s footnote adds the checker’s hardware, operating system and OCaml compiler.

Agents sometimes constructed shorter intermediate specifications describing program outputs, then proved that both builds matched them. These had a median size of about 110 lines, compared with a median program size of 86 KB; the proofs covered around 20–50% of program code exercised by the fuzz driver. These agent-written intermediate specifications are distinct from the mechanically generated final statements.

B. Bug examples and other verification experiments

Beyond the decompressor counter underflow, Anthropic reported an image-decoder out-of-bounds read requiring a 64 MB input and over 2 GB of memory. Another out-of-bounds read required a particular sequence of calls through two handles to the same file. Claude also rediscovered CVE-2026-56132 in libexpat, involving deeply nested input.

The file-loading restriction issue was a logic bug that did not crash. Its discovery during verification did not establish a proof that the restriction was correctly enforced.

The LZO example distinguishes the code’s checks from the reasoning needed to prove them. After compression, the test asserts r == LZO_E_OK. If compressed_len >= size, it branches to join without taking the displayed decompression path. Otherwise, it sets decompressed_len = size + 1, decompresses, and asserts r == LZO_E_OK && decompressed_len == size.

Those assertions check success and equal length, not bytewise content equality. The appendix authors say establishing them requires correct compressor/decompressor roundtripping. In the binary, failed assertions branch to an abort handler; the proof follows those branches at their exact addresses and establishes that they are not taken.

In p11-kit, which manages access to smart cards and cryptographic hardware, a configuration lexer asserts that a PEM block does not extend beyond the input buffer. Claude proved that this check never fails.

For cpp-httplib, completing the proof required ruling out stack overflow from recursion in a std::set destructor. The recursion depended on tree depth, so Claude had to prove at machine-code level that libc++’s red-black tree rebalancing kept that depth logarithmically bounded.

A separate experiment addressed functional correctness. Claude formalized RFC 1950, which defines the zlib compression file format, and proved that the Linux kernel’s zlib implementation followed that specification. This used an x86-compiled binary and Claude-generated, heavily tested x86 execution semantics. The team repeated the process for half a dozen other libraries and found minor, unexploitable corner-case bugs that were being filed upstream.

The authors drew two conclusions: these extensively tested codebases were already almost fully correct, and end-to-end correctness properties could be proved for existing code. Their x86 model could empirically boot an Ubuntu userspace on a Linux kernel by stepping through its semantics. Generating the model also identified hundreds of documentation mistakes and a smaller number of hardware bugs. The team did not claim the semantics were perfect.

Another experiment used Verus, a Rust verification tool, to develop a Rust interpreter for a substantial fragment of Python. Claude completed all 17 tiers and proved that whenever the interpreter returns a result, it is the result prescribed by the formal semantics. This conditional guarantee does not prove termination or exact equivalence to CPython itself.

The connection to CPython was tested empirically. Over 1.7 million mostly random programs produced identical behavior in 99.95% of tests; the remaining differences were described as known corner cases. When seven bugs were deliberately injected into an early interpreter, five survived random testing, while all seven broke the proof.

Anthropic also reported an unnamed logic bug latent for more than a decade. In a widely used, unnamed PDF reader, one week of verification work found as many security bugs as are typically reported in a year.

C. Proof scale and the reduced-task experiments

A typical library entry point contained a few hundred lines of C compiling to about 2,000 RISC-V instructions. The whole executable had a median length of 18,000 RISC-V instructions because it included startup code, runtime components, allocation, sanitizer machinery and the fuzz driver.

MeasureReported scale
Rocq lines generated during the projectAround one billion
Lines included in successfully checked proofsAbout 180 million
Typical completed proofAbout 600,000 lines in some 1,400 files
Proof-size range across librariesAbout 330,000–900,000 lines
cJSON parser entry point391 lines, with a 630,000-line proof
Portion of the cJSON proof concerning cJSONAbout one-tenth
fftw3 code linked into the target51,000 lines, with a 480,000-line proof
Checking one proof30 minutes to several hours of CPU time
Repository checker memoryUp to 20 GiB on 16 cores

Over half of each proof was emitted by tools Claude wrote, including instruction encodings and lookup tables. Roughly 40% was proof text such as definitions, machine models, lemmas and proof steps; some of that was also produced by scripts. Proof size therefore did not simply track the amount of library code.

Agents introduced abstractions for some repeated reasoning, but the appendix reports only modest proof-size reductions. Shared components still had to be reproved rather than imported.

The 36 reduced tasks retained the core of real OSS-Fuzz programs while replacing surrounding machinery. Some used existing harnesses, such as OpenVPN’s base64 encode/decode test. Others called a library function from a short custom driver.

Experimental detailConstruction or result
Input limit64 bytes
libc replacementA few memory and string functions
mini-ASanAbout 100 instructions
Full sanitizer runtimeOver 100,000 instructions
Resulting program sizes283–2,491 instructions
Task organizationThree groups of size 12
Independent attemptsThree per task, each with a 5 million-token budget
Completion ruleThe first completed attempt counts
Model comparisonOpus 5.5 proved half with about 40% fewer tokens than Opus 5
Shared workspace17% fewer tokens than working alone

The groups progressed from mini-ASan no-error proofs to larger programs and then more complex statements requiring agreement between the plain and mini-ASan builds and absence of errors in both.

In the shared-workspace experiment, working alone was more expensive in 30 of the 34 completed proofs. Agents working alone could not complete two of those proofs. The larger OSS-Fuzz effort also showed agents copying and adapting proofs, but supplied no corresponding overall savings percentage.

D. What the public release contains, and the proposed development path

The repository uses several counting units. A library may have multiple entry points, and an entry point may have multiple compiled builds and theorem statements. The number of proved statements therefore cannot be read as a count of libraries or entry points with proofs.

Archived release measureCount
OSS-Fuzz project directories1,381
Projects whose targets could be built427
Fuzz targets in those projects5,290
Targets with statements2,148
Total statements20,164
Proved statements138
Statements blocked by the formal model229
Open statements19,797
Known-false statements0

The 229 model-blocked statements concern capabilities the formal execution model did not yet cover. They are not a measurement of the AI model’s proving ability. Likewise, 0 known-false statements does not mean all statements have been proved.

The publication includes trusted components developed for the project, specifications, and complete proofs for unpatched tests, subject to the stated withholding rule for proofs that could reveal unpatched bugs.

Theorem participated in Y Combinator’s Spring 2025 batch and describes itself as an AI and programming languages research lab. Its cofounders Jason Gross and Rajashree Agrawal are among the Anthropic article’s authors. Its separate roadmap proposes working through the Nix ecosystem by dependency relationships, including glibc, OpenSSL and cURL.

Anthropic describes generic binary specifications as a way to verify existing code without rewriting whole codebases in another language. Its proposed package-level reuse would let dependent programs build on verified packages. The source’s rationale is that dependencies follow a power law, so a relatively small set of shared libraries supports a broad body of software. This remains a roadmap rather than a property of all current proofs.

Wallach contrasted the project with Kaashoek and Zeldovich’s xv6 operating-system verification work using MachCSL, a logic for reasoning about concurrent programs and separately owned memory. That work deliberately designed the logic; Wallach described the Anthropic/Theorem effort as more automated, with agents developing and sharing reasoning techniques. Existing OSS-Fuzz tests had already supplied properties that could become theorems.

His source-contract proposal names Verus, Aeneas and Frama-C as possible tools for carrying learned requirements into maintained code. He also paraphrases a compiler-correctness point: extracting a machine-level correctness proof is more straightforward when the compiler itself is proved correct, and harder when it is not. His proposal retains the goal of machine-level proofs while seeking a development process that can preserve those guarantees through change.

Sources

Four sources, with attribution

OfficialLLMs are making formal software verification feasible at a much larger scale

Anthropic Research · 2026-10-22 · Frontier Red Team and Theorem. Methods, results, bugs, limitations and footnotes.

OfficialTechnical appendix (6 pages)

Exact theorem definitions, proof scale, expert assessment, reduced tasks, assertion examples and the Python interpreter experiment.

OfficialTheorem proof repository · archived v2026.10.0 README

60 entry points / 25 libraries; release versions, memory budgets, scope and statement counts. Archived 2026-10-26.

Third-partyDan Wallach’s commentary

Rice University professor researching computer security · 2026-10-23. Bug-finding value, maintenance concerns and suggestions for source-level contracts.