Building a zkVM used to mean hand-crafting a constraint system for every instruction in the ISA, one artisanal circuit per opcode. Jolt's bet is that this whole approach is backwards: don't constrain the instruction, look it up. Every RISC-V op becomes one row in a table so big you'd never build it, and it turns out that doesn't matter.
I want to walk through why that isn't a slogan. It's a real architectural shift, and the thing that makes it work, the sum-check protocol, is the same primitive quietly running underneath GKR, Spartan, and basically every modern SNARK worth caring about. Learn it once here and a bunch of other posts click into place.
Most zkVMs (SP1, RISC Zero, the older Cairo-style systems) work by writing a set of polynomial constraints for each RISC-V instruction. ADD gets a constraint. AND gets a different constraint. SLT gets its own thing. Multiply that by a real ISA and you get hundreds of hand-tuned constraint systems, each one a small research project, each one a place a bug can hide.
This scales badly in the way hand-written anything scales badly. Adding an instruction means writing new circuitry from scratch. Auditing the VM means auditing every opcode's constraint system independently. It's the zk equivalent of writing a new assembly routine for every button on a keyboard instead of building a keyboard driver.
Jolt's founding move, from the Lasso and Jolt paper, is to stop constraining instructions and start looking them up. If you already know every possible input/output pair for AND, you don't need a constraint system that proves the arithmetic. You just need to prove "the output I claimed is the row in the table that the inputs point to." That's a lookup problem, not a circuit-design problem, and lookup problems have gotten a lot cheaper to prove.
Here's the naive version. Take a 64-bit AND. Define a table T where the entry at index (a, b) is AND(a, b). The index space is every possible pair of 64-bit operands, which is 2^128 rows. You are never going to materialize a 2^128-row table. Nobody's disk is that big, nobody's field is that big, this is a non-starter as written.
The trick is decomposition. AND is bitwise, so you can split each 64-bit operand into eight 8-bit chunks and compute the answer chunk by chunk:
AND(a, b) = sum over c=0..7 of 2^(8*c) * AND8(a_c, b_c)
AND8 is a table over two 8-bit inputs: 2^16 entries. That's nothing. You build eight tiny subtables (or one subtable reused eight times), do eight lookups instead of one impossible lookup, and recombine with a weighted sum. The 2^128-row monster was always secretly eight 65536-row toys wearing a trenchcoat.
A toy implementation of the decomposition:
function decomposeAND(a: bigint, b: bigint): bigint {
let result = 0n;
for (let c = 0; c < 8; c++) {
const shift = BigInt(8 * c);
const aChunk = (a >> shift) & 0xffn;
const bChunk = (b >> shift) & 0xffn;
const chunkAnd = aChunk & bChunk; // this is the "AND8" subtable lookup
result |= chunkAnd << shift;
}
return result;
}This is the "spirit, with an asterisk" version of the slogan. Not every instruction is literally one lookup. Most decompose into a handful of small subtable lookups plus a cheap recombination step, and control flow (branches, jumps) still lives outside the lookup machinery entirely, in an R1CS. But the core claim survives: you never build a table the size of the ISA's full input space. You build small tables and pay for the recombination.
This "decomposable into MLE-structured subtables" property is exactly the requirement for the next piece.
Lasso is the lookup argument that makes the decomposition tractable as a proof, not just as a compute trick. The property that makes Lasso different from older lookup arguments is what it charges you for.
Older lookup arguments (things built on top of plookup-style permutation checks) tend to have prover cost that scales with the size of the table, because the argument has to commit to something as big as the table itself. That's fine for a 256-row table. It's a dealbreaker for a conceptual 2^128-row table, even a decomposed one, if the proof system still has to "see" the whole thing.
Lasso's sparse-dense decomposition means prover cost scales with the number of lookups you actually perform plus the size of the small subtables, not the size of the conceptual big table. You did a few thousand AND operations in this execution trace. Lasso charges you for a few thousand lookups into 2^16-row subtables. It does not charge you for the 2^128 rows you never visited. This is the whole "lookup singularity" idea from the original announcement: once lookups get this cheap, you push as much of the VM's logic into lookups as you possibly can, because the alternative (hand-written constraints) doesn't get cheaper with scale and lookups do.
Underneath Lasso, underneath Jolt's memory-checking, underneath basically all of this, is one protocol: sum-check. If you only remember one thing from this post, remember this, because it shows up again in GKR and Spartan and it's genuinely not complicated once you see it.
The problem: a prover claims that a multivariate polynomial g(x1, ..., xn), summed over every corner of the Boolean hypercube (every x_i in 0,1), equals some value H.
H = sum over all (x1,...,xn) in {0,1}^n of g(x1, ..., xn)
A verifier checking this directly has to evaluate g at all 2^n points and add them up. For any real n that's the whole problem sum-check exists to avoid.
Sum-check trades 2^n verifier work for n rounds of cheap algebra, one variable eliminated per round:
Round 1. The prover doesn't send the full sum. It sends a univariate polynomial, s1(X1), that you get by summing g over every possible value of every variable except x1, leaving x1 as a free variable named X1:
s1(X1) = sum over x2,...,xn in {0,1} of g(X1, x2, ..., xn)
The verifier does one cheap check: does s1(0) + s1(1) equal H? If the prover is honest, yes, because that's just re-summing over x1 in 0,1. The verifier also checks that s1 has the degree it's supposed to have (the degree check, more on why that matters below). Then the verifier picks a random challenge r1 and asks the prover to continue as if x1 had been fixed to r1.
Round 2. The prover sends s2(X2) = sum over x3,...,xn of g(r1, X2, x3, ..., xn). The verifier checks s2(0) + s2(1) == s1(r1), picks a random r2, and hands the baton forward again.
This repeats n times. After the last round, every variable has been bound to a random challenge, and the verifier makes exactly one final check: it evaluates g at the point (r1, ..., rn) directly (one query) and confirms that matches the last polynomial the prover sent. That's it. O(n) rounds of cheap univariate-polynomial checks instead of 2^n points.
A toy version, over a small prime field so the numbers stay legible:
const P = 101n; // small prime, for the toy only, NOT cryptographically sound
// g is given as its 2^n evaluations over the hypercube, indexed by bits
function sumOverRest(evals: bigint[], fixed: number[], nBits: number): bigint {
// sums g over every completion of `fixed` prefix bits, mod P
let total = 0n;
const remaining = nBits - fixed.length;
for (let i = 0; i < 1 << remaining; i++) {
let idx = 0;
for (let b = 0; b < fixed.length; b++) idx |= fixed[b] << b;
for (let b = 0; b < remaining; b++) idx |= ((i >> b) & 1) << (fixed.length + b);
total = (total + evals[idx]) % P;
}
return total;
}
function sumcheckVerifierRound(sAt0: bigint, sAt1: bigint, prevClaim: bigint): boolean {
return (sAt0 + sAt1) % P === prevClaim;
}Why is this sound, and not just a prover getting to say whatever it wants? Because of the degree check. In each round the polynomial s_i is only allowed to have a bounded degree, determined by g's structure. If the prover tried to cheat, is has to fake a polynomial that doesn't match g's actual sum, and by the Schwartz-Zippel lemma, two distinct low-degree polynomials only agree at a tiny fraction of points in the field. A random challenge r_i will catch the lie with probability at least 1 - d / |F|, where d is the degree bound and |F| is the field size. This is why real deployments use large fields, not the toy field above. My P = 101 example above is for legibility, not security. With a small field the failure probability isn't negligible, and you'd want |F| big enough that d / |F| rounds to nothing.
Watch what happened across all n rounds: a 2^n-point sum became n rounds of "send a low-degree polynomial, check two values, sample a random point." That's the whole protocol.
Jolt expresses "did this RISC-V program execute correctly" as three separate checkable claims, each discharged with sum-check-flavored machinery, per the engineering overview:
The thing that surprised me when I first read this breakdown: the lookups, the whole "lookup singularity" pitch, are a quarter of the cost. The dominant line item is the boring part, fetch and decode, the glue that figures out which instruction you're even running before Lasso gets to do its thing. "The whole VM is one big lookup" is the headline. "Three sum-check instances stapled together, and the cheap-sounding decode step is actually the bill" is the reality, and it's a more useful mental model if you're trying to reason about where a real optimization would land.
Current proof sizes for Jolt-class systems sit in the multi-megabyte range (roughly 10MB, ballpark, per the FAQ). The next move, per the Binius work, is moving the polynomial commitment from a big prime field to a binary field, GF(2^128), using small-field sum-check techniques. Committing to bits is dramatically cheaper than committing to big field elements, and the projected outcome is proof sizes dropping from roughly 10MB toward roughly 50KB, with prover speedups reported in the 5-10x range.
I want to flag that number for what it is: a projection from the team building the thing, not a benchmark you can go run today. Treat "50KB" as a direction, not a spec.
This is also the exact same engine (sum-check, GKR-style layered proving) that shows up when you go looking at zkML cost curves, where the workload is neural network inference instead of a RISC-V trace. The lookup singularity made the cheap, structured circuits (arithmetic, bitwise ops) close to free. Whether the same trick tames the hard, unstructured workload (matrix multiplies at LLM scale) is the open question, and it's a much bigger fight than anything in this post.
A few things worth being straight about. The 25/25/50 prover-time split and the 10MB-to-50KB Binius number are a16z's own reported figures, cite them as "as reported," not as independently verified benchmarks. The 5x-over-RISC-Zero, up-to-2x-over-SP1 comparisons are from the initial implementation FAQ at a specific point in time, and zkVM benchmarks move fast enough that you should assume they're stale within a year. "Every instruction is one lookup" is the pitch, not the literal mechanism. Most instructions are a few subtable lookups plus recombination, and branches and jumps live in the R1CS side of the system, not in Lasso at all. And the toy sum-check code above uses a tiny field to keep the arithmetic legible. Real security needs a field large enough that the Schwartz-Zippel failure probability, d / |F|, is negligible, which a 101-element field absolutely is not.
If you take one thing from this: sum-check is the primitive, not Jolt specifically. Once you can derive "reduce a sum over 2^n points to one random-point evaluation, one variable per round," you've got the key that opens GKR, Spartan, and the harder zkML cost-curve conversations too. Jolt is just the cleanest place to watch it work, because the lookup argument built on top of it turned an "obviously intractable" 2^128-row table into something you can decompose into 8-bit chunks and forget about.
The lookup singularity made the easy circuits cheap. Whether it makes the hard ones, real neural nets, cheap too, is still an open fight. If you implement the toy sum-check prover/verifier above and get it running end to end, send it to me.