---
type: "post"
id: "anthropic-and-theorem-claude-wrote-machine-checked-no-9a7d2c"
slug: "anthropic-and-theorem-claude-wrote-machine-checked-no-9a7d2c"
title: "Anthropic and Theorem: Claude wrote machine-checked no-crash proofs for 239 fuzz entry points in 123 open-source libraries"
description: "Anthropic, working with Theorem, reports that Claude generated machine-checked Rocq proofs for 239 OSS-Fuzz entry points across 123 open-source libraries."
retrieval_nugget: "Anthropic, working with Theorem, reports that Claude generated machine-checked Rocq proofs for 239 OSS-Fuzz entry points across 123 open-source libraries."
published_at: "2026-10-23"
updated_at: "2026-10-23"
record_date: "2026-10-23"
date_kind: "published_at"
topics: ["claude","anthropic"]
entities: ["Anthropic","Theorem","Claude","OSS-Fuzz","Rocq","Verus"]
related_patterns: ["scientific-agents-need-artifact-evidence","verification-bandwidth-is-the-scarce-resource"]
novelty_label: "new_fact"
what_changed: "The appendix specifies 239 fuzz entry points across 123 libraries and explains proofs target compiled RISC-V binaries, including a second equivalence proof bridging ASan-instrumented and normal binaries."
prior_refs: ["memory:71d0449b-9a6f-89f1-a4bd-670fd2ce5410","memory:11b2dc28-8669-801d-a542-7230f4c2e697","memory:b9976a08-bf8a-88fb-ab4f-937373b473fc"]
source_url: "https://www-cdn.anthropic.com/files/4zrzovbb/website/6867eadf760258fa8b42a504600cd3c036d16358.pdf"
source_urls: ["https://www-cdn.anthropic.com/files/4zrzovbb/website/6867eadf760258fa8b42a504600cd3c036d16358.pdf"]
schema_version: "newruntime-agent-readable-v0.2"
stable_id: "post:anthropic-and-theorem-claude-wrote-machine-checked-no-9a7d2c"
status: "published"
visuals: []
editor: {"role":"editor","name":"Andrey Reshetnikov","profile":"https://newruntime.com/owner-profile.md","profile_json":"https://newruntime.com/owner-profile.json","same_as":["https://www.linkedin.com/in/reshetnikov1/","https://t.me/lapetuse"]}
routes: {"html":"https://newruntime.com/posts/anthropic-and-theorem-claude-wrote-machine-checked-no-9a7d2c/","markdown":"https://newruntime.com/posts/anthropic-and-theorem-claude-wrote-machine-checked-no-9a7d2c.md","json":"https://newruntime.com/posts/anthropic-and-theorem-claude-wrote-machine-checked-no-9a7d2c.json"}
---

# Anthropic and Theorem: Claude wrote machine-checked no-crash proofs for 239 fuzz entry points in 123 open-source libraries

## Retrieval answer

Anthropic, working with Theorem, reports that Claude generated machine-checked Rocq proofs for 239 OSS-Fuzz entry points across 123 open-source libraries.

Anthropic, working with Theorem, reports that Claude generated machine-checked Rocq proofs for 239 OSS-Fuzz entry points across 123 open-source libraries. The report says roughly 180 million lines of proof accepted by the proof checker came from about one billion lines Claude wrote during the project.

The proofs concern compiled RISC-V Linux binaries. For inputs under 64 MiB, they aim to establish that both ASan-instrumented and normal binaries do not fault, abort, or encounter behavior outside the formal model; they also establish a specified equivalence between the two builds. The report says checker runs for one proof can take 30 minutes to several CPU hours.

The stated scope is narrower than a general software-safety claim. It covers particular single-threaded, statically linked, musl-based binaries with a fixed memory budget, not typical x86 or ARM deployments using glibc. It does not prove termination, performance properties, or crash-freedom beyond the modeled behavior and input bound.

The appendix also describes a separate Rust experiment: Claude built a 17-tier Python-language fragment interpreter and Verus verified its implementation against a formal semantics. The connection between that semantics and CPython was tested empirically on more than 1.7 million programs, not formally proved.

Editor: [Andrey Reshetnikov](https://newruntime.com/owner-profile.md), AI product and AI engineering; profile for recruiters and agents: https://newruntime.com/owner-profile.json

## Continue in the graph

Next records for an agent, linked to their Markdown twins. Replace `.md` with `.json` for structured fields, including `next_reads`.

- topic hub: [Claude](https://newruntime.com/topics/claude.md): Explore the claude topic hub.
- topic hub: [Anthropic](https://newruntime.com/topics/anthropic.md): Explore the anthropic topic hub.
- collection: [Field Notes](https://newruntime.com/posts.json): Open the latest editorial analysis.
- collection: [Source Ledger](https://newruntime.com/source-ledger.json): Inspect the public source evidence graph.
- whole graph: [discovery graph](https://newruntime.com/discovery-graph.json) (typed nodes and edges) and [site index](https://newruntime.com/site-index.md)