AI-Assisted Formal Verification of RISC-V Software: What Anthropic and Theorem Demonstrated

On 22 October 2026, Anthropic reported that Claude had generated machine-checked formal proofs for 239 fuzz-test entry points across 123 open-source libraries, working with Theorem. The proof targets were compiled RISC-V binaries; the Rocq proof assistant checked formal claims about their behaviour under a defined execution model. This is a substantial demonstration of AI-assisted proof construction, not evidence that 123 complete libraries are defect-free. It is also not a proof that a physical RISC-V processor correctly implements its instruction set. For semiconductor verification engineers, the central lesson is the evidence boundary: a successful proof depends on the statement being checked, the model used to interpret the binary and the assumptions connecting that model to deployed systems. [1][2]

What Did Anthropic and Theorem Actually Prove?

Anthropic’s 22 October study describes using Claude to develop proofs concerning 239 OSS-Fuzz entry points in 123 libraries. The authors report an input-size limit below 64 MB, together with assumptions about a single-threaded, statically linked RISC-V/Linux execution environment and fixed memory resources. The AI also found bugs and, in some cases, patched the software before completing proofs. These figures describe Anthropic’s reported research programme; they are not an independently reproduced count of complete, fully verified libraries. [1]

An entry point is a fuzzing harness: a particular route into the code through which a fuzzer supplies inputs. A library may expose many other entry points and behaviours. A compiled binary is the particular executable built from a source revision, compiler, dependencies and flags. A theorem statement formalises a property of that executable. A proof artefact supplies a derivation for that statement, and a checked proof is one accepted by the trusted Rocq kernel under its permitted assumptions. The execution model gives meaning to the RISC-V instructions and modelled Linux process interactions. None of these objects is interchangeable.

The public evidence is narrower than the company’s overall research report. On 9 November 2026, Theorem’s open OSS Verify repository listed 90 proved entry points across 32 libraries, with proof files, theorem statements and instructions for checking them using Rocq 9.2.0. The repository had expanded beyond earlier reports of 60 entry points across 25 libraries. It is a public subset, not a publication or independent reproduction of all 239 study proofs. [2]

How the AI-Assisted Formal Verification Workflow Worked

The starting point was a developer-written fuzz test from Google OSS-Fuzz. Conventional fuzzing repeatedly supplies generated or mutated inputs, looking for failures; it does not, by itself, establish that all permitted inputs are safe. Anthropic and Theorem instead used existing harnesses as the basis for formal obligations that could be checked across a defined modelled input space. [1][4]

The evidence workflow can be understood as eight stages:

1. Select a harness and source revision. Identify the entry point and the property represented by its failure conditions.
2. Build a specific executable. Compile the harness and library into a static RISC-V/Linux binary; retain the compiler, linker settings and binary identity.
3. Define the semantics and obligation. Interpret the executable using the RISC-V instruction model and Linux Process Semantics (LPS), and state the applicable error, input and resource conditions.
4. Generate a candidate proof. Claude develops Rocq proof material for the formal obligation. The language model proposes the proof; it is not the trusted mathematical checker.
5. Check mechanically. Rocq verifies that the proof term establishes the stated proposition within the formal system and accepted axioms.
6. Investigate failures. An unsuccessful proof attempt can reveal an actual software defect, an incomplete proof, an invalid assumption or a limitation of the model. Failure to prove is not automatically proof of a bug.
7. Patch and regenerate where necessary. Anthropic reports letting Claude modify code to address discovered defects. A change creates a new source and binary revision and therefore requires renewed checking; a proof of the patched version does not prove the original version safe.
8. Preserve provenance. Record the exact binaries, source, theorem statements, LPS release, allowed axioms, checker version and results. [1][2][3]

An additional concern is specification gaming: an automated patch could make a no-crash condition easier to satisfy by disabling useful behaviour. Anthropic describes auditing patches and discouraging unnecessarily broad changes. Independent review of the intended semantics, diff and regression results remains essential. [1]

Figure 1: From AI-generated proof to trusted verification evidence.

Figure 1 shows Evidence chain for AI-assisted formal software verification. Claude generates candidate proofs, Rocq checks formal statements, and the resulting claims depend on the model and assumptions. Separate verification evidence is required to establish the correctness of a physical RISC-V implementation.

What Does a Machine-Checked Proof Establish?

