Formal verification has always been the thing everyone agrees is worthwhile and nobody can afford. Anthropic and a startup called Theorem just made a serious dent in that, and the numbers are absurd in the best way: Claude wrote and proved formal guarantees for 239 fuzz-test entry points across 123 open-source libraries from OSS-Fuzz, at the RISC-V assembly level, in a few weeks. The verified proofs total about 180 million lines of Rocq.
For scale: a typical proof runs to about 600,000 lines, for a median binary of 18,000 RISC-V instructions. Anthropic’s total attempts came to around a billion lines of proof text, of which 180 million passed the proof checker. Machine-generated proofs are verbose. That is fine. Verbosity is what the checker is for.
The trick is the spec, not the prover
The hard part of formal verification was never proving things. It was writing the specification. Get the spec wrong and you have proven something irrelevant, expensively. Teams like the seL4 project spent 20 person-years verifying a kernel that took 2 person-years to write, which is why machine-checked proofs stayed confined to avionics and kernel microkernels.
Anthropic’s pipeline sidesteps the problem by converting existing fuzz tests into formal properties. Each OSS-Fuzz test becomes the machine-checked claim “this test suite always passes, for every input under 64 MB, for every modeled Linux OS response and memory layout”. No human writes a spec, no human reviews 180 million lines. The trust base shrinks to three artifacts: the formal models of RISC-V and Linux processes, the theorem statements themselves, and the Rocq proof checker. Everything else is mechanically verified against those.
This is, per Anthropic, the first large-scale effort to apply formal verification to production software at the assembly-code level using AI. The phrase “to its knowledge” is doing appropriate work there, but nobody else has published anything comparable.
What the proofs actually found
Proving properties is not just paperwork. The pipeline found bugs that fuzzers miss, because real fuzzers cap inputs at around 1 MB and the proof held for inputs up to 64 MB. Examples from the run: a counter underflow that causes an out-of-bounds write only on inputs near 20 MB with a rare memory layout, an out-of-bounds read that needs both a 64 MB input and over 2 GB of memory, and a rediscovery of CVE-2026-56132 in libexpat. During verification of a widely used PDF reader, the team found as many security bugs in one week as typically get reported in a year, including a logic bug that had been sitting in the code for over a decade.
Claude was allowed to patch bugs it found and re-prove the patched code, and Anthropic penalized and audited patches specifically to discourage reward hacking, meaning rewriting the program so trivially that it never crashes. That anti-gaming discipline matters if you are going to trust the pipeline.
Side quests that would be headlines on their own
The appendix of the technical report is where things get strange. Claude generated formal semantics for the x86 instruction set autonomously. The resulting semantics could boot an Ubuntu userspace single-stepped on a simulated Linux kernel, and producing them surfaced hundreds of mistakes in the official x86 reference documentation, plus a small number of apparent hardware bugs. Claude also wrote a formal spec of the zlib format and verified the Linux kernel’s zlib implementation at the x86 binary level against it. In a separate experiment, Claude built a Python interpreter in safe Rust and proved it with Verus; running 1.7 million randomly generated Python programs against it matched CPython behavior 99.95 percent of the time.
None of these are production results. All of them are previews of a workflow where an LLM writes the semantics, writes the code, and machine-checks the guarantee, with humans reviewing the spec rather than the code.
The cost problem, and its slope
The bottleneck is tokens. Proofs can consume hundreds of millions of them. But the direction is favorable: on 36 small verification tasks drawn from real OSS-Fuzz code, Opus 5.5 proved half of them while using about 40 percent fewer tokens than Opus 5. Proof reuse helps too. Agents sharing a workspace spent 17 percent fewer tokens, mostly by copying and adapting each other’s completed proofs across similar libraries.
Compare that trajectory with the status quo, where verification of anything meaningful costs person-years. Fuzzing went from research curiosity to table stakes because per-target cost collapsed. This looks like the same curve starting from a higher point.
Read the fine print
Before anyone declares fuzzing dead: the guarantees here are conditional. The proofs cover single-threaded, statically linked RISC-V binaries against musl libc. Most real deployments run x86 or ARM with dynamically linked glibc, and threading is entirely outside the model. “Formally verified” means the spec matched the modeled machine, and it does not mean bug-free. Anthropic is explicit about this, which is more than can be said for most coverage of formal methods.
Still, the artifacts are real and public. A subset of the proofs, the RISC-V and Linux Rocq semantics, and a Claude skill are published. Theorem is offering to run the same pipeline for other projects, with a roadmap to verify the Nix ecosystem’s core libraries, including glibc, OpenSSL and cURL. If you maintain C or C++ code with fuzz tests, the practical move is to treat those tests as future proofs and keep them clean: the pipeline converts whatever crash semantics they express directly into formal claims.
The security industry has spent thirty years getting better at finding bugs. This is a credible step toward proving their absence instead, and it costs tokens rather than person-years. That trade is new.