---
id: "2026-10-22-anthropic-formal-verification-oss-fuzz-rocq"
url: "https://postcutoff.com/e/2026-10-22-anthropic-formal-verification-oss-fuzz-rocq/"
as_of: "2026-10-23T13:24:00+02:00"
date: "2026-10-22"
date_precision: day
category: research
importance: 4
confidence: high
status: [Confirmed]
sources: 3
editor: human editor
human_review: null
version: null
---

As of: 2026-10-23 13:24 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-22-anthropic-formal-verification-oss-fuzz-rocq/

# Claude formally verifies 123 open-source libraries

Full title: Anthropic's Frontier Red Team uses Claude to write ~180M lines of machine-checked Rocq proofs: no-crash guarantees for 239 OSS-Fuzz entry points in 123 open-source libraries

On Oct 22, 2026 Anthropic's Frontier Red Team, working with the verification startup Theorem, reported that Claude wrote machine-checked proofs that 239 OSS-Fuzz fuzz-test entry points across 123 open-source libraries cannot crash (under AddressSanitizer) on any input up to 64 MB. The proofs are about compiled RISC-V binaries, total about 180 million lines of Rocq (about 600,000 lines for a typical proof), and took "a few weeks". On the way Claude surfaced hundreds of bugs. Anthropic argues formal verification "will soon be as practical as fuzzing is today for almost all production software", while warning that "formally verified" does not mean "bug-free".

## Key facts
- Authors (Anthropic Frontier Red Team): Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal, Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich, Nicholas Carlini, Rajashree Agrawal and Jason Gross; collaborator Theorem, which offers to run the pipeline on other open-source projects and published a Claude skill for it
- Main result: no-crash proofs for 239 fuzz entry points in 123 libraries from Google's OSS-Fuzz, at the level of compiled RISC-V binaries (median ~18,000 instructions), for inputs under 64 MB; assumptions: single-threaded static binaries, fixed memory budget, RISC-V, Linux with musl libc
- Scale: ~180 million lines of Rocq in total, a typical proof ~600,000 lines; proofs can take hundreds of millions of tokens; whole effort 'a few weeks' (Anthropic contrasts seL4: ~2 person-years to implement, ~20 to verify)
- Bugs: hundreds surfaced, e.g. a decompressor counter underflow causing an out-of-bounds write only on ~20 MB inputs with one rare layout; an image-decoder out-of-bounds read needing a 64 MB input and 2 GB+ memory; a rediscovery of CVE-2026-56132 in libexpat; a logic bug latent for over a decade; a review of a widely used PDF reader found as many security bugs in one week as are typically reported in a year
- Other case studies: the Linux kernel's zlib proven against a spec written from RFC 1950 at the x86 binary level; a Claude-written Rust interpreter for a Python subset proven (Verus) to follow CPython semantics, matching CPython on 99.95% of 1.7M random programs
- Model efficiency: on 36 small verification tasks Opus 5.5 needed ~40% fewer tokens than Opus 5 to prove half of them; sharing proofs in a common workspace cut tokens by 17%
- Reward hacking: Claude could make a proof go through by rewriting code so it never crashes; the team penalised patches, required proofs of how much patches changed behaviour, and audited them
- Limitations stated: specs may not match the real machine; RISC-V/musl differs from the x86/ARM, glibc, dynamically linked builds most people run; ASan does not catch every memory-safety bug; dead code and unverified entry points are not covered; callers can still misuse libraries; the trusted base includes Rocq, the RISC-V and Linux semantics, hardware and the OCaml compiler
- Reach: @AnthropicAI post ~1.05M views (fxtwitter, Oct 23); Hacker News 354 points

## What happened

Anthropic's Frontier Red Team published a research post on Oct 22 showing Claude producing formal proofs at industrial scale. The
setup: for each OSS-Fuzz harness, Claude writes a proof in the Rocq proof assistant that the compiled RISC-V binary never triggers an
AddressSanitizer crash on any input below 64 MB; Rocq's kernel checks the proof against a specification built on Theorem's formal
semantics of RISC-V instructions and Linux processes. "Claude writes the proof; the Rocq kernel checks it against the specification."
Where a proof failed, the counterexample often was a real bug, so the fuzz-to-proof pipeline doubled as a bug finder. The post adds
smaller case studies (the kernel's zlib at the x86 binary level, a verified Python-subset interpreter, simple security properties of a
PDF reader) and a token-efficiency benchmark across Opus 5, Opus 5.5 and Fable 5.1.

## Why it matters

It arrived a day after PHP2Shell showed AI-found bugs in core internet software can be exploited within days of disclosure. Anthropic's
answer is that the same models can make proofs of absence of whole bug classes cheap: work that took ~20 person-years for seL4 was done
for 123 libraries in weeks. The caveats are real (narrow property, RISC-V/musl builds, trusted base), but this is the largest
machine-checked verification effort reported so far, and it points defence toward proofs rather than only faster patching.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 175 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 114 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 205 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 144 days after its cutoff

## Sources

1. [Anthropic: LLMs are making formal software verification feasible at a much larger scale (Oct 22, 2026)](https://www.anthropic.com/research/formal-verification) (anthropic.com, official)
2. [Anthropic on X: using Claude to formally verify software at large scale](https://x.com/AnthropicAI/status/2113390212911083894) (x.com, official)
3. [Hacker News discussion (354 points)](https://news.ycombinator.com/item?id=50202217) (news.ycombinator.com, discussion)

## Changes

- 2026-10-23 (filed): Created (HN, Google News)

## Related

- 2026-10-21: [PHP2Shell: critical remote-code-execution flaws in PHP, found with GPT-5.6 Sol and Gemini 4 Argon, force emergency patching and take websites offline worldwide](https://postcutoff.com/e/2026-10-21-php2shell-ai-found-php-rce/index.md)
- 2026-10-21: [Claude Security adds continuous scanning](https://postcutoff.com/e/2026-10-21-claude-security-continuous-scanning/index.md)
- 2026-10-20: [Anthropic: Claude flags 493 attack-surface issues in 25 open-source projects](https://postcutoff.com/e/2026-10-20-anthropic-claude-attack-surface-reduction/index.md)
- People: [Nicholas Carlini](https://postcutoff.com/person/nicholas-carlini/)
- Archived: 1 post, listed in https://postcutoff.com/e/2026-10-22-anthropic-formal-verification-oss-fuzz-rocq/index.json