At its core, a machine-checked proof shows that a precisely stated proposition follows within an encoded logic and model. It does not independently decide whether that proposition captures the engineer’s real requirement. Rocq can check a correct proof of a weak or misplaced statement just as rigorously as a useful one. That makes the theorem’s wording, preconditions and reachable behaviour as important as the proof term itself. The related risk of proving the wrong property is explored in Alpinum’s article on vacuous proofs and over-constrained formal verification. [2][5]

Theorem’s released agreement statements make this more concrete. For LPS-valid process inputs where the ordinary binary stays inside a stated memory budget, the normal build and a sanitizer-instrumented build must avoid defined errors and have matching sets of observable behaviours. Observable behaviour includes process output, exit status and final file contents. Instrumented variants may use AddressSanitizer (ASan), UndefinedBehaviorSanitizer (UBSan) or both. For released agreement obligations, the plain-build memory-budget premise is 2 GiB with ASan-related builds and 16 GiB for UBSan. These numbers are premises, not guarantees for executions that exceed them. Each statement also restricts which environment-induced system-call failures are permitted. [2]

The public release now includes another theorem type: halts statements. These assert, under their own specified conditions, that executions terminate with an allowed status. At the 9 November source check, Theorem documented 179 proved halts statements. This matters because an agreement proof alone may permit infinite execution, whereas a specific halts proof addresses termination within its premises. Do not transfer a halts guarantee to entry points for which only agreement has been proved. [2]

As an illustrative property, not a quotation of a published theorem, consider: For every model-valid input satisfying a memory-budget premise, the selected executable does not reach a specified invalid-memory-access state. A checker can verify a proof of this property. It cannot establish that every input in the deployed system satisfies the premise or that the model covers every physical failure mode.

Where the Proof’s Trust Boundary Ends

Theorem explicitly describes LPS as an incomplete model of a Linux process running a RISC-V binary. Its documentation lists restrictions on valid inputs and operating-system responses. The trust boundary includes more than the proof text: Rocq’s kernel and permitted axioms, the LPS semantics, the conversion from ELF binaries to modelled memory images, the proof-checking wrapper and the identities of the binaries and model revisions. A successful check is evidence only for the formal artefacts actually supplied. [2][3]

The distinction becomes important at several boundaries:

• Program scope: Only code reachable through the selected fuzz harness is covered. Another API, caller configuration or unreachable library function may have different defects.
• Build scope: The released proofs concern static riscv64 binaries built with clang 20.1.8 against musl. They do not automatically transfer to x86-64, Arm, another compiler or dynamically linked glibc builds. The wider RISC-V software ecosystem adds compilers, runtimes and operating systems that require their own evidence.
• Inputs and resources: The Anthropic study describes the below-64-MB input bound; the public theorem forms additionally impose model-validity, resource-budget and system-call premises. An excluded input or resource-exhaustion case is not covered merely because an adjacent case was proved.
• Error coverage: ASan and UBSan detect specified fault classes; they do not establish arbitrary functional correctness, freedom from memory leaks or the correctness of every output.
• Liveness: An agreement proof does not imply termination. Only the relevant halts theorem, where present, carries the stated termination obligation.
• Model fidelity: A proof can be mathematically sound when the formal semantics omit an operation or differ from the real Linux environment. Source-to-binary mapping and build provenance are therefore part of the assurance argument. [1][2][3]

This is not a criticism peculiar to AI-generated proofs. Formal verification always depends on the relationship between the property, assumptions and implementation. The larger scale of generated proof material makes those boundaries more important, not less.

Why Software Proofs Do Not Verify a RISC-V Processor

The key architectural distinction is between a mathematical instruction-level model and an RTL implementation of a processor. The software theorem reasons about what the executable would do when instructions and process operations behave according to the trusted model. It does not establish that a specific pipeline, load-store unit, cache, memory interface or physical silicon implementation conforms to that model. RISC-V’s ratified specifications define architectural behaviour; conformance of a particular implementation is a separate verification obligation. [2][6]

A complete assurance argument could connect these layers. Teams might establish ISA compliance for relevant instructions, prove selected RTL properties, then validate the compiler, runtime, OS interfaces and applications on the actual target. That integration is an engineering possibility, not an outcome reported for the Anthropic–Theorem software study. Alpinum discusses processor and block-level obligations in formal verification for RISC-V processors and SoCs.

