Never Decrypted: Proving You Ran the Computation Without Revealing It

1. Trust Me, I Ran It Right#

A cloud service runs a model you are not allowed to see, on data you refuse to hand over, and returns an answer. How do you check that it actually ran that computation -- without re-running it yourself, and without either side surrendering its secret? For most of computing history the honest answer was: you could not. Today the party doing the work can hand you a receipt a few kilobytes long that settles the question in milliseconds, and the receipt reveals nothing about the inputs, the model weights, or how the work was done.

That is the whole promise, and it is worth stating precisely, because it is easy to overclaim. A zero-knowledge proof lets a prover convince a verifier that a computation was performed correctly while revealing nothing about the private inputs (or model weights) ^[1]. Not "nothing at all" -- the statement being proved is public, and so is the output. What stays hidden is the witness: the private data the prover used to make the statement true.

Three players, then. The prover does the work and wants credit for doing it right. The verifier wants assurance without redoing the work or seeing the secret. And the witness -- the private input -- is the thing the whole apparatus exists to protect ^[2]. Keep those three straight and most of the confusion around this field dissolves.

It helps to say what this is not. The already-published companion post "The Anonymity That Actually Holds" is about hiding who paid whom -- coin privacy, one specific application. This post is about the general machine underneath: proving how a computation ran while hiding the how. It is also not the same as encrypted computation. The series' part-1 post on fully homomorphic encryption computes on data it cannot read; a zero-knowledge proof proves a computation ran. Different guarantees -- and, as we will see, they compose cleanly.

The destination is a concrete artifact: a receipt that says "I ran this exact program (or this committed model) on an input I am not showing you, and got this output." The receipt is small, it is fast to check, and its honesty rests on mathematics rather than on trusting the prover. The catch, and this article stays honest about it throughout: producing the receipt is expensive, often thousands to millions of times more than running the computation once.

The endpoint of this whole story is a few-kilobyte certificate that says "I ran this exact program, or this committed model, and got this output" -- and that reveals nothing about the private inputs that went in. Conviction without disclosure. That is the thing to hold onto; everything else is how we earn it.

To keep breadth from becoming sprawl, we will carry one ledger across the whole article and watch it fill in, generation by generation:

Right now the ledger has two rows: where we started, and where we want to end up. Everything in between is the story.

flowchart LR
W["Private witness: inputs, model weights"] --> P["Prover runs program f"]
Prog["Public: program f, output y"] --> P
P -->|"few-kilobyte receipt"| V["Verifier"]
V --> D{"Receipt valid?"}
D -->|"yes"| A["Accept: f ran correctly"]
D -->|"no"| R["Reject and distrust"]
W -.->|"never revealed"| V

This sounds impossible. How can a transcript convince you of something while carrying none of the secret that makes it true? To see why it is not impossible -- and it genuinely is not -- we have to go back to 1985.

2. 1985: A Proof That Teaches Nothing#

In 1985 Shafi Goldwasser, Silvio Micali, and Charles Rackoff asked a question nobody had thought to formalize. For centuries a mathematical proof meant one thing: a certificate you could read and check. Their question was different. Not whether a statement is true, and not even how hard it is to prove, but how much knowledge the act of proving leaks ^[1].

Their paper, "The Knowledge Complexity of Interactive Proof Systems," recast a proof as a conversation. Instead of a static certificate, a prover and a verifier trade messages, the verifier tossing coins and issuing challenges, until the verifier is either convinced or not. The ideas ran years ahead of print: the interactive-proofs work was presented in 1985, but the definitive journal version did not appear until 1989 ^[1].

Such a proof must satisfy two obvious properties and one strange one. Completeness: if the statement is true, an honest prover convinces the verifier. Soundness: if the statement is false, no prover, however devious, can convince the verifier except with negligible probability. Those two alone describe an ordinary proof. The third is what made the paper historic.

Zero-knowledge: the verifier learns nothing from the conversation beyond the single fact that the statement is true. GMR made "learns nothing" precise with one of the most elegant definitions in cryptography -- the simulator.

Picture a machine that never talks to the prover and does not know the secret, yet fabricates transcripts of the conversation indistinguishable from real ones. If such a simulator exists, the real conversation could not have taught the verifier anything it could not already produce alone. A transcript you could have written yourself carries no information. That is the whole trick, and it repays a pause: conviction and information transfer come apart.

This is exactly where the popular picture goes wrong. A zero-knowledge proof does not hide everything. The statement is public. In our cloud example, "this program produced this output" is out in the open; what the simulator argument protects is the witness -- the private inputs or the model's weights. Get that boundary wrong and every later claim about zkVMs and zkML will be off by a mile.

GMR established zero knowledge for a handful of specific number-theoretic problems. The natural next question was how far it reached. In 1986 Oded Goldreich, Silvio Micali, and Avi Wigderson answered it about as completely as a question can be answered. Their title is a thesis in itself: "Proofs that Yield Nothing But Their Validity, or All Languages in NP Have Zero-Knowledge Proof Systems" ^[3]. Assuming secure encryption exists -- technically, one-way functions -- every statement whose truth can be efficiently checked, every language in NP, has a zero-knowledge proof.

