The ZK Field Manual

The 2016 pairing-based preprocessing SNARK over R1CS: the proof is three group elements verified with a single pairing product equation. Requires a per-circuit setup on top of a reusable universal phase one.

Choose it whenA stable circuit verified on-chain at high frequency where gas is the binding constraint. Also the standard final compression layer for STARK-based systems.

A permutation-argument-based universal SNARK over a custom-gate arithmetisation — selector columns, copy constraints, optional lookup columns. One SRS serves all circuits up to a size bound. The most frequently occurring family among deployed on-chain verifiers.

Choose it whenGeneral-purpose circuits where churn is expected and a per-circuit ceremony would be painful, and where on-chain verification is required but need not be absolutely minimal.

AIR or PLONKish arithmetisation committed with Reed–Solomon codewords and Merkle trees, with FRI as the low-degree test. No trusted setup, hash-based, plausibly post-quantum. The workhorse of large-scale transparent proving: StarkWare's Stone and Stwo, the Plonky2 and Plonky3 toolkits, RISC Zero, Miden and ZKsync Airbender are all instances of this family, differing mainly in field, hash and lookup argument.

Choose it whenHigh-throughput server-side proving of large computations, especially zkVM execution, where a final wrapper handles settlement.

The same PLONKish frontend with two very different backends. The original uses an inner-product argument over a curve cycle and needs no trusted setup, with recursion via accumulation. The widely used Ethereum-oriented variant replaces IPA with KZG, giving constant-size proofs and a practical Solidity verifier — and a universal trusted setup. These are routinely conflated.

Choose it whenIPA: systems verified on a node rather than in a gas-metered contract, where trusted setup is unacceptable. KZG: EVM-verified application circuits and coprocessors needing expressive custom gates.

Folding reduces checking two instances of a relation to checking one, so each step of a long computation costs a couple of multi-scalar multiplications rather than an in-circuit SNARK verification. Variants add non-uniform steps and generalised constraint systems.

Choose it whenLong, repetitive computations and memory-constrained provers, where the final compression step happens once.

SNARKs over towers of binary fields, with a commitment that has no embedding overhead for tiny field elements. The current generation computes natively over 64-bit words with built-in bitwise and multiplication constraints, explicitly targeting client-side proving on commodity CPUs.

Choose it whenHash- and bitwise-heavy workloads, and client-side proving, for teams able to track a fast-moving codebase.

Two successors to FRI from the same research lineage. STIR reduces query complexity by recursively improving the rate of the tested code; WHIR builds on constrained Reed–Solomon codes to give very fast verification, and doubles as a polynomial commitment.

Choose it whenReplacing FRI where hash-based proof size or verifier latency is the binding constraint, for teams who will follow the literature.

The GKR protocol proves layered-circuit evaluation using sumcheck, with prover time linear in circuit size. Modern systems combine it with an error-correcting-code commitment, or use GKR to run the lookup argument itself.

Choose it whenWide, shallow, highly parallel workloads — bulk hashing, signature aggregation, inference — and zkVMs using a multilinear arithmetisation.

A transparent SNARK for R1CS built on sumcheck and a multilinear commitment, with sublinear verification after preprocessing and no FFTs. Its distinguishing property is that the commitment scheme is swappable.

Choose it whenAn intermediate proof layer, or the theoretical core of a zkVM — particularly when you want to change commitment schemes without changing arithmetisation.

Logarithmic-size zero-knowledge arguments from the inner-product argument, with no trusted setup. Best known for range proofs in confidential transactions; general circuits are supported but not the strength.

Choose it whenRange proofs and small confidential-transaction statements verified by full nodes.

Lookup arguments prove that values appear in a table, and are how systems express operations that are expensive as raw arithmetic. Plookup is the original and ubiquitous; LogUp uses logarithmic derivatives and is substantially cheaper for wide multi-column lookups; cq makes prover cost independent of table size after preprocessing; Lasso and its successors exploit table structure so huge tables need never be materialised.

Choose it whenEvaluate the lookup argument explicitly whenever range checks, bitwise operations or instruction decoding dominate your constraint count.

