Questions
- Where would I actually use this?
- How does an execution trace work if you don’t know the next row?
- Where do I start learning?
- Why only addition and multiplication?
- How would mObywatel work with ZK?
- Can I use bounds larger than 8 bits?
- Can you formally prove a circuit is correct, e.g. with Lean?
- Is this a SNARK or a STARK?
- ZK in electronic voting
- Is ZK verification cost-effective on-chain?
#1 “I’m missing a real use case. I don’t know where I’d use this.”
Two people asked for the same thing: show me a real-world example, not an abstract circuit.
You’re checking into a hotel. They need to verify your ID belongs to an adult. In Poland there are ID cards issued to minors (dowód osobisty dla osoby niepełnoletniej), and you can’t tell from the document number alone whether the holder is 18+.
With a ZK proof, the hotel verifies: “this person has a valid government-issued ID, and the date of birth in that ID satisfies age >= 18.” The hotel sees yes or no. No date of birth, no name, no document number.
Under the hood this is a range check: prove that (current_date – date_of_birth) >= 6570 days without revealing date_of_birth. Range checks are one of the most basic operations you can build in a circuit (see question #6 for how they work), and age verification is one of the most practical applications.
Technically: you have your digital ID (e-dowód) on your phone. At check-in the phone generates a ZK proof locally and presents it as a QR code. The hotel scans the code, verifies the proof, gets the yes/no answer. Everything happens locally, no server required.
This isn’t theoretical. The EU Digital Identity Wallet (eIDAS 2.0) is designed to support exactly this kind of selective disclosure. mObywatel 3.0 is planned for late 2026 as part of this framework (more on mObywatel in question #5).
#2 “How can I know what’s in the next row of the execution trace if I’m only at the current one?”
This is the most common confusion: people think proving IS executing. It’s not. These are two separate steps.
First, you do the execution. The prover takes the program, runs it on the inputs, and records every intermediate value into a table. That table is the execution trace. At this point the prover knows everything: every input, every output, every step.
Then you do the proving. The prover takes the completed trace with all constraints and turns it into a proof. You don’t need to “know the next row” during proving, because the full trace is already there.
Here’s what one looks like. Focus on rows 0-1 (the subtraction gates) and the Notes column on the right. The rest is bit decomposition, same idea repeated for each bound.
Row │Gate/Formulas│ Col A │ Col B │ Col C │ Notes ─────┼─────────────┼───────────┼───────────┼────────────┼───────────────────────── 0 │ subtraction │ 42 │ 10 │ 32 │ secret - lo = diff_lo 1 │ subtraction │ 100 │ 42 │ 58 │ hi - secret = diff_hi 2 │ bit_decomp │ 32 │ 0 │ │ 3 │ bit_decomp │ 16 │ 0 │ │ 4 │ bit_decomp │ 8 │ 0 │ │ 5 │ bit_decomp │ 4 │ 0 │ │ 6 │ bit_decomp │ 2 │ 0 │ │ 7 │ bit_decomp │ 1 │ 1 │ │ 8 │ bit_decomp │ 0 │ 0 │ │ 9 │ bit_decomp │ 0 │ 0 │ │ 10 │ │ 0 │ │ │ Col A must be zero! 11 │ bit_decomp │ 58 │ 0 │ │ 12 │ bit_decomp │ 29 │ 1 │ │ 13 │ bit_decomp │ 14 │ 0 │ │ 14 │ bit_decomp │ 7 │ 1 │ │ 15 │ bit_decomp │ 3 │ 1 │ │ 16 │ bit_decomp │ 1 │ 1 │ │ 17 │ bit_decomp │ 0 │ 0 │ │ 18 │ bit_decomp │ 0 │ 0 │ │ 19 │ │ 0 │ │ │ Col A must be zero!
Slide from my talk at the Kraków Rust meetup (27.02.2026). This is the full execution trace for a range check: proving that 42 is between 10 and 100 by decomposing the differences into bits. Every row is filled in BEFORE the proof starts.
#3 “Do I need to learn the fundamentals first, and where?”
Best book to start: “Proofs, Arguments, and Zero-Knowledge” by Justin Thaler. People in the audience were taking photos when I showed it.
You don’t need to read the whole thing. Chapters 1-4 give you the foundation: randomized algorithms, interactive proofs, and the sum-check protocol. Polynomial commitments come later (chapters 14-16), but without the foundation from 1-4 the rest won’t make sense.
If you’d rather skip the book: my posts on rustarians.com start from zero (polynomials, roots of unity, execution traces) and include interactive code.
#4 “Why can’t I just use a comparison? Why only multiplication and addition?”
Because a circuit is not a program. In regular code you have if, else, comparisons, loops. In an arithmetic circuit the only building blocks are addition and multiplication over field elements.
In PLONKish systems like halo2 you can define custom gates that combine multiple additions and multiplications into a single constraint (e.g. a * (b + c) = d in one gate). But the building blocks are still the same: addition and multiplication. Nothing else.
Why no comparison? Because comparison is not a polynomial operation. You can’t write a < b as a polynomial equation. This isn’t just a finite field problem. Even over regular integers, a < b is not expressible as a polynomial. And every constraint ultimately has to be a polynomial, because that’s what fits into the polynomial commitment scheme that makes the proof work.
So you decompose comparisons into operations the circuit can express. For example, a < 256 becomes: check that a fits in 8 bits. Decompose a into bits (b0, b1, …, b7), check that each bit is 0 or 1 (bit * (1 - bit) == 0), and verify the sum b0 + 2*b1 + 4*b2 + ... + 128*b7 == a. All additions and multiplications.
#5 “How would mObywatel work with ZK?”
Same use case as question #1, but now the question is how to build it. You have a digital ID on your phone (mObywatel). You want to prove you’re 18+ without revealing your date of birth or any other personal data.
The prover (your phone) puts three things into the circuit: your certificate from mObywatel, the government’s public key, and the age constraint (age >= 18). The circuit verifies the signature on the certificate, extracts the date of birth, checks the constraint, and produces a proof.
The verifier (the hotel) takes three things: the proof, the government’s public key, and the same age constraint. That’s it. No certificate, no personal data, just the proof and the public inputs.
Implementation detail (you don’t need to know these algorithms, just the punchline): Schnorr or EdDSA signature verification in a ZK circuit costs ~10-11k constraints. RSA-2048 costs ~536k. That’s roughly 50x more. The choice of cryptographic primitives matters in ZK: pick the wrong ones and your proof size and proving time explode.
#6 “Can I use bounds larger than 8 bits in the example?”
Yes, but the cost grows linearly with the number of bits. 8 bits = 8 bit decomposition gates + 1 for the sum. And for a range check you need two decompositions: one for the lower bound, one for the upper bound. So 8-bit range = 2 x 8 bit decomposition gates. 16 bits = 2 x 16. 256 bits = 2 x 256.
For large ranges, bit decomposition gets expensive. You can use lookup tables instead: you have a table of allowed values and check whether your value is in the table. halo2 has built-in lookup tables, and for large ranges they’re faster than bit decomposition.
#7 “Can you formally prove a circuit is correct, e.g. with Lean?”
Yes, and this is not theory. People already do it on production circuits.
| Tool | Proof assistant | What it verified | Result |
|---|---|---|---|
| Halva (Nethermind) | Lean | Scroll’s Keccak-256 circuit | Found critical production bug |
| CertiPlonk (Nethermind) | Lean | PlonK protocol IOP | Formalized |
| sp1-lean (Succinct) | Lean | SP1 zkVM chips | Verified |
| CODA (UT Austin) | Coq | 77 circom circuits | Found 6 new vulnerabilities |
Lean has become the dominant proof assistant for ZK. For a comparison of frameworks, see this zkSecurity overview.
This is still expensive though. Each circuit needs a separate proof, and verifying a production circuit takes weeks or months.
What people do when they don’t have the budget for formal verification: property-based testing (generate random inputs and check the circuit behaves correctly) + MockProver in halo2 (catches under-constrained circuits during development). Property-based testing won’t catch all corner cases, but it’s much cheaper than a formal proof and catches most of the obvious bugs.
#8 “Is what you showed a SNARK or a STARK?”
It depends on the backend. halo2 is a proof system based on PLONKish arithmetization with polynomial commitments. Whether it’s a “SNARK” depends on which commitment scheme you plug in.
SNARK = Succinct Non-interactive ARgument of Knowledge. STARK = Scalable Transparent ARgument of Knowledge. Here’s how they compare:
| SNARK (KZG) | SNARK (IPA) | STARK | SNARK (lattice, Greyhound) | |
|---|---|---|---|---|
| Proof size | O(1), tiny | O(log n), small | Tens of KB | ~93 KB (Greyhound) |
| Verification | O(1), fast | O(n), slow | Medium | Slow (research stage) |
| Trusted setup | Yes | No | No (transparent) | No (transparent) |
| Quantum-safe | No | No | Yes, hash-based | Yes, lattice-based |
| Used by | Scroll, PSE | Original Halo | RISC Zero, StarkNet | Nobody yet (research) |
The IPA case is interesting: the proof is small, but verification is O(n). Technically not succinct. The original Halo paper avoids calling it a SNARK for this reason. In practice, the accumulation scheme amortizes that linear cost across recursive steps, so people call it a SNARK anyway.
STARKs have larger proofs but no trusted setup and are quantum-resistant (based on hashes, not elliptic curves). Prover is usually faster for large circuits. That’s why RISC Zero wraps its STARK proof in a Groth16 SNARK for on-chain verification: fast prover off-chain, small proof on-chain.
#9 “ZK in electronic voting”
This works through nullifiers. Each voter has a secret key, and from that key and the election ID they compute a hash called the nullifier. If someone tries to vote twice, the same nullifier already exists and the transaction gets rejected, but nobody can tell whose nullifier it is because hashing is one-way. Zcash uses the same mechanism for private transactions and Semaphore uses it for anonymous signaling.
An eVoting system with ZK works like this:
- Registration: each eligible voter gets a secret key. Their public key goes into a merkle tree on-chain.
- Voting: the voter creates a ZK proof: “my key is in the merkle tree of eligible voters, I vote for option X, here’s my nullifier.”
- Verification: the smart contract checks the proof, checks the nullifier hasn’t been used, records the vote.
- Counting: votes are public (option A: 47, option B: 53), but who voted for what is hidden.
Projects building this: MACI (by Privacy & Scaling Explorations / Ethereum Foundation, v3 on the way), Vocdoni (building a zkRollup for voting), and Semaphore-based voting.
The hard part is coercion resistance: how do you guarantee nobody is forcing you to vote a certain way? MACI solves this through key rotation. You can change your key after voting, so even if someone saw your vote, they don’t know if you changed it afterwards.
#10 “Is ZK verification cost-effective on-chain?”
Bottom line: verifying a ZK proof on Ethereum costs about $3. Generating the proof costs CPU time off-chain. Verification is cheap, proving is expensive.
The details: a Groth16 verification costs roughly 200k-300k gas (~181k + 6k per public input). The ecPairing precompile (EIP-1108) costs 34,000 * k + 45,000 gas where k is the number of pairings. At 5 gwei and ETH at $2,500, that works out to about $3 per verification.
When ZK makes economic sense:
- The computation is expensive on-chain but cheap off-chain (e.g. batch processing 1000 transactions, proved with a single proof)
- Privacy has value (user pays a premium for anonymity)
- Regulations require privacy (GDPR, personal data)
When ZK does not make sense:
- Simple computations (cheaper to execute directly)
- You don’t need privacy or compression
- Latency is critical (proving takes seconds to minutes)
Next Up
I’m turning the meetup demo into a full interactive post: building a range check circuit in halo2, step by step, with runnable code. If you want to go from “I get the concept” to “I can write this,” that’s the one.
Halo2 Cheat Sheet
API patterns, security pitfalls, fork comparison. One-page PDF reference for halo2 development.
Get the Cheat Sheet