"Proofs that Yield Nothing But Their Validity, or All Languages in NP Have Zero-Knowledge Proof Systems." The 1986 title that turned zero knowledge from a curiosity into a universal tool.

Their vehicle was a puzzle a child could play: graph 3-coloring. Color the vertices with three colors so that no edge joins two of the same color. The problem is NP-complete, so any NP statement can be re-encoded as a coloring.

The protocol is almost mischievous. The prover commits to a randomly permuted coloring -- picture locking each vertex's color in a sealed box. The verifier points at one random edge and asks only for those two boxes. If the coloring is valid, the two colors differ, every time. If the prover cheated, at least one edge is bad, and the verifier has some chance of pointing straight at it ^[3].

sequenceDiagram
participant P as Prover
participant V as Verifier
Note over P: Knows a valid 3-coloring of graph G
P->>V: Lock each vertex color in a commitment, colors randomly permuted
V->>P: Challenge with one random edge
P->>V: Open the two commitments at that edge only
Note over V: Accept iff the two revealed colors differ
Note over V: One bad edge is caught with probability at least 1 over the edge count

One round barely convinces: a cheating prover slips past most of the time. But repeat the game hundreds of times, reshuffling the colors on each round, and the odds of a fraud surviving every challenge collapse toward zero -- while the verifier still learns only "yes, a valid coloring exists," because each round reveals two mismatched colors under a fresh permutation. Soundness is bought by repetition; zero knowledge is preserved by re-randomization. The apparent paradox from Section 1 is resolved: the transcript convinces precisely because a simulator could have produced it.

GMW proved that any computation's correctness could be proven in zero knowledge. It also left the idea thoroughly impractical: interactive, demanding a live verifier and many rounds; bespoke, hand-built for each statement; and often as expensive to check as to run. Nearly every advance for the next forty years is an attempt to knock down one of those three walls. The first to fall was interaction.

3. Removing the Verifier, Shrinking the Proof#

The first wall is the live verifier. A GMW proof is a conversation, and a conversation is perishable: you cannot post it, archive it, or let a third party check it tomorrow. For outsourced computation -- exactly our cloud scenario -- that is fatal. Prover and verifier are rarely online together, and one proof ought to convince the whole world, not a single interlocutor.

Two escapes from interaction appeared almost at once, and the field still runs on both.

The first is a shortcut from Amos Fiat and Adi Shamir in 1986 ^[4]. In a public-coin protocol the verifier's only real job is to supply unpredictable random challenges. So replace the verifier: derive each challenge by hashing everything the prover has committed to so far. If the hash behaves like a truly random function, the prover cannot predict or steer the challenge, because the prover must commit before the hash exists. The whole conversation collapses into one message the prover computes alone and anyone can recheck.

// Replace the verifier's random challenge with a hash of the transcript.
// (Toy hash for illustration -- real systems use SHA-256 or Poseidon
//  playing the role of a random oracle.)
function toyHash(str) {
let h = 2166136261 >>> 0;                 // FNV-1a, 32-bit
for (const ch of str) {
  h ^= ch.charCodeAt(0);
  h = Math.imul(h, 16777619) >>> 0;
}
return h >>> 0;
}

const statement  = "graph G is 3-colorable";
const commitment = "sealed boxes: c1,c2,...,cn";   // prover's first message

// The challenge is DERIVED from the transcript, not asked for interactively.
const challenge = toyHash(statement + "|" + commitment) % 1000;
console.log("Prover derives challenge (edge index):", challenge);

// Any verifier, later and offline, recomputes the identical challenge.
const recomputed = toyHash(statement + "|" + commitment) % 1000;
console.log("Verifier recomputes the same challenge:", recomputed === challenge);
console.log("No live verifier needed -- the proof can be posted and checked by anyone.");

The subtlety that will bite later: the hash must absorb the statement and every commitment. Leave an input out and a cheating prover can grind for a favorable challenge -- the "weak Fiat-Shamir" flaw that the sibling break-post on how these systems fail takes apart in detail. Done correctly, Fiat-Shamir is the most-used bridge from interactive proof to publishable certificate in cryptography.

The second escape, from Manuel Blum, Paul Feldman, and Silvio Micali in 1988, stays rigorous without a random oracle by leaning on a common reference string: a short, honestly generated string handed to both parties in advance ^[5]. Given it, a single message suffices. That CRS is the ancestor of every structured reference string and every "trusted setup ceremony" in the SNARKs to come -- and the object whose compromise Section 8 will scrutinize.

Non-interactivity solved posting and storing. It did nothing for size. A proof as long as the computation is useless for delegation: if checking costs as much as running, why outsource at all? The fix is succinctness, and it arrived in two steps.

In 1992 Joe Kilian built the first succinct interactive argument: commit to a long probabilistically checkable proof with a Merkle tree, then reveal only the few symbols the verifier queries, for communication polylogarithmic in the work ^[7]. Two years later Silvio Micali applied Fiat-Shamir to Kilian's protocol and produced the first non-interactive succinct argument, his "CS proofs" -- the direct ancestor of the SNARK ^[8].

