# Anthropic Says Claude Formally Verified 123 Open-Source Libraries at the Assembly Level

The machine-checked proofs total about 180 million lines of Rocq, cover 239 fuzzing entry points, and came with patches for bugs that trillions of fuzz runs had missed.

- Published: 2026-10-23T06:19:29.884Z
- Canonical: https://polylog.news/ai/2026-10-23/anthropic-says-claude-formally-verified-123-open-source-libr
- Publisher: Polylog (AI desk)
- Section: tech
- Sources: [Anthropic Frontier Red Team (via Hacker News)](https://www.anthropic.com/research/formal-verification), [Unite.AI](https://www.unite.ai/anthropic-says-claude-proved-security-properties-across-123-libraries/), [Interesting Engineering](https://interestingengineering.com/ai-robotics/claude-formal-verification-software-security)

Anthropic's Frontier Red Team [published research on October 22](https://www.anthropic.com/research/formal-verification) saying Claude produced machine-checked proofs of security properties for 239 fuzz-test entry points across 123 open-source libraries. Anthropic did the work with Theorem, a formal-methods startup. The proofs target compiled RISC-V binaries, not source code. They show that each program exits normally without a memory-safety error or a failed assertion for every input under 64 MB and for every modeled Linux system-call response and memory layout, [according to Unite.AI's account of the post](https://www.unite.ai/anthropic-says-claude-proved-security-properties-across-123-libraries/).

The workflow ran in a loop. When a proof attempt failed, Claude found the bug behind the failure, patched it, and then proved the patched binary. [Interesting Engineering reports](https://interestingengineering.com/ai-robotics/claude-formal-verification-software-security) that some of these flaws had gone undetected for years despite the targets having been through trillions of automated fuzzing runs. The output is large. The proofs come to about 180 million lines of Rocq, the proof assistant formerly called Coq. A typical proof runs about 600,000 lines and covers a binary with a median length of 18,000 RISC-V instructions. Anthropic says the full effort took a few weeks. It describes the project as, to its knowledge, the first large-scale use of AI to apply formal verification to production software at the assembly level. That claim of a first comes from Anthropic, and no independent party has checked it.

The method's strengths and its limits are both worth noting. A Rocq proof checks itself, so the kernel does not have to trust the model that wrote it. That is a stronger guarantee than a vendor-reported score on any agentic coding benchmark. The guarantee is limited by the specification and the environment model, however. The proofs cover a fixed property (normal exit, no memory errors, no failed assertions), an input bound, and a modeled operating system. They do not prove functional correctness, and they say nothing about behavior the model of Linux leaves out. The entry points are fuzzing harnesses, so the verified surface is the surface the harnesses already exercised. Reviewers outside Anthropic have not yet audited the trusted base, meaning the RISC-V semantics and the system-call model.

The result changes the economics of a technique the industry has largely been unable to afford. Before this, formal verification at the binary level was limited to small, expensive projects with expert teams, such as seL4 and CompCert. Anthropic's claim is that the binding constraint is now tokens and compute, not proof engineers.

## What this means

The mechanism is cost. If a frontier model can write proofs that a small kernel checks, then software assurance becomes a matter of compute spend, not of how many specialists a team can hire. Exposure runs in two directions. Sellers of fuzzing and static analysis lose their claim to the best available guarantee. Model vendors gain a use case where the output can be checked outright, which is what buyers in critical infrastructure and defense want. The market already expects AI to find bugs. Proofs that cover all inputs within a bound are the new part. The consensus may be wrong to read this as a capability headline, because the limiting factor shifts to the specification and the environment model, and those still need human experts. The closest precedent is seL4's machine-checked kernel proof in 2009, which took about 20 person-years and stayed a niche product for a decade. The likelier outcome is that within months other labs and security vendors publish similar proof campaigns on widely used C libraries, and regulated buyers begin asking for machine-checked memory-safety evidence in procurement. That depends on outside reviewers confirming that the trusted base is sound. A published flaw in the RISC-V semantics or the system-call model that invalidates a large share of the proofs would prove this read wrong.

## What to watch

- Whether Anthropic and Theorem publish the proof artifacts and the environment model so outside teams can replay the Rocq checks. Open artifacts would turn a vendor claim into a result anyone can check.
- Whether OpenAI or Google DeepMind answer with a verification campaign of their own. That would show checkable assurance becoming a contested product category.
- Whether maintainers of the affected libraries confirm the patched bugs and assign them vulnerability identifiers. Confirmation would show the proof failures caught real, exploitable defects.