AI Formal Verification: Claude Proved 123 Libraries Crash-Free

Anthropic published results on October 22, 2026 that put a number on a claim people have repeated for years: language models make formal verification cheap enough to use. Working with Theorem, Anthropic says Claude proved that 239 fuzz-test entry points across 123 open-source libraries never crash on any input under 64 MB, and found bugs that had survived trillions of fuzzing runs on the way. If you searched for "formal verification AI" this week, this is the post that moved the term.

Last updated: October 23, 2026

What Anthropic says it did#

Everything below is from Anthropic's write-up, and the numbers are Anthropic-reported, not independently reproduced.

• The spec is a fuzz test. Instead of writing a bespoke specification, the team took each library's existing OSS-Fuzz entry point and compiled it to a RISC-V binary. The spec is then "this test never crashes for any input under 64 MB", checked against formal models of RISC-V and Linux processes.
• Claude writes the proof, a checker accepts it. The proofs are written for the Rocq proof assistant, total about 180 million lines, and a typical one runs to about 600,000 lines. Virtually none of that needs human review, because the Rocq kernel checks it.
• Claude fixes bugs as it goes. When a proof attempt exposes a crash, Claude patches the code, the spec regenerates, and the proof continues. Anthropic notes the reward-hacking risk (rewriting the program so it trivially never crashes) and says it penalized broad patches and audited them.
• The bugs are the odd kind. Examples include a counter underflow in a decompressor that needed roughly 20 MB of input with one rare layout, an out-of-bounds read that needed a 64 MB input and over 2 GB of memory, and a rediscovery of CVE-2026-56132 in libexpat.
• Token cost is falling. On 36 small verification tasks from real OSS-Fuzz code, Anthropic reports Opus 5.5 solves half of them with about 40% fewer tokens than Opus 5. When agents could copy each other's proofs from a shared workspace, they used 17% fewer tokens than agents working alone.

Anthropic is publishing a subset of the proofs and the RISC-V and Linux semantics so others can check them.

What "verified" does and does not mean#

The post is unusually candid here, and the limits matter more than the headline. Anthropic states that "formally verified" does not mean "bug-free". The proofs assume a single-threaded, statically linked RISC-V binary with a fixed memory budget on Linux, while most people run these libraries on x86 or ARM with dynamic linking. They cover the entry points that were verified, not the whole library, and a caller can still misuse the library and corrupt memory on its own side. What you have to trust is the RISC-V and Linux models, the exact theorem statements, and the Rocq checker.

That is still a real shift. Auditing three small trusted components is a different job from auditing every line of the code they cover. It is also the reason I would not read this as "AI proved these libraries secure". Read it as "a no-crash property is now provable at scale for code with a good fuzz harness".

The Monday angle: your fuzz target is now your spec#

The practical lesson is for maintainers and for anyone letting an agent write tests. Theorem's published add-project skill is the most concrete artifact in the release, and its rules for writing a proof-worthy fuzz target are good practice even if you never enroll:

1. Never use assert() for a property. The skill warns that many builds define NDEBUG, which removes every assert() silently. It tells you to write if (!condition) abort(); and put a comment above it saying what the check protects.
2. Show that every check runs. Build a small seed corpus and compile with coverage flags (-fprofile-instr-generate -fcoverage-mapping), then confirm each API call and property check has a count above zero.
3. Show that every property can fail. Make a one-line mutant that breaks it, find an input that trips the check, undo the change and record both in a comment. The skill's phrase is blunt: a property that no change can make fail checks nothing.
4. Depend only on the input. No threads, clocks, network or environment reads, and bound every loop and size that comes from the input.
5. Do not return -1 for a failed property. The skill explains that libFuzzer reads -1 as "do not keep this input", and the driver counts it as a pass, so a real failure would slip through.

If you use a coding agent to write tests, these five rules double as a review checklist for its output, in the same spirit as the tests-as-contract ideas in software factories fail without harness engineering. A weak harness makes a proof vacuous, and it makes an agent's "all tests pass" vacuous in the same way.

Maintainers who want the pipeline run on their project can follow the enrollment route. Note the skill's own constraints: it produces a pull request that the maintainer opens, only the maintainer can accept the terms, and the builder currently handles C, C++, Rust and Python projects.

Where this sits next to other AI proof work#

This is a different animal from the headline math results. Anthropic's Lean formalization of Fermat's Last Theorem and Leanstral's theorem-proving model are about mathematics in Lean. This release is about shipped binaries and security properties, and it lands alongside Anthropic's push on finding vulnerabilities in open source, covered in how to enroll in the OSS Scanner. Together they describe one pipeline: models find bugs, then models prove what remains. The cost of that second step is the part that bites maintainers, which is the same triage pressure described in the AI security triage bottleneck.

What people are actually saying#

The Hacker News thread hit 295 points and 162 comments within hours. It is skeptical in a useful way:

• The spec problem. The top objections ask how you know what was proved is what you wanted, and whether proving "never crashes" is much beyond what a fuzzer plus a fix already gives you. One commenter calls it closer to validation than end-to-end verification. This tracks Anthropic's own limitations section.
• The Lean precedent. Another commenter compares it to earlier AI-written Lean proofs where the formal statement did not match the prose claim, and warns the same gap can open here. That is a fair worry about theorem statements, which is why Anthropic lists them among the things a human must trust.
• Practitioners who tried it. One developer says they use a Rocq proof of behavioral equivalence to merge an agent-written SIMD optimization with confidence. Another reports translating C and Rust into Lean to prove equivalence for a Postgres rewrite, covering about 12% of the code so far. Both are self-reported single accounts, not benchmarks.
• A tooling prediction. Some expect agents to drift toward more declarative languages that are easier to verify. That is speculation in the thread, not evidence from the release.

The fair summary: strong on the engineering, honest about limits, and the open question is who writes and reviews the specs.

Continue Reading#

• Anthropic's Fermat proof is an autoformalization milestone - the Lean side of AI proof work
• Anthropic OSS Scanner: how to enroll - the bug-finding half of the same pipeline
• Leanstral 1.5 theorem proving model - an open model aimed at proofs
• The AI security triage bottleneck - who pays when models find more bugs than maintainers can read
• Software factories fail without harness engineering - why the test harness is the real product

Sources#

• Anthropic: LLMs are making formal software verification feasible at a much larger scale - October 22, 2026
• Theorem OSS Verify: add-project skill
• Published proofs (theorem-labs/oss-verify-proofs)
• Rocq Linux process semantics (theorem-labs)
• Hacker News discussion