What is OpenVM actually trying to prove?
A zkVM lets a prover execute a program normally and produce a cryptographic proof that the execution followed the rules of the machine. The verifier does not need to replay the entire computation.
OpenVM approaches this with a modular, no-CPU architecture. Instead of putting the complete virtual machine into one giant proving circuit, it decomposes the machine into specialized chips and extensions.
Execution produces a trace → AIRs constrain the trace → buses prove that chips agree → the proof system proves those constraints → recursion makes the result scalable.
The architecture at a glance
The important architectural distinction is that OpenVM is not best understood as a conventional CPU with several peripherals. The proving architecture is intentionally decomposed into chips, with each chip responsible for a well-defined part of execution and its corresponding algebraic constraints.
From Rust to RISC-V
The developer starts with ordinary Rust guest code. They do not write AIR, STARK constraints or polynomial commitments. The normal compilation pipeline lowers the program toward a machine-level representation, targeting RISC-V.
Rust guest program
│
▼
Rust compiler
│
▼
HIR
│
▼
MIR
│
▼
LLVM IR
│
▼
RISC-V binary
│
▼
OpenVM transpiler
│
▼
OpenVM ISA
The key boundary to remember is RISC-V semantics ↔ OpenVM semantics. If the translation changes what an instruction means, the prover and the machine can disagree before the STARK system even enters the picture.
A modular instruction set
OpenVM supports a RISC-V-based instruction set and is designed to be extended with specialized operations. The motivation is straightforward: some cryptographic operations are extremely expensive if decomposed into many ordinary instructions.
RV32IM
Arithmetic, logic, loads, stores, branches and other ordinary RISC-V execution.
Keccak / SHA
Specialized proving paths for cryptographic hashing workloads.
Int256 / modular ops
Large-integer operations that would otherwise expand into many smaller VM steps.
ECC / Pairings
Specialized chips for elliptic-curve and related cryptographic operations.
Keccak using ordinary instructions
Keccak
│
├── many RISC-V instructions
├── large execution trace
└── expensive proving
│
▼
dedicated chip
│
▼
Keccak AIR
│
▼
smaller / specialized
proof workload
No central CPU — chips execute the machine
A useful mental model is a collection of cooperating proving components. A base chip handles ordinary operations, while memory and specialized extensions handle their own responsibilities.
OpenVM
│
┌──────────────────┼──────────────────┐
│ │ │
▼ ▼ ▼
Base chip Memory chip Extension chips
ADD / MUL LOAD / STORE Keccak / SHA / ECC
branches read / write Int256 / Pairing
│ │ │
└──────────────────┼──────────────────┘
│
▼
Execution traces
For example, an addition can be represented by a trace row containing the operands and result. A memory operation needs more information: address, value, access type and ordering information all have to be represented in a way that later constraints can enforce memory consistency.
How execution becomes mathematics
An AIR — Algebraic Intermediate Representation — replaces the informal statement "the machine executed correctly" with algebraic constraints over the execution trace.
a = 5
b = 7
c = 12
constraint:
c - a - b = 0
valid:
12 - 5 - 7 = 0
invalid:
13 - 5 - 7 ≠ 0
Real AIRs are substantially richer. They constrain current rows, transitions between rows, flags, selectors, memory accesses and other machine state. The central idea remains the same: a valid execution trace must satisfy every required constraint.
Instruction correctness
Constrains arithmetic, logic, register updates, program counter behavior and related state transitions.
Read / write consistency
Constrains the representation of memory accesses and the consistency of values over time.
Specialized operations
Represents the algebraic correctness of operations such as Keccak or ECC.
Initial / final state
Connects the trace to the intended program inputs, outputs and machine state.
How independent AIRs agree
AIR proves that one chip's trace obeys its own equations. That alone is not enough. The chips also have to agree with one another.
Execution chip
│
│ "read address 100"
▼
BUS / INTERACTION
│
▼
Memory chip
│
│ "address 100 → value 42"
▼
Execution state
│
▼
register x5 = 42
A useful mental model is that a bus behaves like a proof-level API. One AIR emits an interaction and another AIR supplies the matching interaction. The proving system checks that the required collections of interactions match.
VM semantics, AIR semantics and cross-AIR interactions must describe the same computation.
SWIRL: from constraints to a proof
Once the traces, AIR constraints and cross-chip interactions are defined, the proving layer turns those statements into polynomial claims and then into a succinct cryptographic proof.
AIR constraints
│
▼
Bus / interaction claims
│
▼
LogUp
│
▼
GKR / reductions
│
▼
Zerocheck
│
▼
Polynomial claims
│
▼
Stacking
│
▼
WHIR
│
▼
Low-degree testing
│
▼
STARK / SWIRL proof
LogUp
Supports lookup and multiset-style matching arguments used to connect interactions.
GKR
Reduces large structured computation claims into smaller claims that are cheaper to verify.
Zerocheck
Turns "this constraint polynomial is zero on the required domain" into a proof claim.
WHIR
Handles polynomial openings and low-degree testing inside the STARK-style proving stack.
Continuations and deferral
Large programs can produce enormous execution traces. OpenVM's proof composition architecture provides mechanisms for splitting and postponing expensive work rather than forcing everything into one monolithic proof.
The security boundary is the connection between segments and between deferred work and the computation that depends on it. A proof of a segment is only useful if the next segment really starts from the state produced by the previous one.
From many proofs to one root proof
Recursive verification means that one proof can be verified inside another proving computation. This allows a large collection of segment proofs to be compressed into an aggregate result.
Proof π₁ Proof π₂ Proof π₃ Proof π₄
│ │ │ │
└───────────────┴───────────────┴───────────────┘
│
▼
Recursive verifier
│
▼
Aggregate proof
│
▼
Recursive verifier
│
▼
ROOT PROOF
│
▼
Verify
The important property is not merely that proofs are combined. The recursive verifier must correctly enforce the statement that every child proof was valid and that its public inputs and commitments are connected to the aggregate statement.
The verifier sees a proof, not the whole program
After proof composition, the final verifier checks the resulting cryptographic statement. It does not need to replay billions of VM steps.
Huge Rust computation
│
▼
RISC-V execution
│
▼
many trace rows
│
▼
many AIRs + interactions
│
▼
STARK / SWIRL proofs
│
▼
recursive aggregation
│
▼
small final proof
│
▼
VERIFIER
│
┌────┴────┐
▼ ▼
ACCEPT REJECT
This is the payoff of the entire architecture: the computational work can be enormous while the final verification task is comparatively small.
One ADD, from Rust to proof
Take a tiny guest program that computes z = x + y, where
x = 10 and y = 20. The exact internal trace is
more detailed than this simplified example, but the architectural flow is:
Rust │ │ z = x + y ▼ RISC-V │ │ ADD ▼ OpenVM ISA │ ▼ Execution chip │ │ trace row ▼ ADD / Base AIR │ │ constraint: │ result - x - y = 0 ▼ Bus interactions │ ▼ Polynomial constraints │ ▼ SWIRL / STARK proving │ ▼ Segment proof │ ▼ Recursive aggregation │ ▼ Final proof │ ▼ Verifier → ACCEPT
What happens when you add a new operation?
One of OpenVM's strongest architectural ideas is that a new specialized operation does not require redesigning one enormous monolithic circuit. The extension is integrated into the VM's execution and proving model.
NEW OPERATION
│
┌──────────────┼──────────────┐
▼ ▼ ▼
Guest interface Transpiler Executor
│ │ │
└──────────────┼──────────────┘
▼
New chip
│
▼
New AIR
│
▼
Bus interactions
│
▼
STARK proof
This modularity is why understanding the chip → AIR → bus pattern is more useful than memorizing individual extension names.
OpenVM stack, layer by layer
| Layer | Technology / concept | Purpose |
|---|---|---|
| Guest | Rust | Program being proven. |
| Compiler | Rust compiler + LLVM | Lower guest code toward RISC-V. |
| ISA | RISC-V RV32IM | Machine-level instruction target. |
| Translation | OpenVM transpiler | Maps RISC-V into OpenVM's instruction representation. |
| Execution | Modular chips | Execute different classes of operations. |
| Memory | Memory architecture | Represent and constrain reads and writes. |
| Extensions | Keccak, SHA, ECC, arithmetic, etc. | Efficient specialized operations. |
| Arithmetization | AIR | Express execution correctness algebraically. |
| Interaction | Buses / lookups | Connect independent AIRs. |
| Proof | STARK / SWIRL stack | Prove polynomial constraints and interactions. |
| Composition | Continuations | Split long executions into segments. |
| Deferred work | Deferral | Move selected expensive proving work to another stage. |
| Aggregation | Recursion | Compress many proofs into a smaller proof. |
| Verification | Final verifier / on-chain integration | Check the resulting cryptographic statement. |
| Extension language | Rust | Implement VM extensions and proving components. |
How to study the OpenVM codebase
The most effective approach is to move from architecture to one concrete instruction, then expand outward into proving and recursion.
-
Top-level architectureUnderstand the relationship between the VM, extensions, chips and proving backend.
-
RV32IM extensionStart with ordinary instructions before studying specialized cryptographic chips.
-
TranspilerFollow how RISC-V instructions become OpenVM instructions.
-
ExecutorSee how an instruction is executed and what data is recorded for proving.
-
MemoryStudy reads, writes, ordering, roots and the interactions that connect memory to execution.
-
One simple chipUnderstand the complete executor → trace → AIR lifecycle with the smallest useful example.
-
Keccak / specialized chipLearn why specialized operations need their own execution and AIR logic.
-
BusesTrace one interaction between two chips and identify exactly what prevents mismatches.
-
STARK backend / SWIRLOnly after understanding AIRs and buses, study LogUp, GKR, Zerocheck, stacking and WHIR.
-
ContinuationsUnderstand how long executions become independently provable segments.
-
RecursionFollow how one proof becomes an input to another proof.
-
DeferralUnderstand how expensive work can be moved out of the main proving path.
-
Final verifierFinish by tracing the exact public inputs, commitments and proof checks.
Where bugs are most interesting
The architecture gives a natural audit methodology. At every boundary ask: what information crosses, what invariant must hold, where is it enforced, and can I construct a counterexample?
Compiler / transpiler
Can RISC-V semantics and OpenVM semantics diverge for an instruction or edge case?
VM execution
Can an instruction, branch, register update or program-counter transition be implemented incorrectly?
AIR constraints
Is every value that matters actually constrained? Are selectors, flags, boundaries and transitions fully enforced?
Memory
Can reads, writes, ordering or memory-root construction become inconsistent with execution?
Bus interactions
Can one chip emit an interaction that another chip accepts without representing the intended operation?
Recursive verifier
Can malformed proof data, public inputs or bounds cause an invalid child proof to be accepted?
Final verifier
Are commitments, field encodings, selectors and public inputs interpreted exactly as intended?
Composition boundaries
Do continuation and deferred proofs preserve the exact state and statement that the next stage expects?
Execution → Trace → AIR → Bus → Proof → Recursion → Verification
OpenVM in one picture
RUST
│
▼
Rust Compiler
+ LLVM
│
▼
RISC-V
│
▼
OpenVM Transpiler
│
▼
OpenVM ISA
│
▼
┌─────────────────┐
│ CHIP EXECUTION │
└────────┬────────┘
│
┌────────────────┼────────────────┐
│ │ │
▼ ▼ ▼
Base AIR Memory AIR Extension AIRs
│ │ │
└────────────────┼────────────────┘
│
▼
BUS / LOOKUPS
│
▼
AIR + INTERACTIONS
│
▼
SWIRL / STARK
│
▼
SEGMENT / DEFERRED
PROOFS
│
▼
RECURSION
│
▼
ROOT PROOF
│
▼
VERIFIER
│
┌──────┴──────┐
▼ ▼
ACCEPT REJECT
OpenVM executes a RISC-V program by decomposing machine behavior into chips, proves each chip algebraically through AIR, connects the chips through proof-level interactions, and composes those proofs until a final verifier can establish the correctness of the computation.