← Back to feed

Formal software verification has been the domain of aircraft and critical infrastructure — the cost of 20 person-years to verify a microkernel kept it out of reach for ordinary software. A new paper from Anthropic and Theorem.dev argues that barrier is gone.

Using Claude, the team proved security properties across 123 open-source libraries at the RISC-V assembly code level. Anthropic describes this as the first large-scale effort to apply AI to formal verification of production software at assembly level.

What Claude Actually Proved

The scope is specific: Claude produced proofs that target programs will always exit normally — no memory-safety errors, no failed assertions — for every input under 64 MB, every modeled Linux OS response, and every memory layout, under a constrained execution model: single-threaded static binary, fixed memory budget, RISC-V CPU.

The constraints matter. They define what the proofs cover. Proofs under these conditions are still meaningful — they cover the attack surface of inputs that real software processes in production.

While writing those proofs, Claude found bugs that had persisted despite prior fuzzing at the scale of trillions of test runs. Formal verification found what statistical testing missed: edge cases that are reachable in theory but vanishingly rare in practice.

Why Assembly Level Is Harder

Most formal verification work targets source code. Assembly-level verification has to reason about the actual machine instructions — compiler outputs, memory layout, system call boundaries — rather than the programmer’s intent. The gap matters because bugs can exist in code that looks correct at the source level but breaks guarantees at the compiled, executing level.

The seL4 microkernel verification benchmark is illustrative: the implementation took two person-years; the formal proof took 20. Claude is doing something analogous, autonomously, across 123 libraries.

The Security Threat Model Behind This

Anthropic’s framing is pointed. LLMs can already find bugs at scale — including their own research on chaining low-severity bugs into critical exploits. The Linux kernel had over 1,000 vulnerabilities disclosed in a recent period. The offensive capability of frontier models is outpacing patch velocity.

Formal verification offers a different kind of defense: not finding bugs but proving their absence, within the scope of the proof. It cannot cover everything, but it removes entire classes of vulnerability from specific code paths.

The collaboration with Theorem.dev, a formal methods startup, suggests Anthropic is treating this as infrastructure work, not a one-off benchmark.

Limits

Anthropic is explicit about assumptions: single-threaded execution, static linking, fixed memory budget, RISC-V. Real software is multi-threaded, dynamically linked, and runs on x86. The proofs cover important ground, but not all ground.

Scaling to cover more realistic execution environments — multi-threading, dynamic linking, x86-64 — is the next problem. Whether Claude can handle that complexity is an open question.