What Anthropic's AI Proofs Mean for Formal Verification

Claude has found and patched hundreds of bugs in open-source libraries, including some that had gone unnoticed for years despite trillions of fuzzing runs. It found them by trying to formally verify the code.

In a report published on October 22, Anthropic’s Frontier Red Team and Theorem describe how, over a few weeks, Claude produced machine-checked proofs that 239 fuzz-test entry points across 123 libraries never crash on any input under 64 MB, reasoning directly about the compiled RISC-V binaries in a modeled Linux environment. Formal verification means proving mathematically that a program satisfies a stated property for all inputs in its scope, rather than testing the inputs someone thought to try. Such proofs are often considered prohibitively expensive and worth it only for extremely important mission-critical code. However, as AI code generation becomes cheaper, proving formal properties becomes feasible and achievable for a much wider class of applications.

At Serokell, we work close to this field: our GHC team has spent years bringing dependent types to Haskell, and we have published a series on constructive and non-constructive proofs in Agda. It’s a good moment to review the current development and its possible implications for the future.

Generated proofs are different from generated code

LLMs are often critiqued for ‘slop generation’: badly structured, overengineered code that is hard to follow and hard to maintain. In order to fix these issues, a human-in-the-loop concept is still very important: a human reviews the output and fixes LLM code quality issues. That work may take a lot of effort, comparable with code development from scratch, if taken seriously.
Generating proofs is different. Proofs are objects for which only existence matters. If they are formally correct and the compiler (or proof verifier) successfully checks them at compile-time, then they’re good enough.

What Claude actually proved

• For OSS-Fuzz libraries, specifications were generated mechanically from existing fuzz tests: the entry point must not crash on inputs under 64 MB (a parameter of the spec that, according to Anthropic, can be raised with trivial effort) in the modeled RISC-V/Linux environment. The guarantee is only as strong as the test. A no-crash proof isn’t proof of functional correctness, but a failed assertion counts as a crash, so tests that assert functional properties carry them into the proof. LZO’s compression fuzz test asserts that compression succeeds and, when the compressed output is smaller than the input, that decompression succeeds and returns as many bytes as the input had.
• The proofs also have two clear limits. They cover only code reachable from the entry point, and the machine model is narrower than real deployments: the proofs assume single-threaded static RISC-V binaries linked against musl, while most people run these libraries on x86 or ARM with glibc.
• In the zlib experiment, Claude generated a formal specification of RFC 1950 and proved that the Linux kernel’s zlib implementation satisfies it, using an x86 machine model that Claude also generated. Anthropic tested that model by using it to boot an Ubuntu userspace, which is a strong check but not a proof that it matches real hardware.

What gets cheaper, and what remains expensive

‘Debugging is twice as hard as writing the code in the first place. Therefore, if you write the code as cleverly as possible, you are, by definition, not smart enough to debug it.’ – Kernighan’s law

Let’s start with a rough estimate to see the progress here. It’s very hard to give an exact estimate of code verification complexity (compared with code development complexity); folklore gives a factor of 10. The report references seL4, which provides a comparable number (a factor of 9, but some part of the verification work was spent on tooling).
Claude-assisted verification is much cheaper, but still not cheap: tests convert mechanically and LLMs draft the rest, but the drafts still need checking, and the report still describes some human involvement. Anthropic itself expects formal verification to become as practical as fuzzing for almost all production software. So, we may be seeing a shift from “prohibitively expensive” to simply “expensive”, and this may become affordable for many applications.
However, as proofs become cheaper, the value of proper specifications grows, despite some limited progress — and the report indirectly backs this claim.

• The fuzz tests for OSS-Fuzz libraries were written by human developers; the specifications were derived from them mechanically — and formal proof of fuzz tests is not the best idea in general, since they check only what their assertions express, only for inputs within the size bound, and only the code their entry points reach.
• Claude translated the RFC 1950 spec into a machine-checkable formal specification — but the original spec was developed by software engineers.
• An automatically developed specification is not itself verified, and may inherit the same problems as the code being developed. The generated specification may lack knowledge about human motivation; it can easily become verbose, dense and difficult for humans to review.

As it looks now, the only real producer for the specs is the customer (the human), who decides what they want to build and how their prompts should be interpreted.

Where we can get from here

If LLMs really can produce formal proofs cheaply, a few directions open up.

• Specifications are the core component here, and some iterative process is expected (specs developed, code produced, then specs altered and the loop continues). Moreover, improper specifications can pose big security risks (imagine a backdoor attack through CPU spec manipulation). The process of spec building did not start today, and it will grow: see, for example, Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents.
• Use of Rocq or some other separate formal engine is not always the best choice. If the code is originally developed in some other language (which is usually the case), this language gap would bring additional effort, like verified conversion between languages or machine-code proofs.
  We definitely need better tooling for this. For example, JetBrains is working on the SnaKt plugin for Kotlin, which should let developers write specifications alongside Kotlin code and verify them through Viper. And this is not the only direction (dependent types in Haskell can be viewed as such at an early stage).
• The process of software development with possible on-the-spot formal verification of code pieces can change dramatically: when an engineer specifies a formal requirement instead of a prompt, the LLM generates code and a proof, and an independent checker verifies that the proof establishes the specified property under the modeled assumptions.

Proofs are getting cheaper. And now the task of specifying what we actually want from the software becomes more and more important and visible, and that is where most of the work now lies.