Underneath much of what follows sits one more engine from this era: the sum-check protocol of Lund, Fortnow, Karloff, and Nisan, and its circuit-shaped descendant GKR, which reduce a claim about a giant sum of a low-degree polynomial to a handful of single-point checks ^{[9] [10]}. It will return, decades later, as the fastest known way to prove.

By the mid-1990s the theory was astonishing and the practice was nonexistent. Two walls remained. The PCP machinery underlying succinctness carried constants so large that no one could implement it. And every proof was still hand-crafted per statement: to prove a new computation, a cryptographer sat down and designed a new protocol.

Breaking both walls needed a different bridge: a way to turn any computation, mechanically, into a single algebraic statement a proof system could attest. Two more rows have quietly joined our ledger, non-interactive and then succinct, but they still wear the goal row's asterisk: bespoke, and barely buildable. The generation that removed the asterisk is where the field turns practical.

4. The Evolution: Making It General and Cheap to Check#

The logjam broke with one idea: stop proving statements and start proving polynomials. Everything in this section is a variation on that move, and each variation ends in the specific failure that forced the next.

flowchart TD
G0["Gen 0: NP witness, reveals everything"] --> G1["Gen 1: Interactive ZK, 1985. Wall: interactive"]
G1 --> G2["Gen 2: Non-interactive, 1986. Wall: large proofs"]
G2 --> G3["Gen 3: Succinct arguments, 1992. Wall: bespoke"]
G3 --> G4["Gen 4: Arithmetized SNARKs, 2013. Wall: trusted setup"]
G4 --> G5["Gen 5: Universal and transparent, 2018. Wall: slow prover"]
G5 --> G6["Gen 6: Folding and lookups, 2021. Wall: per-circuit"]
G6 --> G7["Gen 7: The zkVM, 2023. Any program"]
G7 --> G8["Gen 8: zkML on a committed model"]

Arithmetization: a computation becomes one equation#

In 2013 Rosario Gennaro, Craig Gentry, Bryan Parno, and Mariana Raykova showed how to compile a computation into a single algebraic statement without the impractical PCP machinery ^[11]. Their Quadratic Arithmetic Programs unroll a program into an arithmetic circuit of additions and multiplications, express that circuit as a Rank-1 Constraint System, then interpolate the whole thing into one polynomial-divisibility identity. The claim "I executed this program correctly" becomes the claim "this polynomial is divisible by that one."

Later the same year, Pinocchio turned the theory into a working system: a proof of just 288 bytes, verified in about 10 milliseconds, and -- for the first time in a general-purpose system -- checking a computation cost less than running it ^[12].

flowchart TD
A["Program: compute y from input x and witness w"] --> B["Arithmetic circuit of add and multiply gates"]
B --> C["R1CS: matrices A, B, C encoding every gate"]
C --> D["Interpolate to polynomials, one divisibility identity"]
D --> E["Commit to the witness polynomials"]
E --> F{"Identity holds at a random point?"}
F -->|"yes"| G["Accept: computation correct"]
F -->|"no"| H["Reject"]

Why does checking one random point suffice? Because a wrong computation produces a wrong polynomial, and two different low-degree polynomials can agree at only a few points. Evaluate at a point the prover cannot predict, and a lie is exposed with overwhelming probability. This is the Schwartz-Zippel intuition, and it is the reason a billion-step execution collapses to spot-checking a handful of numbers.

// A wrong low-degree polynomial betrays itself at a random point.
const p = 97;                          // a small prime field, for illustration

// The honest computation, encoded as a degree-3 polynomial C(x).
const C = x => (3*x*x*x + 2*x + 7) % p;

// A cheating prover hand-tunes a DIFFERENT polynomial that still
// matches C at x = 5 -- the one point they hope will be checked.
const Cheat = x => (C(x) + (x - 5)) % p;    // equals C only when x === 5

console.log("At the hoped-for point x=5, honest and cheat agree:", C(5) === Cheat(5));

// The verifier instead picks the evaluation point at RANDOM.
let caught = 0;
const trials = 10;
for (let i = 0; i < trials; i++) {
const r = Math.floor(Math.random() * p);
if ((((C(r) - Cheat(r)) % p) + p) % p !== 0) caught++;
}
console.log("Random checks that caught the cheat: " + caught + " out of " + trials);
// Two different degree-d polynomials agree at most d of p points,
// so one random evaluation exposes the lie with probability about 1 - d/p.

Pinocchio was a breakthrough, but it inherited two burdens. Every distinct program needed its own trusted setup, complete with toxic waste, and the prover was heavy. The secret randomness sampled to build a structured reference string -- the "powers of tau" -- is called toxic waste. Anyone who keeps it can forge proofs for that circuit forever, which is why ceremonies destroy it through a multi-party computation that stays sound as long as a single participant was honest.

Minimal proofs, then universal setup#