An Illustrative RISC-V Hardware–Software Verification Gap

Hypothetical example, not a defect reported by Anthropic or Theorem. Consider a parser that reads a one-byte length field using the RV64I LBU instruction, then checks a buffer boundary before accessing the payload. In the mathematical instruction model, LBU returns the addressed byte zero-extended to register width. Assume the relevant memory address is valid and the platform configuration meets the instruction’s architectural conditions. [6]

Suppose a software theorem establishes that the compiled parser does not perform an out-of-bounds access for the specified model-valid inputs. Now imagine a processor RTL defect in which the byte-select logic sometimes returns an adjacent byte when the low address bits match a rare pattern. The software proof can remain perfectly valid: its modelled LBU operation returned the correct byte. The defective physical processor did not. It could therefore bypass the intended bounds decision and produce behaviour outside the proved model.

A hardware team would need to check the relevant LBU address selection, returned data, access and exception behaviour across legal configurations; correlate instruction-level and RTL observations; and test the integrated memory path and parser on the target platform. Even that work would leave compiler, runtime, peripheral and untested-system assumptions to address. This example illustrates a missing evidence link, not a flaw in Rocq’s checker.

What Semiconductor Verification Engineers Can Learn

The practical lesson is to make proof evidence reviewable, not merely voluminous. A useful engineering record starts with the intended requirement, identifies the exact theorem and legal assumptions, pins the binary and model versions, and records the toolchain that checked the proof. For AI-authored material, preserve the candidate and any source changes separately from the accepted result. [2][3]

A team assessing similar methods should ask five questions. What is the claim? A no-error, agreement or termination theorem has different meaning. Which implementation is covered? A static binary is not interchangeable with source code or a deployed build. Who checks the proof? The checker should validate formal derivation rather than rely on the model’s prose. Which assumptions remain trusted? Inspect input restrictions, semantics, axiom lists and resource limits. What further evidence is necessary? ISA/RTL conformance and end-to-end system validation remain separate engineering tasks.

Proof-driven bug repair also needs control: review source diffs, maintain build identities, re-establish the formal obligation after patching and confirm that the change preserves intended functionality. In a verification organisation, acceptance and sign-off remain engineering decisions.

Where AI-Assisted Formal Verification Could Go Next

Promising directions include reusable proof components, better model validation, formal semantics for other architectures and runtime environments, and stronger methods for connecting software-level guarantees to verified processor implementations. These are research and engineering opportunities, not capabilities that the present OSS Verify release universally demonstrates. [1][2] The important shift is the possibility of generating substantial proof material economically enough to make more properties checkable. Whether that improves a particular verification team’s throughput or assurance will depend on review effort, compute cost, model quality, reproducibility and the importance of the chosen obligations.

Conclusion

The Anthropic–Theorem research is significant because it demonstrates AI-assisted construction of formal proof artefacts that can be mechanically checked, rather than accepted on the language model’s authority. Its value lies in the precision of the evidence: which executable, which property, which execution model and which assumptions were actually verified.

For semiconductor teams, that precision also defines what remains to be done. A proof about software executing in a formal RISC-V model does not automatically establish correct RISC-V processor RTL or a working SoC. Organisations evaluating these cross-layer obligations can explore Alpinum’s Formal Verification Services to develop a requirement-led verification and evidence strategy.

References

1. Anthropic, “LLMs are making formal software verification feasible at a much larger scale,” 22 October 2026. https://www.anthropic.com/research/formal-verification
2. Theorem, OSS Verify: proofs about OSS-Fuzz fuzz targets (public repository; reviewed 9 November 2026). https://github.com/theorem-labs/oss-verify-proofs
3. Theorem, OSS Verify trust documentation and LPS semantics documentation, accessed 9 November 2026. https://github.com/theorem-labs/oss-verify-proofs/blob/main/docs/trust.md ; https://github.com/theorem-labs/oss-verify-proofs/blob/main/docs/semantics.md
4. Google, OSS-Fuzz documentation. https://google.github.io/oss-fuzz/
5. The Rocq Prover, official project documentation. https://rocq-prover.org/
6. RISC-V International, RISC-V Ratified Specifications Library: RV64I Base Integer Instruction Set, version 20260120. https://docs.riscv.org/reference/isa/v20260120/unpriv/rv64.html

FAQs