Lambda VM: design principles

Lambda VM is an open-source zkVM for RISC-V that LambdaClass, Aligned and 3MI Labs are building together. You give it a program compiled for RV64IM and it gives you back a STARK proof that the program ran correctly. Anyone can check that proof without running the program again.

There are already several zkVMs out there, so the obvious question is why we're building another one. The short answer is that we wanted one we could read from top to bottom. The long answer is this post, and most of it comes down to a single idea: keep it simple.

Why another zkVM

A zkVM doesn't remove trust from a system so much as move it around. Before, you trusted a computation because you re-ran it yourself. Now you trust a proof. The Ethereum roadmap puts it as going from "everyone re-executes" to "one proves, everyone verifies", and that shift is what would let the L1 raise the gas limit without asking every validator to buy a bigger machine.

The catch is where the trust ends up. Underneath everything, a zkVM is a set of rules that says what a valid execution looks like. If one of those rules is wrong, or missing, a prover can build a proof for an execution that never happened and the verifier will accept it. There's no error message, no warning. The proof just passes.

So "how fast is it" isn't the only question worth asking about a zkVM. The other one is "how sure are you that its rules are right", and that one doesn't show up in a benchmark.

Ethereum's answer to this kind of risk has been client diversity: several independent implementations, so that a bug in one doesn't take down the network. The same reasoning applies to zkVMs, with a caveat that's easy to forget. Diversity only helps if the implementations are actually independent. If five zkVMs sit on top of the same proving library and that library has a soundness bug, you don't have five zkVMs, you have one bug in five places.

That's the case for Lambda VM: a zkVM that is small, sticks to the RISC-V standard, uses boring cryptography, and comes with a written spec that the code mirrors table by table. Something a person can audit in a reasonable amount of time.

From program to proof

Four steps.

1. Compile. You write the program in Rust and build it with the standard toolchain for our riscv64im target. What comes out is an ordinary ELF binary. A small crate provides the handful of syscalls the guest needs to talk to the host: read inputs, commit public outputs, halt.
2. Execute. The executor loads the ELF and runs it the way any RISC-V machine would. While it runs, it records every step: program counter, instruction, the registers read and written, every memory access. That record is the execution trace.
3. Build the witness. The trace gets split into tables, one per kind of operation (multiplication, division, comparisons, branches, loads, stores, and so on). Each table comes with a set of constraints that every row has to satisfy.
4. Prove. The STARK prover commits to the tables and proves that all the constraints hold, and that the tables are consistent with each other.

Worth stating plainly, because it confuses people at first: the prover never runs the program. The program runs in the executor, not in the prover. Everything after that is about convincing a verifier that the trace it produced is a valid RISC-V execution.

Plain RISC-V

Lambda VM implements RV64IM: the 64-bit base integer ISA plus the multiply and divide extension. No custom instructions (the accelerators are reached through the standard ECALL, like any syscall), no changed semantics.

The reason to be strict about this is that in a zkVM two things have to agree on what an instruction does: the compiler that emitted it and the constraints that check it. Every place where a zkVM strays from the standard, even slightly, is a place where those two can drift apart without anyone noticing. Bugs of exactly this kind have already turned up in production zkVMs.

Staying on the standard also keeps the problem well posed. The reference for what Lambda VM should do is the RISC-V spec and nothing else, so there is no custom instruction behavior for us to define, document, or get wrong. What we add on top, a handful of syscalls and the accelerators, goes through the standard ECALL and has its own section in the spec.

The Ethereum Foundation runs the official RISC-V compliance suite (the Architecture Compatibility Tests) against zkVMs and publishes the results on its zkEVM track. Lambda VM passes all 72 tests, and not just in execution: the suite is run through the prover too, so each test is executed, proven and verified.

The proof system

Lambda VM's proof system is a STARK, and every choice in it leans conservative.

The field. All arithmetic is in Goldilocks, p = 2⁶⁴ − 2³² + 1. Elements fit in a u64, so the arithmetic is fast on ordinary CPUs, and it pairs naturally with a 64-bit ISA.

The extension. 64 bits is too small a space to draw random challenges from. Wherever the protocol needs randomness we move to a degree-3 extension of Goldilocks, which gives roughly 192 bits.