A low-level DSL that compiles templates into R1CS, typically proved with Groth16 or PLONK. The developer writes constraints explicitly and assigns witness values separately — the source of both its efficiency and its characteristic bug class.

Choose it whenFixed, small-to-medium, high-volume statements where the verifier must be cheap and the circuit will be audited hard: membership proofs, identity and anonymity sets, signature verification.

A Rust-like DSL that compiles to ACIR, an intermediate representation intended to be consumed by several proving backends. The compiler emits constraints for you, removing the manual assign-versus-constrain bug class. Browser and WASM proving are first-class targets.

Choose it whenNew application circuits where developer velocity and client-side proving matter, and teams uncomfortable with manual constraint discipline.

PLONKish arithmetisation with custom gates, lookup arguments and explicit region and column layout under developer control. The upstream implementation uses an inner-product argument and needs no trusted setup; a widely used fork swaps in KZG for constant-size, cheaply verifiable proofs.

Choose it whenTeams needing trusted-setup-free proving with a non-EVM or off-chain verifier, who have cryptography-capable engineers.

A Go SNARK library offering a high-level circuit API over Groth16 and PLONK, instantiable on six curves, with an extensive standard library and in-circuit recursive verifiers.

Choose it whenGo-based backends, proof aggregation and recursion layers, and wrapper circuits for STARK systems.

A toolkit of polynomial IOP primitives — fields, FRI, commitment schemes, DFTs — for building STARK provers over small fields. Not a DSL: you write AIRs against it or build a zkVM on it. It is the shared substrate beneath a large fraction of the modern zkVM landscape.

Choose it whenTeams building a zkVM, a custom AIR-based prover, or a domain-specific proving engine.

A language for provable programs executed by its own VM and proved by a Circle STARK prover over a small field. Verification is available both natively and as a verifier written in Cairo itself and run on the Cairo VM, which is what makes recursion native.

Choose it whenApplications native to its ecosystem, and any workload wanting a battle-tested, setup-free STARK stack with mature native recursion.

A RISC-V zkVM proving execution of programs compiled from Rust. The current generation uses a multilinear proof system with sumcheck-based arguments; final proofs are wrapped in Groth16 or PLONK for on-chain verification.

Choose it whenProving large existing Rust codebases — state transitions, consensus and EVM verification, bridges — where on-chain cost matters and published assurance evidence is a selection criterion.

One of the earliest general-purpose RISC-V zkVMs, based on FRI/STARK with a Groth16 wrapper for on-chain verification. Ships an unusually complete operational surface: local proving, hosted remote proving, and a live decentralised proof market.

Choose it whenTeams wanting the most operationally complete RISC-V zkVM today, including off-the-shelf outsourced proving, and who value documentation and stability over peak prover speed.

A zkVM framework with a no-CPU architecture: rather than one central processing chip, functionality is composed of independent chips and extensions, so custom instructions and precompiles can be added without forking the core.

Choose it whenTeams needing custom instructions, domain-specific precompiles, or an application-specific VM, who want to build on an audited modular base rather than fork a monolithic zkVM.

A RISC-V zkVM and STARK prover over the Mersenne-31 field, built to prove ZKsync OS and, by extension, any program compiled to RISC-V 32I+M. Its distinguishing claim is single-GPU throughput: published figures show a full Ethereum block proved on one GPU, with reproducible benchmarks in the repository.

Choose it whenTeams for whom raw proving cost on commodity GPUs is the deciding constraint and who can absorb a less mature developer surface.

A zkVM built on a lookup-centric, sumcheck-based design over multilinear commitments rather than FRI over AIRs, with memory-checking arguments enabling a streaming prover intended to prove arbitrarily long executions in bounded memory without recursion. In September 2026 the maintainers announced a lattice-based variant that replaces the elliptic-curve commitment, claiming post-quantum security and a faster prover.

Choose it whenResearch, prototyping, and workloads where the streaming low-memory profile is the deciding factor — with a plan to re-evaluate before any production deployment.

A STARK-based virtual machine with its own assembly language and a Rust compiler target, purpose-built for client-side proving and programmable privacy — a design point most general zkVMs do not target.

