News · 2026-10-23

Anthropic and Theorem report machine-checked proofs for 239 software entry points

Anthropic and Theorem used Claude to generate machine-checked proofs for 239 software test entry points across 123 open-source libraries. The October 22 announcement shows AI taking on substantial proof-writing work while a separate checker validates the resulting logic. The guarantees concern specified failures in particular compiled programs under explicit assumptions, rather than entire libraries being free of bugs.

Key facts

• Anthropic reports coverage of 239 fuzz-test entry points across 123 libraries.
• The crash guarantees cover inputs under 64 MiB within the modeled environment and resource limits.
• Claude writes proof material; the Rocq proof checker checks it against the formal specification.
• Primary source: Anthropic’s October 22 research announcement.

Testing searches for failures by running examples. Formal verification tries to establish that a stated property holds for every case inside a defined domain. The difference is like driving a bridge’s busiest vehicles across it versus proving a structural property under specified loads. The proof can be stronger than the test while still depending on whether the loads, materials and structure in the model match the real bridge.

Anthropic’s project begins with existing fuzz tests, programs that exercise library code on many unusual inputs. Those test programs already contain a partial specification: they identify an entry point, drive a particular sequence of operations and sometimes assert properties that must hold. The AI-assisted effort turns those expectations into claims a proof system can check. A missing assertion remains a missing requirement; proof generation does not automatically discover everything users intended.

The work targets compiled RISC-V programs. RISC-V is a processor instruction set, and Theorem helped construct formal descriptions of those instructions and Linux process behavior. Proving a claim about the compiled instructions avoids relying solely on a translation of source code into a proof language. It moves attention to another trust boundary: the accuracy of the processor and operating-system models. The semantics repository exposes part of that machinery for inspection.

Claude proposes the proof. Rocq checks whether the proof follows from the specification and allowed logical rules. This division is central. Readers do not need to accept an AI’s confident explanation as proof, because a separate program checks the argument. They still need to ask whether the theorem describes the desired behavior and whether the modeled environment describes the deployment. Ground Truth’s proof-assistant lesson explains this difference between generating a convincing argument and checking a formal one.

Anthropic makes the boundary unusually explicit: “formally verified” does not mean “bug-free.” A covered entry point can have a guarantee against certain crashes without establishing correct answers, freedom from memory leaks or eventual termination. Uncovered entry points remain outside the result. Real deployments often differ through processor choice, dynamic linking, concurrency, memory layout or resource budgets.

The effort also found bugs while trying to prove their absence. Anthropic describes failures requiring large or unusual inputs, as well as logic errors that did not crash. Such cases illustrate how proof construction can force attention onto conditions ordinary testing rarely reaches. The company says Claude patched bugs during the process and then proved the patched builds against regenerated specifications. That is an account of the proof workflow, rather than confirmation that every resulting patch entered an upstream release.

One concrete upstream record is libexpat pull request 1272, which attributes a report to Anthropic and Trail of Bits and shows a June 20 fix. Anthropic calls the issue a rediscovery. The record supports that attribution and merge date; it does not show this October campaign originated the earlier report.

The public artifacts also need a denominator. The published proof repository examined for the dossier lists 60 entry points across 25 libraries, rather than the full reported campaign. It is valuable inspectable evidence, but readers should not mistake the released subset for all 239 proofs.

Cost is an unresolved practical question. Anthropic says the main effort ran over weeks and could consume hundreds of millions of model tokens; checking a proof can take from half an hour to several hours of processor time. It does not provide a per-library price. The appendix’s expert assessment raises a scaling concern about very verbose proofs and the need for better reusable abstractions. The dossier verified that appendix in one pass; a later pass could not reopen it, so the main announcement and public artifacts carry the central claims here.

The useful result is a larger role for AI in producing work that can be checked independently. The strongest counterargument concerns coverage and economics: a technically sound proof of a narrow property may be expensive and still leave the most important deployment behavior unproved. Evaluating this approach means inspecting the theorem, build and trusted models alongside the headline number of libraries.

Primary source, verified: read the paper →

Ground Truth. (2026, October 23). Anthropic and Theorem report machine-checked proofs for 239 software entry points. Ground Truth. https://groundtruth.day/news/anthropic-theorem-prove-properties-of-239-fuzz-entry-points.html

@misc{groundtruth:anthropic-theorem-prove-properties-of-239-fuzz-entry-points,
  title  = {Anthropic and Theorem report machine-checked proofs for 239 software entry points},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {oct},
  url    = {https://groundtruth.day/news/anthropic-theorem-prove-properties-of-239-fuzz-entry-points.html}
}

Topics: formal-verification · software · anthropic · coding · research