Formal software verification

Definition

Formal verification proves that a mathematical model of a program satisfies a stated specification. A proof checker validates the derivation; whether the specification and machine semantics describe the intended deployment remains a separate trust requirement. (source)

Why It Matters

Anthropic and Theorem use existing fuzz-test entry points to define no-crash specifications over compiled binaries. This gives Agents (LLM Agents) a checkable objective while retaining explicit limits on what a successful proof establishes. (source)

State of the Art (2026-10-25)

The October 22 report says Claude patched bugs and proved no-crash properties for 239 entry points across 123 OSS-Fuzz libraries, producing about 180 million lines of Rocq. The proofs concern single-threaded static RISC-V Linux binaries, a fixed memory budget and inputs below 64 MB. They do not establish that whole libraries or ordinary x86/ARM deployments are bug-free. (source)

On 36 small verification tasks, Opus 5.5 proves half with about 40% fewer tokens than Opus 5. Each task receives three independent single-agent attempts with a 5M-token budget; the first completed attempt establishes success. A shared proof workspace uses 17% fewer tokens than agents working alone. These are vendor-reported experiments, not independent replications. (source)

Open Problems

Proofs can require hundreds of millions of tokens. Trusted components include the formal semantics, theorem statements and Rocq checker, with its underlying execution stack. AddressSanitizer misses some memory errors; the study does not cover every entry point or caller misuse. Allowing agents to patch code can also trivialize a specification, so the authors penalize patches and audit them for reward hacking. (source)

Key Papers

• The October 22 technical report publishes a subset of proofs and the RISC-V/Linux semantics. The linked appendix and proof repository have not been independently checked here. (source)

Related Concepts

• AI for Mathematics — machine-checkable derivations are related, while software verification additionally depends on the program specification and machine model. (source)
• Eval Harness Configuration — a passing result depends on what the specification actually covers. (source)