Hashes only. Commitments are Merkle trees over Keccak-256. The Fiat-Shamir transcript that makes the protocol non-interactive is Keccak as well. FRI is the low-degree test, the part that checks that what was committed really came from polynomials of the expected degree. The security of the whole thing rests on the hash function: no elliptic curves or pairings anywhere, and no trusted setup. It's also why the proofs are considered post-quantum secure.

Our own stack

The cryptography lives in the same repo as the VM: field and extension arithmetic, NTT, Merkle trees, FRI, and the STARK prover and verifier. It started out as lambdaworks primitives and has grown alongside the VM since.

We deliberately don't sit on top of a large external proving framework. Outside the proof system the dependency list is short: a Keccak implementation on the host side, secp256k1 arithmetic to generate witnesses for the signature accelerator, and the usual crates for serialization and parallelism.

And it's not a lot of code. The executor is around 3k lines of Rust, the prover with all its tables and constraints around 21k, the cryptography around 26k. Call it 50k lines total, not counting tests or the optional GPU backend.

Owning the stack also feeds back into the diversity argument from earlier. Lambda VM doesn't share a proving stack with any other zkVM, so a bug in someone else's library isn't a bug in ours, and vice versa.

A spec the code mirrors

This is the part we care about most.

Every chip in Lambda VM (a chip is a table plus its constraints) is defined first in a small machine-readable file: its inputs and outputs, their types, its constraints, and how it interacts with the other chips. The spec document is generated from those files, plus prose explaining each chip and the pieces that cut across several of them, like the memory argument.

The code is organized the same way, one chip per file:

spec/src/mul.toml     ↔  prover/src/tables/mul.rs
spec/src/branch.toml  ↔  prover/src/tables/branch.rs
spec/src/memw.toml    ↔  prover/src/tables/memw.rs
...

Same chips, same variables, same constraints on both sides. If you want to know how a multiplication gets proven, you open one chip definition and one Rust file and read them next to each other.

Why this helps an auditor

When the spec and the code have the same shape, an audit breaks into two smaller jobs that don't have to happen at the same time, or even be done by the same person.

The first is: is the spec right? Do the constraints on each chip actually pin down what the RISC-V instruction does? Do the chips together force a valid execution? This is a math question. You can answer it without opening a Rust file.

The second is: does the code match the spec? That's a comparison between two documents with the same structure.

Neither job involves reverse-engineering what the code is trying to do, which is where audits normally burn most of their hours. And when something changes, it's immediately obvious whether the change touched the spec or just the implementation.

And a formal verification effort

The same structure is what makes formal verification look realistic rather than aspirational.

To formally verify a zkVM you need a precise statement of what the VM enforces, and then a proof that the code enforces exactly that. In most systems the first part is the expensive one, because the statement has to be dug out of the code after the fact. Here it already exists: it's the spec. It's small, and each chip can be checked on its own, first against the RISC-V semantics and then against its implementation.

We don't want to oversell this. Formally verifying a zkVM is a lot of work under any architecture. But here it's work that can start right away, chip by chip, instead of work that starts with an archaeology project.

Continuations and recursion

Everything so far is about proving one execution in a single shot. Real workloads, an Ethereum block for instance, are far too big for that, and two pieces of Lambda VM exist to deal with it.

Continuations. A single proof needs the whole trace in memory at once, and for a long-running program it simply won't fit. Continuations cut the execution into fixed-size segments and prove each one independently. Nearly every constraint is local to its segment. The exception is memory, since a later segment may read something an earlier one wrote, so one extra proof checks that the memory state at the end of each segment is the memory state at the start of the next. The result is that peak memory stays flat however long the program runs. This is what we run today; we're also experimenting with a second way to bound memory that re-runs the program instead of splitting the proof, and we'll write about that one separately.

Recursion. The Lambda VM verifier is just a program, which means it can run inside Lambda VM, which means one proof can verify another. That's the building block for folding many proofs into one and, eventually, for a proof cheap enough to verify on Ethereum.

Each of these deserves its own post and will get one. So will the Keccak and secp256k1 accelerators (the two most expensive parts of proving an Ethereum block) and GPU proving. All of it sits on top of the same small core described above.

Where to start

Code and spec are open source under MIT / Apache-2.0: github.com/yetanotherco/lambda_vm

If you want to understand how Lambda VM works, start with the spec, not the code. If something in it is unclear or wrong, open an issue.

For a VM whose whole selling point is being easy to audit, an unclear spec counts as a bug.