In 2016 Jens Groth pushed the pairing-based proof down to three group elements, roughly 128 to 200 bytes, verified by a single pairing-product check in constant time ^[13]. For years that was the smallest practical pairing-based proof, and Groth16 remains the constant-size gold standard and the final artifact of many systems today. Its cost was unchanged, though: a fresh per-circuit ceremony for every program, and no defense against a quantum computer.

The ceremony problem was an operational nightmare -- a new trusted setup for every program is a governance disaster. PLONK, in 2019, fixed it with a universal and updatable structured reference string: one ceremony serves every circuit up to a size bound, and any newcomer can update it, keeping it sound as long as one contributor stayed honest ^[14]. Sonic had introduced the universal-SRS idea and Marlin developed it in parallel ^{[15] [16]}. The remaining catch: the setup was still structured, still built on elliptic-curve assumptions, and still not post-quantum.

Transparency: dropping the ceremony entirely#

The trusted setup was the field's biggest trust liability, so the next generation removed it, three lines doing so differently. Bulletproofs, in 2018, gave transparent proofs whose size grows only logarithmically -- no setup at all ^[17]. But its verifier does linear work, so Bulletproofs is not succinct. Bulletproofs are transparent and their proofs shrink logarithmically, yet the verifier's cost grows linearly with the statement. Perfect for the short range proofs inside confidential transactions; the wrong tool for a million-step program, where linear verification defeats the entire point of delegating.

STARKs, also 2018, took the other road: hash-based commitments and the FRI low-degree test yield transparent, scalable proofs that are plausibly post-quantum, at the price of larger proofs measured in tens to hundreds of kilobytes ^{[18] [19]}. Halo added transparent recursion, later the backbone of Halo2 and the zkML tool EZKL ^{[20] [21]}; Spartan delivered a transparent sum-check SNARK ^[22].

This is the payoff behind the discipline from Section 3. Transparency proves that a trusted setup was never intrinsic to succinct arguments -- it was a feature of specific constructions. But notice what transparency did not remove: the random oracle. You still need a setup, just not a trusted one.

Amortizing the prover#

By 2021 the prover, not the proof, was the bottleneck, and two ideas began to chip at it. Nova introduced folding schemes: instead of proving each step of a repeated computation and recursively verifying each proof, fold two instances of the same relation into one of the same size, deferring the expensive proving to the very end, at a per-step cost of about two group scalar multiplications ^[23]. Lasso, in 2023, turned enormous lookup tables -- larger than $2^{128}$ entries -- into cheap arguments by never materializing them, charging the prover only for the entries actually used ^[24].

A wrong computation is a wrong polynomial, and a wrong polynomial cannot hide at a random point. Everything after 2013 is engineering around that one fact.

Watch how far the ledger has come:

Every branch above shared one unsolved problem and one unspoken assumption. The problem was the prover's cost. The assumption was that someone still had to hand-build a circuit for every new computation. Folding and lookups made a step cheaper to prove, but you still had to describe your computation as constraints by hand. The obvious, audacious question hangs over the whole table: what if one circuit could verify them all?

5. The Breakthrough: The zkVM#

The answer inverts the whole problem. For forty years the craft was: given a computation, build a circuit that proves that computation. The zkVM asks the opposite. Build one circuit that verifies the execution trace of a general-purpose CPU, then compile any program you like to that CPU. Prove the processor, and you have proven every program that runs on it.

Concretely, you arithmetize an execution trace. A processor's run is a long table: at each step, the contents of its registers, the memory it touched, and the instruction it executed. Constrain that table so every row follows legally from the one before -- each instruction updating registers and memory exactly as the instruction set specifies -- and a valid trace is a proof that the program ran correctly. The flagship instruction set is RISC-V, an open, clean, deliberately small design that is a pleasure to arithmetize.

The hard part is not the arithmetic. Registers are easy; memory is the challenge. A program reads and writes RAM in an unpredictable order, and the proof must guarantee that every read returns the value most recently written to that address, without replaying the whole memory. This is the job of a memory-checking argument, a line running from Spice through to the 2025 designs ^[28]. Solve memory checking cheaply and the zkVM becomes tractable.

The decisive trick is the one foreshadowed in Section 4. A CPU instruction is a function: given an opcode and its operands, it produces a result and a next state. That is precisely a lookup into a table of the instruction set's behavior.

In 2023 Jolt made this the entire design: express almost every RISC-V step as a lookup into a single gigantic table -- conceptually larger than $2^{128}$ entries, and never materialized -- committing to only about six field elements per step ^[29]. Barry Whitehat had named the goal the "lookup singularity" ^[30]; Lasso unlocked it and Jolt built the zkVM on top -- aim a lookup argument at an instruction set, and one circuit verifies any program's execution.

The zkVM turns verifiable computation into a compiler target. Instead of a cryptographer hand-crafting a circuit for each new statement, you write Rust, compile it to RISC-V, run it, and emit a receipt. Generality stops being artisanal and becomes, roughly, cargo build. That is the moment "prove any computation" changed from a theorem into a toolchain.

This is not a whiteboard idea. RISC Zero and SP1 are production RISC-V zkVMs available today: compile ordinary Rust, run it inside the zkVM, and receive a verifiable receipt attesting "I ran this exact program and got this output" ^{[31] [32]}. The receipt carries a public journal of whatever outputs you chose to reveal and a cryptographic seal over the execution; the private inputs never appear in it.

