Original version with full formatting on rustarians.com.
I gave a talk about halo2 at a Rust meetup in Krakow. The audience asked 10 questions I didn't have time to answer properly on stage, so I wrote them up.
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 (dowod osobisty dla osoby niepelnoletniej), 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.
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-dowod) 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.
(The original post includes the full execution trace table from my talk slides, showing a range check for proving that 42 is between 10 and 100 by decomposing the differences into bits.)
#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 building blocks are addition and multiplication over field elements. In PLONKish systems like halo2 you can define custom gates, which 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.
Why can't you just compare? You might think it's because finite fields have no ordering. But even over integers (which do have ordering), you'd have the same problem: comparison is not a polynomial operation. You can't write a < b as a polynomial equation. 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. You take a, decompose it into bits (b0, b1, ..., b7), check that each bit is 0 or 1 (bit * (1 - bit) == 0), and that the sum b0 + 2*b1 + 4*b2 + ... + 128*b7 == a. All additions and multiplications. The proof boils down to: the number can be expressed as a polynomial encoding its bits, and that polynomial satisfies all the constraints.
#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.
If I were building this, I'd use Schnorr or EdDSA for the document signature, not RSA. Schnorr verification in a ZK circuit costs ~10-11k constraints, RSA-2048 costs ~536k, 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.
Nethermind built Halva: a framework for formal verification of halo2 circuits in Lean. They used it on Scroll's Keccak-256 circuit and found a critical bug in production.
The same team built CertiPlonk for formalizing the PlonK protocol IOP in Lean, and sp1-lean together with Succinct Labs for verifying chips from SP1 zkVM.
CODA (from UT Austin) uses Coq and verified 77 existing circom circuits. They found 6 new vulnerabilities nobody had noticed before.
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 what you mean by SNARK. halo2 is a proof system based on PLONKish arithmetization with polynomial commitments. Whether it's a "SNARK" depends on which backend you use and how strictly you define the "S."
SNARK stands for Succinct Non-interactive ARgument of Knowledge. "Succinct" means small proof and fast verification. With KZG commitments (used by Scroll, PSE), halo2 is a SNARK: O(1) proof size, O(1) verification, but requires a trusted setup.
With IPA (Inner Product Argument), the proof is O(log n), which is small, but verification requires a linear-time multi-scalar multiplication: O(n). So the proof is succinct, but verification is not. The original Halo paper avoids calling it a SNARK, using "non-interactive argument of knowledge" instead. In practice, people call it a SNARK anyway because the proof is small and the accumulation scheme amortizes the linear verification cost across recursive steps. But strictly speaking: IPA verification is not succinct.
STARK (Scalable Transparent ARgument of Knowledge)
- Larger proof (tens of KB)
- No trusted setup (transparent)
- Quantum-resistant (based on hashes, not curves)
- Prover is usually faster for large circuits, but verification is slower and the proof is bigger. That's why RISC Zero wraps its STARK proof in a Groth16 SNARK for on-chain verification
#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 that do this: MACI (Minimal Anti-Collusion Infrastructure, concept by Vitalik, built by Privacy & Scaling Explorations / Ethereum Foundation, actively developed, v3 on the way), Vocdoni (building DAVINCI, a zkRollup for voting with recursive proofs), 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?"
General rule: verifying a ZK proof on-chain is cheap (compared to executing the full computation on-chain). Generating the proof is expensive (off-chain, on the prover's CPU/GPU).
Some numbers: a Groth16 verification on Ethereum costs roughly 200k-300k gas depending on the number of public inputs (formula: ~181k + 6k per public input). The underlying 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's roughly $3 per verification, less when gas is low.
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.
These are questions from the Krakow Rust meetup (27.02.2026). Original post on rustarians.com.
I'm running a free live session on March 17: From Polynomials to Proof in 60 Minutes. If you want to see a range check circuit built step by step, that's where it happens.
Questions? Found a bug? linkedin.com/in/adam-smolarek
Top comments (0)