Choose it whenApplications needing client-side proving and programmable privacy. Less compelling as a general-purpose off-chain proving engine.

Services that run prover hardware on your behalf behind an API, typically bundled with an SDK, CI integration and autoscaling. Some are multi-zkVM, reducing lock-in at the operational layer.

Choose it whenPre-product-market-fit teams, bursty or low-volume workloads, and proving over public inputs. A poor fit for privacy-critical witnesses or systems requiring censorship resistance.

Protocols matching proof requests with a permissionless set of prover nodes using staking, bidding and on-chain settlement. The leading examples are anchored to their sponsor's own zkVM.

Choose it whenNon-private, latency-tolerant, variable-volume demand where censorship resistance matters more than deterministic latency. Pair with a self-hosted fallback prover for critical paths.

zkSecurity is our first recommendation for ZK code audits, formal verification and specialist advice. Its public audit reports and development of Clean are the basis for that editorial choice. Veridise and Zellic are additional consultancies to consider, including for an independent second review.

Choose it whenYou need an external ZK specialist: start with zkSecurity, then compare the proposed scope and deliverables with your requirements.

Line-by-line review of the arithmetisation by reviewers fluent in the DSL and proof system: is every witness value constrained, are ranges enforced, are components composed with their preconditions satisfied, is every public input actually bound. In practice the reviewer builds a model of what the constraint system permits and then searches for a satisfying assignment the developer did not intend.

Choose it whenEvery engagement, as the backbone. Highest value on novel application logic, custom gadgets, and cross-component composition — anywhere a specification exists to check against.

Tools that reason about the constraint system directly and either prove that outputs are unique given inputs, or produce two distinct witnesses satisfying the constraints for the same public input. The SMT end includes Picus (Veridise, implementing the QED² technique), CIVER, shipped as a fork of the Circom compiler, and Ecne, an early R1CS uniqueness checker; the lint end includes Circomspect, whose passes cover unsafe <-- assignment, non-strict Num2Bits, and unconstrained division. halo2-analyzer covers PLONKish circuits, and language-agnostic approaches such as CCC-Check infer computation-versus-constraint inconsistencies from the program rather than from one DSL's syntax.

Choose it whenMandatory pre-audit hygiene for any Circom or R1CS codebase, and a permanent CI gate — so the paid engagement is not spent on findings a linter would have caught.

Stating a circuit's intended behaviour as a theorem in a proof assistant and proving the constraint system implies it. Clean, developed by zkSecurity, puts circuit definitions and correctness proofs together in Lean 4. Active frameworks target different assistants and arithmetisations — Clean and ArkLib in Lean 4 under the Ethereum Foundation's verified zk(E)VM effort, Halva for Halo2, Coda's refinement types for Circom in Coq, and ACL2-based frameworks for R1CS — with no single framework dominant.

Choose it whenStable, high-value, heavily reused components: hash gadgets, field and bigint arithmetic, ISA instruction chips, the proof system's verifier. Poor fit for application logic still under design.

Executing the circuit against an independent oracle and searching for divergence, or mutating the prover to simulate a malicious one and checking the constraints reject it. For zkVMs, conformance suites are the natural oracle — the RISC-V architectural certification tests and the reference tests in Ethereum's execution specs provide an externally defined notion of correct. This is how a specification-conformance bug in a formally verified zkVM was found: by conformance tests, outside the verification effort's scope.

Choose it whenzkVMs, ISA and EVM emulation chips, standard cryptographic gadgets, and any circuit with an independent reference implementation. Also the right home for regression tests from prior findings.

Review of the argument system itself and everything below the arithmetisation: the soundness argument and its assumptions, what the Fiat–Shamir transcript absorbs, commitment instantiation, hash and sponge parameterisation, curve and subgroup structure, recursion composition, and the concrete bit-security the chosen parameters actually imply. This layer produces the highest-impact failures because they are construction-wide rather than deployment-specific.

Choose it whenMandatory if you implement, modify or newly compose a proof system, add recursion or aggregation, change the transcript, or pick non-standard parameters. Reducible — not eliminable — if you use a mainstream library unmodified at a pinned, audited version.