flowchart TD
A["Rust or C program"] --> B["Compile to RISC-V instructions"]
B --> C["Execute, recording the full execution trace"]
C --> D["Per-step lookups: opcode and operands map to result"]
D --> E["Prove the trace in a transparent STARK, about 200 kB"]
E --> F["Wrap into a Groth16 receipt, about 200 bytes"]
F --> G["On-chain verifier checks in constant time"]
F -.->|"last-mile trusted setup"| H["Soundness caveat, not privacy"]

One more move makes this practical on a blockchain, and it matters precisely because it reintroduces a cost we thought we had escaped. A zkVM proves a huge execution most cheaply in a transparent STARK -- no trusted setup, scaling to enormous traces -- but a STARK proof is large, around 200 kilobytes, and expensive to verify on-chain.

So systems wrap it: prove the big computation in the STARK, then prove that the STARK proof is valid inside a small Groth16 circuit, yielding a final receipt of roughly 200 bytes that verifies on-chain in constant time ^[33]. RISC Zero's pipeline does exactly this.

Read that trade carefully. The transparent inner proof needed no trusted setup, but the Groth16 wrapper does. Wrapping reintroduces a trusted setup at the last mile. This is a soundness property, not a privacy one: a compromised wrapping ceremony could let someone forge a receipt, yet it reveals nothing about anyone's private inputs. It is the ledger's "no trusted setup, never no setup" showing up one final time, now as a deliberate choice you make in exchange for a tiny on-chain proof.

Step back and see what the zkVM delivers. It is the thesis made fully concrete: prove that $f(x) = y$ for a real program $f$ and a private input $x$, revealing nothing about $x$, for any $f$ you can write in Rust. The forty-year march from "any NP statement, in principle" to "any program, by compiling it" is complete. Which leaves the only questions that matter next: how good is it, really, and what does it cost?

6. State of the Art: The Stack in 2026#

Modern verifiable computation is not one system; it is a stack. Every deployed proof is three decisions: an interactive-proof engine (how the computation is reduced to a polynomial claim), a polynomial commitment scheme (how that claim is bound and later opened), and a front-end (how the computation becomes constraints at all). Fix those three and you have named a system. The production zkVMs differ mainly in the first two.

RISC Zero proves each segment of a run in a STARK, recursively joins the segments, and compresses the result into a Groth16 receipt for the chain ^[33]. Its strength is maturity: unbounded programs through continuations, and clean proof composition.

SP1 began on a STARK stack, then in 2025 rebuilt its engine from the ground up. SP1 Hypercube swaps univariate STARKs for a multilinear system -- a purpose-built Jagged polynomial commitment plus a heavily optimized LogUp-GKR lookup ^{[32] [34]}.

The payoff is the field's most arresting benchmark: SP1 Hypercube proves 93% of Ethereum mainnet blocks in under 12 seconds, averaging 10.3 seconds, on a cluster of about 160 RTX 4090 GPUs ^[34]. This is the first credible "real-time Ethereum proving." Read the caveat as loudly as the headline: it closes the gap for one heavily engineered workload, not for arbitrary programs.

Jolt takes the lookup-singularity design to its conclusion -- nearly every step a lookup, proved with sum-check over an elliptic-curve commitment -- and is, by a16z's assessment, currently the fastest RISC-V zkVM, with roughly a further 3x expected as its Twist and Shout memory-checking arguments land ^{[29] [35] [36]}.

The headline insight from Setty and Thaler is easy to miss, because it contradicts the popular framing. The primary lever on prover speed is not "hashing versus elliptic curves." It is the sum-check and multilinear axis. Jolt, using elliptic-curve commitments, outruns STARK systems that use hashes -- because it uses sum-check. That is why both SP1 Hypercube and Jolt converged on multilinear engines ^[35].

The same stack, aimed at a neural network, becomes zkML. The move is simple to state: commit to the model's weights in advance, then prove that this committed model, on some input, produced a claimed output -- revealing nothing about the weights, and optionally nothing about the input.

flowchart TD
W["Model weights"] --> C["Commit: hash or polynomial-commit the weights"]
C --> CM["Public commitment to the model"]
X["Private input"] --> P["Prover runs inference on the committed model"]
CM --> P
P --> R["Receipt: this committed model produced output y"]
R --> V["Verifier checks in milliseconds"]
W -.->|"weights never revealed"| V

Three systems mark the range. zkCNN proved real convolutional inference in 2021: on VGG-16, 88.3 seconds to prove, a 341 kilobyte proof, and 59.3 milliseconds to verify ^[37]. EZKL made it turnkey, compiling ONNX models exported from PyTorch or TensorFlow into Halo2 circuits with the model committed into the circuit ^{[38] [39]}. And zkLLM reached transformer scale in 2024, with a parallel lookup argument and a bespoke attention proof, proving inference for a 13-billion-parameter model in under about 15 minutes with a proof under 200 kilobytes ^[40].

