Can Claude’s Formal Proofs Replace Tests for Your Service?

A verified dependency does not verify your entire service

Claude's formal-verification results are not a reason to delete a deployed service's tests. A proof concerns a particular executable under a particular statement and set of assumptions. Building the library differently or embedding it in an application creates questions that the original proof may not cover.

The October 22 research announcement from Anthropic and Theorem is significant within that boundary. Claude wrote proofs about open-source test entry points, and Rocq checked them. This supplies a machine-checkable argument rather than a model's assurance that code looks safe.

The adoption question is therefore concrete: does the proof cover the binary, environment and property you actually need?

Existing tests help define the property to prove

A fuzz target accepts generated inputs and exercises library code. Running more inputs can expose more failures, but it does not exhaust all possible inputs.

The research instead targets compiled RISC-V programs with formal statements covering the inputs within their assumptions. A condition encoded as a test failure can become a property to prove. As Theorem explains, the behavior a harness rejects matters: the test helps define what success means.

The execution environment also needs a mathematical description. The Linux Process Semantics model describes RISC-V program execution and observable behavior. A checked proof is meaningful relative to that model and its statement; checking the proof does not independently establish that the model captures every relevant detail of a real deployment.

The 123-library study is broader than the public release

The announcement and the public proof repository describe different scopes. As of October 26:

The last row is easy to miss. Excluding errors is different from proving that every execution eventually finishes. The repository explicitly says the release contains no proof of a halting statement. Reading it as “always terminates normally” would overstate the result.

Nor do these proofs exclude every wrong output or memory leak that the sanitizers cannot detect. Code unreachable from the selected entry point, other builds and other machine environments need separate consideration.

Start from a fuzz target; retain tests beyond its guarantee

Theorem offers its verification program free to qualifying open-source projects. Enrollment uses a pull request containing project metadata, a Dockerfile for the build environment and a script to build fuzz targets. An existing OSS-Fuzz setup is a starting point, though producing static riscv64 binaries may require porting work.

For a delivered proof, match the entry point, executable and input or memory assumptions to the intended use. A result about a RISC-V binary does not automatically carry over to an x86 or ARM service. Application integration and unproved behavior still need testing.

The useful outcome is a stronger guarantee over a defined scope. Tests continue to cover requirements and environments beyond it. Connecting those scopes is what turns an AI-generated proof into usable engineering evidence.

FAQ