Review of everything between a valid proof and a state change: the verifier contract or host routine, public input encoding and ordering, field-range validation, verifying-key provenance and immutability, nullifier storage and replay logic, upgrade authority, and the binding between the deployed key and the audited circuit. This is where circuit-correct systems still fail.

Choose it whenEvery deployment. Assign one party explicit ownership of the circuit-to-verifier boundary, and require them to check the deployed verifying key against a reproducible build of the audited circuit.

A fixed prize pool distributed among independent researchers reviewing a pinned scope over a bounded window, weighted by severity and duplicate-adjusted. Public zkVM and circuit scopes have run in this format, with pool rules varying on whether low-severity findings are paid at all.

Choose it whenA complement after at least one targeted review and after internal tooling is clean. Weak substitute for a cryptography review of a novel proof system.

An open-ended funded programme covering deployed code, with published severity classification and reward scale. The better ZK programmes state explicitly whether circuits, prover, verifier contract and setup artefacts are in scope, whether completeness failures (valid inputs rejected, funds stuck) count alongside soundness failures, and what proof of concept is required at each severity.

Choose it whenEvery production system, funded proportionally to value at risk and live from mainnet day one. State explicitly whether circuits, prover, verifier contract and setup artefacts are in scope.

Automated review pipelines built on large language models with domain-specific context engineering, run over circuit and cryptographic library code. The category has moved from speculative to evidenced: a missing subfield membership check in an optimised pairing routine was found this way, assigned a CVE, and fixed upstream. Disclosure: that finding is the work of this document's maintainer, and it is a single self-reported result — weight it accordingly against the peer-reviewed evidence behind the other categories here.

Choose it whenA supplementary sweep alongside manual review and deterministic tooling, especially over large cryptographic library surfaces. Not a substitute for any other category.

Choose a proof system with a public-coin setup so there is no trapdoor to protect: FRI/STARK-based systems, Bulletproofs, Halo2 with IPA, and hash- or Pedersen-based multilinear commitments. This is the option most teams should evaluate first, because it removes the workstream rather than managing it.

Choose it whenSystems verifying off-chain, or on a chain tolerant of larger proofs, and any team for whom parameter lifecycle risk outweighs proof size.

The de facto toolchain for Circom-based Groth16 and PLONK projects, covering both the universal phase and the circuit-specific phase, on BN254 and BLS12-381. powersoftau verify validates the full chain of embedded public keys, not merely hash continuity.

Choose it whenCircom-based Groth16 and PLONK teams, and anyone consuming .ptau artefacts from Perpetual Powers of Tau.

Go implementation of the two-phase Groth16 MPC setup inside the gnark proving library, exposing contribution, verification and sealing as ordinary library calls. Phase 2 initialises from a phase-1 file plus the circuit's constraint system.

Choose it whenTeams whose circuits are written in gnark and who want the ceremony in the same toolchain as the prover.

Coordinator-run platforms that automate queueing, timeouts, per-contribution verification and attestation publication across multiple circuits at once, with browser and CLI contribution. The leading open platform states it is no longer actively developed, which is the most decision-relevant fact here: adopting it means owning it. Third-party coordination does buy something real — it constrains the project's ability to manipulate the ceremony software — but not its control of the circuit, the phase-1 artefact chosen, or the deployed verifying key.

Choose it whenTeams needing an open, browser-accessible phase-2 ceremony with many contributors, who do not want to build queueing and attestation plumbing themselves.

The architecture behind the largest ceremony run to date: a published specification plus a sequencer that authenticates participants, serves state over an API, verifies contributions and appends them. More than ten independent client implementations were produced against the specification.

Choose it whenOrganisations designing a large, public, browser-based ceremony who want a battle-tested reference architecture and verification-client model.

Protocols that remove the central coordinator by running contribution and verification through a smart contract or consensus layer, making eligibility and ordering publicly auditable by construction.

Choose it whenProjects where censorship-resistance of the ceremony itself is a stated requirement, or teams assessing where the field is heading.