The 2025 frontier -- vendor-reported systems such as DeepProve claiming the first zero-knowledge proof of a full LLM inference -- suggests the cost is falling fast, though frontier-scale, real-time proving is not here yet ^[41].

Say precisely what a zkML receipt means, because this is where hype does the most damage. It attests execution integrity of a committed model -- that specific, pre-committed weights ran faithfully on the input -- and nothing more. It says nothing about whether the model is accurate, fair, safe, or well-trained. Proving that the machine ran is not proving that the machine deserves your trust.

The ledger is now complete -- forty years in one table:

"Proving correct execution of a program can be hundreds of thousands of times slower than running it natively." ^[44]

The systems are astonishing. Each one also quietly hands back a trusted setup at the last mile, runs its prover many thousands of times slower than native, and, for AI, proves only that a committed model ran. Which of those are fixable engineering and which are laws? Start with the design space almost everyone gets wrong.

7. The SNARK/STARK Design Space, Honestly#

You have heard "SNARK versus STARK" framed as a rivalry, a cage match between two camps. It is nothing of the sort. It is a single design space with two independent knobs -- the setup and the cryptographic basis -- and getting this right dissolves three popular misconceptions at once. Recall the stack from the previous section:

flowchart TD
FE["Front-end: hand circuit, zkVM, or ML compiler"] --> PIOP["Interactive proof: sum-check, AIR, or R1CS"]
PIOP --> PCS["Polynomial commitment: KZG, FRI, IPA, or Ligero"]
PCS --> FSh["Fiat-Shamir removes interaction"]
FSh --> PR["Non-interactive proof or receipt"]

