Anthropic and Theorem report that Claude generated machine-checked proofs for 239 test entry points across 123 open-source libraries. The result is a concrete use for coding agents: generating a mathematical argument that a separate checker can accept or reject.

The guarantee is narrower than the headline’s promise of secure software. It concerns particular compiled programs, selected properties and a modeled machine. The accompanying artifacts make those boundaries worth examining.

Turning a test into a theorem

Fuzzing runs generated inputs through a program to look for failures. A fuzz entry point is the small driver that feeds those inputs into library code. Existing assertions can check meaningful behavior, such as whether compression followed by decompression returns the original data.

The researchers compiled these drivers and their libraries into RISC-V binaries, programs for a particular processor architecture. They then asked Claude to prove that the binaries avoid specified failures for every input below 64 MiB, within the modeled environment.

Rocq, a formal proof checker, checks the resulting argument. Trust moves from the agent’s confidence to the exact theorem, the checker and the model of the machine.

  • The main experiment covers single-threaded, statically linked RISC-V Linux binaries using musl, a C runtime library, with fixed memory budgets.
  • AddressSanitizer, a tool that detects memory errors during execution, adds failure checks. Separate equivalence proofs connect instrumented and ordinary binaries.
  • The team reports about 180 million lines of successful proof artifacts. Its appendix says more than half of a typical proof is machine-emitted data from tools the agents wrote.
  • Verification attempts also found bugs, including failures requiring unusually large or specially structured inputs that ordinary fuzzing might miss.

The release is smaller than the reported experiment

The public proof repository currently describes proofs for 60 entry points in 25 libraries. That is a released subset, distinct from the 239-entry-point research claim. Anthropic says it withholds proofs that could expose unpatched vulnerabilities.

The repository documents pinned binaries, theorem statements and a checking procedure. The Linux process model explicitly calls itself incomplete and lists assumptions. Those disclosures matter as much as the volume of generated proof code.

Patching can change what gets proved

When Claude encountered a bug, it could patch the program and regenerate the specification. That creates an obvious shortcut: remove useful behavior until the program becomes easy to prove safe.

The researchers say they penalized patches, rewarded descriptions of changed inputs, and logged and audited the edits. Those controls address the risk, but a proof about the edited program still needs a separate account of whether the edit preserves intended behavior.

The technical appendix also questions how far the verbose proof style will scale. Better reusable abstractions may be necessary for more complex programs.

What carries over to deployed software

A proof about one RISC-V build does not automatically cover an x86 or ARM build, dynamic linking, concurrency or a different caller. Selected fuzz drivers leave other library behavior uncovered. AddressSanitizer also misses some memory errors.

Caveat: a checked proof establishes its stated property under its assumptions; it cannot establish that those assumptions capture every relevant feature of a deployed system.

Anthropic sells the model used here, and Theorem offers the verification pipeline. Their forecast that verification will become routine is a commercial research argument, not an independently established cost or adoption result. The reported token reductions on 36 smaller tasks do not supply an end-to-end production cost.

What the discussion adds

In the Hacker News discussion, jaykru highlights the appendix’s concern about scaling verbose proofs. malisper reports equivalence proofs covering roughly 70,000 lines of a Postgres rewrite under single-threaded assumptions. That is a separate practitioner’s self-report, with its own translation and specification risks.

The practical opportunity is a workflow with explicit claims and mechanically checked evidence. Choosing those claims, validating the machine model and reviewing behavior-changing patches remain engineering responsibilities.