AI formal verification: Claude proves 123 libraries cannot crash, with limits

Anthropic says Claude can now prove, mechanically, that real open-source C and Rust libraries will not crash on any input up to 64 MB, across 123 libraries and 239 entry points. The company's Frontier Red Team published the work on October 22, 2026, with a startup called Theorem. It is a real step for AI-assisted formal verification, and the authors are careful to say what "verified" does not mean.

What Claude actually did

Fuzzing throws random inputs at a program and watches for crashes. Formal verification does something stronger: it proves, with a machine-checked argument, that no input in a defined set can cause the failure. It has been used for avionics, cryptography and a few operating system kernels, and it has been expensive. Anthropic's post says it "has historically required years of expert effort."

The pipeline in the post is specific. Claude converted existing fuzz tests from OSS-Fuzz into formal specifications, each stating that the test does not crash for any input under 64 MB. The specifications were checked against compiled RISC-V binaries, using Theorem's formal model of RISC-V and Linux process behavior. Claude wrote the proofs, and the Rocq proof checker verified them. When Claude found a real bug while attempting a proof, it patched the code, regenerated the specification and proved the new version.

That last step opens a door the authors name themselves: a model rewarded for proofs could patch the code to make the proof easier. They say they penalized and audited patches.

The numbers

The post reports 123 open-source libraries and 239 entry points. The proofs total about 180 million lines of Rocq, and a typical proof runs about 600,000 lines. The median binary is about 18,000 RISC-V instructions. Claude found hundreds of bugs while attempting proofs, including bugs a fuzzer was unlikely to find, and in one case a logic bug that had been latent for more than a decade.

Other figures: a Python interpreter written in Rust matched CPython's behavior in 99.95% of 1.7 million random programs, a PDF reader audit found as many security bugs in one week as are typically reported in a year, and reusing proofs across agents cut token use by 17%. On 36 verification tasks, Opus 5.5 used about 40% fewer tokens than Opus 5. The post also reports a proof of end-to-end zlib correctness against RFC 1950 at the x86 binary level.

All of these figures come from Anthropic's own write-up. No outside group has reproduced them yet, to our knowledge.

What the proofs do not cover

The caveats in the post matter more than the headline. The proofs are about single-threaded static RISC-V binaries linked against the musl C library, not the x86 or ARM builds with glibc that most people run. AddressSanitizer does not catch all memory-safety bugs. Not every entry point or library was verified, and a caller that misuses a function can still corrupt memory. Cost is also a barrier, since proofs can require hundreds of millions of tokens.

The authors say it plainly: "\"Formally verified\" does not mean \"bug-free.\"" A proof is only as good as the specification it checks. Here the specification is "does not crash," which is valuable and also narrow. It says nothing about whether the library returns the right answer, leaks secrets or can be tricked into doing something legal but harmful.

Where this fits

The work follows Anthropic's September 4 post, "Formalizing Fermat's Last Theorem," in which Claude, "working largely autonomously over 11 days," wrote a computer-checked proof in Lean of about 13 million lines. That post said the result was verification of a known proof rather than new mathematics. It also says Kevin Buzzard reviewed it and said it "proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics." Proof-checking is a task where an AI's output can be tested by a machine, which is why it is a natural place for models to look useful.

Theorem is a San Francisco startup that raised a $6 million seed round led by Khosla Ventures, VentureBeat reported on January 27, 2026. Co-founder Jason Gross said then: "Now that formal verification is cheap enough, it might be considered gross negligence to not use it." VentureBeat noted that the cost claim is the company's own and was not independently verified. The Anthropic post is the first public data point we have seen that tests it at the scale of 123 libraries, and it shows cost is falling but not yet small: hundreds of millions of tokens for a hard proof is real money.

The hype check

The strong claim is that AI will make software provably secure. The evidence supports a weaker and still useful one: a frontier model, a proof checker and a good formal model of the hardware can verify crash-freedom for real libraries and surface bugs along the way. The headline number of bugs found while trying to prove things is arguably the more durable result, since fixing those bugs helps whether or not any proof completes.

It also connects to the arms race in this week's security news. Models are getting better at finding exploits, a theme in our reports on open-weight cyber capability and the Anthropic cyber mission. Verification is the defensive counterpart: if attackers get cheap bug-finding, defenders need cheap proof.

What we would watch

Three tests would turn this from a promising report into a result. Independent reproduction on libraries Anthropic did not choose. Proofs on x86 or ARM builds that people actually deploy. And specifications richer than "does not crash." Until then, treat "formally verified by Claude" as a strong signal about memory safety on one architecture, and nothing more. Our position: this is one of the more credible security uses of a frontier model this year, because the output can be checked by a machine rather than trusted.