The first knob is the setup. It ranges from a per-circuit trusted ceremony (Groth16), through a universal, updatable ceremony (PLONK), to fully transparent, needing only public randomness (STARKs, Bulletproofs, Spartan, and Halo2 in its inner-product-argument instantiation -- though Halo2's common KZG variant uses a universal setup instead). The second knob is the cryptographic basis: elliptic-curve pairings, which give the smallest proofs but fall to a quantum computer, or collision-resistant hashes, which give larger proofs but are plausibly post-quantum. Every system is a setting of these two knobs, plus an engine choice.

With that framing, three myths evaporate. All SNARKs need a trusted setup? No -- trusted setup is a property of specific constructions, not of the SNARK class, and transparent SNARKs exist. A STARK is a fundamentally different animal from a SNARK? It is terminology: a STARK is a Scalable Transparent ARgument of Knowledge, which is to say a transparent, scalable SNARK. They compete? In practice they compose -- the STARK-to-SNARK wrapping of Section 5 proves the big computation transparently, then wraps it in a pairing SNARK for a tiny on-chain artifact.

"The sum-check protocol is key to fast SNARK provers ... Jolt with elliptic curve commitments is currently the fastest RISC-V zkVM." ^[35]

One more piece of discipline. STARKs are plausibly post-quantum, and that word is load-bearing. Their security reduces to collision-resistant hashing, which no known quantum algorithm breaks -- but "no known attack" is a conjecture, not a theorem ^[18]. Pairing SNARKs are definitely not post-quantum, and any zkVM that wraps into Groth16 inherits that weakness at the final artifact, no matter how post-quantum the inner STARK was ^[13]. The primitive choice drives cost. STARKs pair best with arithmetization-friendly hashes like Poseidon, cheap to express as constraints ^[45], while zkLLM runs its commitments over the BLS12-381 elliptic curve ^[40]. Match the primitive to the proof system, or pay for the mismatch in the prover.

Zero knowledge is also not the only way to trust a computation you did not run. It sits within a family of trust models, each striking a different bargain.

So the design space is a set of trade-offs, not a winner, and each proof you deploy is an honest declaration of which knobs you turned and which trust you kept. But every trade here is bounded by something deeper than engineering.

8. Theoretical Limits#

Some walls are not waiting for a cleverer engineer. They are theorems, and they explain why the honest phrasings in this article keep hedging.

Start with the deepest one, the formal root of "no trusted setup, never no setup." In 1994 Oded Goldreich and Yair Oren proved that non-interactive zero knowledge in the plain model -- no shared string, no random oracle -- exists only for languages already in BPP, the class of problems a randomized algorithm can simply decide on its own ^[6]. If a problem is genuinely hard, you cannot prove it in non-interactive zero knowledge from nothing. You need a setup: a common reference string, or a random oracle. Transparency removes the trust in the setup; it never removes the setup.

The second theorem explains why every practical SNARK rests on an idealization. In 2011 Craig Gentry and Daniel Wichs showed that no black-box reduction can prove a succinct non-interactive argument for all of NP sound under any falsifiable assumption -- the ordinary kind you can state as a game an adversary either wins or loses ^[46]. The consequence is unavoidable: real SNARKs lean on the random-oracle model, or on non-falsifiable "knowledge" assumptions such as the Algebraic Group Model. That is not carelessness. It is a direct response to an impossibility result.

The third is why Bulletproofs never took over. Recent work reduces a proof system's verifier cost to the communication complexity of its polynomial commitment, and the bounds are sharp: for a statement of size $N$, the Bulletproofs commitment needs $\Omega(N)$ work, Hyrax $\Omega(\sqrt N)$, Dory $\Omega(\log N)$ ^[47]. That is rigorous evidence the Bulletproofs verifier cannot be made sublinear -- the exact reason it settled into the confidential-transaction niche instead of superseding the pairing and STARK lines.

Put those together and a structural fact emerges: verification is cheap -- constant or polylogarithmic, milliseconds and a few hundred bytes -- and cheap forever, while the prover pays the whole cost. This asymmetry is not a passing state of the engineering; it is built into what a succinct argument is.

The asymmetry is permanent. Verification stays cheap forever -- milliseconds, a few hundred bytes -- while the prover pays the entire cost, by theorems rather than by accident. And for AI there is a second permanent boundary: a zkML receipt attests that a committed model executed faithfully, never that the model is correct. You can prove the machine ran; you cannot, from the proof alone, prove that what it ran deserves your trust.

A subtler limit bites zkML specifically. A neural network computes in floating point; a proof computes in a finite field. To prove an inference you must quantize the model into integers modulo a prime, and quantization can change the answer. The receipt then attests the quantized field computation, which need not match what the native float model would have produced.

// A proof runs in a finite field; the model runs in floats.
// Quantize to integers mod p and the results can diverge.
const p = 2147483647;   // prime field, 2^31 - 1
const SCALE = 1000;     // fixed-point: 3 decimal places

const w = [0.001, 0.002, -0.0015, 0.0007];   // small weights
const x = [1200,  -300,   950,     4096];     // activations

// Native floating-point dot product.
let floatDot = 0;
for (let i = 0; i < w.length; i++) floatDot += w[i] * x[i];

// Field / fixed-point dot product: quantize the weights, multiply as
// integers, reduce mod p, then de-scale to compare.
let fieldDot = 0;
for (let i = 0; i < w.length; i++) {
const wq = Math.round(w[i] * SCALE);        // quantized weight
fieldDot = (fieldDot + wq * x[i]) % p;
}
const fieldAsReal = fieldDot / SCALE;

console.log("Float result:", floatDot.toFixed(6));
console.log("Field result:", fieldAsReal.toFixed(6));
console.log("They disagree by:", Math.abs(floatDot - fieldAsReal).toFixed(6));
// The proof certifies the FIELD computation. Quantization is a modeling
// choice the receipt cannot see past.

And the post-quantum promise, once more with precision: STARK security rests on collision-resistant hashing surviving quantum attack. No one has broken it, and no one has proven it unbreakable. It is a conjecture, and long-lived proofs should be built in full knowledge of that ^[18].

Here is the twist that turns humility back into ambition. The gap is not in the asymptotics. We already have, on paper, linear-prover, polylogarithmic-verifier, sublinear-proof arguments. The gap is a brutal constant -- the many-thousandfold prover overhead. An asymptotic wall is a theorem you must respect. A large constant is a problem you can attack. And the field is attacking it on every front at once.

9. Open Problems#

If the gap is a constant, the frontier is a race to shrink it -- and the race runs on several tracks at once.

The prover overhead for general computation. This is the headline number, and it deserves a precise range rather than a slogan. SP1's public zkVM benchmark reports CPU proving between 300,000 and 13,000,000 times slower than native, the upper end driven by tiny-input outliers such as a bare SHA-256 ^[48]. a16z's rounder figure, "hundreds of thousands of times slower than running it natively," lands in the same territory ^[44]. Take the general range as roughly ten thousand to ten million times, and never quote a single universal multiplier: it depends entirely on the workload.

Every technique in this article aims at this number: sum-check and multilinear engines, folding, cheaper memory checking (Twist and Shout, over 10x cheaper than prior lookups ^[36]), binary-field commitments ^[49], and raw hardware -- FPGA and ASIC accelerators for the multi-scalar-multiplication and transform primitives report hundreds-fold speedups ^{[42] [43]}.

zkML at LLM scale, in real time, with fidelity. zkLLM proves a 13-billion-parameter inference in about 15 minutes ^[40]; frontier models are far larger, and 15 minutes is not real time. Worse, the field-versus-float fidelity gap from Section 8 means the receipt certifies a quantized model. Closing scale, latency, and fidelity together is open.

Formal verification of the provers themselves. The theorems in Section 8 bound what a correct system can do. They say nothing about implementation bugs, and zkVMs are large, subtle software. A soundness bug -- most notoriously the "weak Fiat-Shamir" class, where a prover fails to hash all the public inputs -- silently breaks the whole guarantee while every proof still looks valid. This soundness-bug class, including the "Frozen Heart" vulnerabilities, is the subject of the sibling break-post on how zero-knowledge proofs fail. This constructive post only points at the door; the break-post walks through it. Delivering a fully formally verified zkVM -- verified engine soundness, commitment binding, Fiat-Shamir security, and a proof that the constraints actually match the CPU's semantics -- is years out ^[44].

Is transparent, post-quantum succinctness a theorem? Today it is a conjecture: STARK security rests on the belief that no efficient quantum attack on the hash exists ^[18]. Turning that belief into a proof, or finding a lattice-based alternative, is unsolved.

The optimality triple. The prize that would collapse the whole design space is a single construction with a linear-time prover of small constant, a constant-size proof, and a constant or logarithmic verifier -- transparent and post-quantum, all at once. No system achieves it. Pairing SNARKs give the proof and verifier ideal but sacrifice transparency and post-quantum safety; STARKs give transparency and a post-quantum hedge but larger proofs; sum-check systems give the fastest prover but commitment-dependent proofs. Wrapping composes two ideals at the cost of a last-mile trusted setup, and no one has yet composed all of them into one.

None of these is solved. All of them are moving -- some by a factor per year. Which brings us back to the receipt we started with, and to the one question left: knowing everything we now know, what can that receipt actually promise, and what can it not?

10. A Practitioner's Guide#

Strip away the theory. Here is how you actually ship verifiable computation in 2026. There are three paths, and the choice is mostly how much of your computation must be proven and how much engineering you can spend.

The zkVM path is the default, and it is remarkably easy. Write your logic in Rust, compile it to RISC-V, run it inside RISC Zero, SP1, or Jolt, and get back a receipt you can verify anywhere ^{[31] [32] [29]}. No circuit design, no cryptography by hand. You choose the system by priority: SP1 Hypercube for rollup and real-time Ethereum latency ^[34], Jolt for raw prover speed ^[35], RISC Zero for mature composition and unbounded programs ^[33].

The hand-rolled circuit path buys efficiency with engineering. When one specific computation is your hot path and you need the smallest, fastest proof, drop to a circuit framework -- Circom, Halo2, gnark, Plonky3, or a folding library like Nova ^{[39] [52]}. You express the computation as constraints yourself. The reward is the best constants in the field; the cost is genuine cryptographic engineering and a far larger surface for the soundness bugs of Section 9.

The zkML path proves inference on a committed model. For small and moderate models, EZKL is the turnkey route: export to ONNX, commit the model into a Halo2 circuit, and prove "this committed model, on this input, produced this output" ^{[38] [53]}. For transformer scale, zkLLM and the 2025 vendor systems push the frontier ^{[54] [41]}. In every case, be exact about what the receipt attests -- a committed model's faithful execution -- and about what it does not: accuracy, fairness, or safety.

Behind all three sits one trade-off you cannot escape: a triangle of proof size, proving time, and verification cost. Push one corner down and another rises. A transparent STARK gives cheap, setup-free proving but a large proof; wrap it into a pairing SNARK and the proof shrinks to a couple hundred bytes for cheap on-chain verification, at the cost of extra proving time and a last-mile trusted setup. There is only the configuration that fits your deployment. In production you rarely run the prover yourself. Managed proving services -- RISC Zero's Bonsai, Succinct's network, and Lagrange for zkML -- rent the GPU clusters and hand back the receipt ^{[31] [32] [41]}.

Sometimes the honest answer is that zero knowledge is the wrong tool today. If you need only integrity, not privacy, at frontier model scale, a trusted execution environment or an optimistic proof will often serve better than a zkML prover that runs for fifteen minutes. Pick the trust model that matches the guarantee you actually need, not the most fashionable one.

The tools are real and the guarantees are precise -- as long as you state exactly what the receipt proves. So let us state it, one last time, with everything we now know.

11. Frequently Asked Questions#

12. Trust Me, I Ran It Right, Revisited#

Return to where we began. A cloud service runs a model you cannot see, on data you will not share, and returns an answer. Can you check it? The answer is now yes, and you can say exactly how.

Interactive proofs made it possible in 1985: Goldwasser, Micali, and Rackoff showed that a transcript could convince you of a truth while a simulator could have faked it, so it carried no secret ^[1]. Non-interactivity and succinct arguments made it portable and cheap to check between 1986 and 1994, as Fiat-Shamir and the common reference string removed the live verifier and Kilian and Micali made the proof shorter than the work ^{[4] [8]}. Arithmetization made it general from 2013 to 2016, when a computation became one polynomial identity and a single random point caught every lie ^{[11] [13]}.

The zkVM made it arbitrary program execution in 2023: one circuit verifies a CPU, so you compile Rust and emit a receipt ^[29]. And zkML aimed the whole stack at a committed model ^[40].

That is the thesis, fully earned: a prover can convince a verifier that a computation ran correctly while revealing nothing about the private inputs. The prover hands over a few-kilobyte receipt -- "I ran this exact program, or this committed model, and got this output" -- checkable in milliseconds, at a prover cost that is real and often enormous.

But hold onto the boundary this article kept drawing. The receipt proves the machine ran faithfully. It does not prove that what the machine ran deserves your trust. A committed model can be biased; a correctly proven program can be a correctly proven mistake. Soundness is not wisdom. That gap -- between a valid proof and a trustworthy one -- is exactly where proofs break, which is the subject of the sibling break-post on how zero-knowledge proofs fail, and the thread the next part of this series takes up.

Nothing was decrypted, and nothing needed to be. The prover simply proved it did the work -- and now you can check.