Anthropic and Theorem Scale Automated Formal Verification to Compiled RISC-V Binaries

Anthropic and Theorem have automated formal proof generation at the assembly level for 123 open-source C/C++ libraries using Claude and Rocq. The pipeline converts existing OSS-Fuzz targets into formal specifications, proving memory safety and assertion integrity over compiled RISC-V static binaries under explicit environmental constraints.

Automated Instruction-Level Proof Generation

Formal verification has historically seen limited adoption outside mission-critical domains due to the immense manual overhead required to write proofs. A joint project by Anthropic's Frontier Red Team and Theorem demonstrates that large language models can autonomously produce machine-checkable proofs at the assembly level. The authors evaluated the approach across Google's OSS-Fuzz project, successfully targeting 239 entry points across 123 open-source software libraries.

Rather than proving high-level source code, the system generates mathematical proofs directly against compiled RISC-V executables. Using Claude, the pipeline proved that target binaries execute without crashing, failing assertions, or violating memory constraints. During proof construction, the model identified and patched long-standing bugs in production codebases that had previously eluded trillions of fuzzing iterations.

Translating Fuzz Targets into Executable Specs

A primary obstacle in scaling formal methods is constructing precise specifications for non-trivial software. The researchers resolved this by converting existing developer-authored fuzzing harnesses into formal specifications. OSS-Fuzz entry points utilize AddressSanitizer (ASan) instrumentation to catch memory safety violations such as out-of-bounds accesses or use-after-free conditions.

The spec formalizes the statement: "this fuzz target will not crash for any input up to 64 MB." Claude generates proof artifacts establishing that the compiled RISC-V binary satisfies this rule across all possible input bitstreams within the length bound. This converts unbounded, probabilistic fuzz testing into a deterministic mathematical guarantee for the specified entry points.

Proof Scale, Architecture, and Environmental Assumptions

The complete verification effort generated approximately 180 million lines of Rocq code. A representative proof runs roughly 600,000 lines of Rocq to formally check a binary with a median length of 18,000 RISC-V instructions. Generated proofs are mechanically validated by the Rocq kernel against formal ISA and operating system models supplied by Theorem.

• The target executable runs as a single-threaded static binary on a RISC-V CPU.
• Program memory allocation strictly operates within a fixed memory budget.
• Valid inputs are bounded to a maximum size of 64 MB.
• Linux operating system responses and memory layouts behave according to Theorem's formalized Linux process model.