← Ventali Tan

Proving the Circuit: Formal Verification for Zero-Knowledge Proofs

Morgan Thomas and Ventali Tan · September 2022, revised September 2026

In 2024 a systematization-of-knowledge paper collected 141 vulnerabilities from audits, disclosures and bug trackers of deployed zero-knowledge proof systems and sorted them by where in the stack they lived.¹ Most were not in the cryptography. They were in the circuits: the systems of polynomial equations over a finite field that encode the computation being proven. The most common root cause was a circuit that accepted more solutions than its author intended, so that a prover could satisfy it with a false statement.

That is the failure mode this post is about. We wrote the first version in September 2022, when the question "how do we formally verify a circuit?" had a handful of research prototypes behind it and no established method. The question has not changed. How do we formally verify that an arithmetic circuit, as used by a zero-knowledge proof system, has the desired characteristics: soundness, completeness, and zero knowledge?

The answer has a shape that is worth stating up front. The proof system is a general theorem, proven once on paper, that holds for every circuit in a class. The circuit is a one-off, and its correctness is a purely mathematical statement about a finite system of polynomial equations. Such a statement can be known only by proof, or by construction from something already proven. Testing does not reach it, because an under-constrained circuit passes every test an honest prover can write. The rest of this post makes that precise: what the statement is, what a constraint system is, which techniques can establish the statement and at what cost, a way of thinking that makes the obligations compose, who was doing what in 2022, and what has happened in the four years since.

1. The leading problem

Fix a finite field F, in practice the scalar field of a pairing-friendly curve with p near 2²⁵⁴, or a small FFT-friendly field near 2⁶⁴ or 2³¹ for STARKs. A constraint system C over F is a finite list of polynomials c₁, …, c_k in variables partitioned into public inputs x ∈ Fⁿ and witness variables w ∈ F^m. We write C(x, w) = 0 to mean that every c_i vanishes at (x, w). The public inputs are the statement being proven. The witness is everything the prover supplies to make the statement check out, secret inputs and intermediate wires alike.

A circuit denotes a set: the set of statements for which some witness exists.

A specification denotes a set as well, the set S ⊆ Fⁿ of statements that are true in the intended semantics. For a hash-verification circuit, x is a pair (d, h) and S is the set of pairs where h is the hash of d. With both sets in hand, the two properties of interest are inclusions.

Soundness of a circuit says it is unsatisfiable on every false statement: no witness, however adversarially chosen, makes the polynomials vanish when x ∉ S. Completeness says it is satisfiable on every true statement. The conjunction, ⟦C⟧ = S, says the circuit denotes the intended relation, and that is the whole of circuit correctness. Table 1 lays out the four cases for a single statement.

The two kinds of bug have names in practice. An under-constrained circuit is one that is unsound: the constraints admit assignments the specification forbids, so the denotation is too large. An over-constrained circuit is one that is incomplete: the constraints exclude assignments the specification requires, so the denotation is too small. Under-constrainedness is the dangerous direction, because an honest prover never notices it. The honest prover computes the intended witness, the circuit accepts it, every test passes, and the extra solutions sit unused until someone goes looking for them.

An under-constrained circuit passes every test an honest prover can write. The extra solutions sit unused until someone goes looking for them.

Most specifications are relations rather than sets. The spec says which meaningful witnesses y ∈ W go with which statements, R ⊆ Fⁿ × W, and the circuit's witness w contains an encoding of y together with auxiliary wires. The set-level statement ⟦C⟧ = { x : ∃ y. R(x, y) } is then the minimum. Applications that need knowledge soundness need the stronger, witness-level form, with a projection π from circuit witnesses to meaningful ones:

The first implication is soundness at the witness level, the second completeness. Verification efforts differ in which of these they prove, and it is worth asking of any result which one it establishes.

Zero knowledge is a property of the proof system rather than of the circuit, and we mostly set it aside here.² It says that a proof reveals nothing beyond the statement: for every verifier strategy there is a simulator that, given only x, produces a transcript indistinguishable from a real interaction with a prover who knows w. What the circuit contributes is the boundary of "nothing beyond the statement". Any fact implied by x together with ⟦C⟧ is fair game, so if the relation lets w be recovered from x, because the function is easy to invert or the domain is small, no proof system can hide it. A circuit that is meant to hide its witness must encode a hard-to-invert function of that witness.

Two subproblems

A proof system Π takes a circuit C, a statement x and a witness w and produces a proof; its verifier takes C, x and the proof and accepts or rejects. Π is complete if honest proofs of true statements are accepted, sound if no prover can get a false statement accepted except with negligible probability ε, and zero knowledge as above. These properties are stated relative to ⟦C⟧, and they are proven once, for all C in the class the system supports.

Put the two obligations together and the application-level guarantee follows. If ⟦C⟧ = S and Π is sound and complete, then the application-specific proving system, Π instantiated with C, accepts exactly the true statements: honest proofs of x ∈ S always verify, and no proof of x ∉ S verifies except with probability ε. The leading problem therefore splits cleanly. One subproblem is verifying the proof system, which is hard, has been done informally for the major systems, and in 2022 had not been done formally for any significant one. The other is verifying the circuit, and that is a problem about systems of polynomial equations, independent of which proof system will consume them.³ This post is mostly about the second.

Formal verification of a circuit needs five things: a formal specification of the relation the circuit is intended to encode, a formal model of the semantics of circuits, the circuit itself, a theorem prover, and a mechanized proof, checked by the prover, of a theorem relating the first three. Figure 1 shows how they fit, and how the result composes with the proof system.

2. What a constraint system is

The polynomial systems that proof systems consume come in a few standard shapes, and the shape matters to verification because it determines what the semantics model in Figure 1 has to say. Three cover almost everything deployed.

Rank-1 constraint systems

An R1CS with k constraints over a vector z = (1, x, w) of length 1 + n + m is a triple of matrices A, B, C ∈ F^{k × (1+n+m)}, satisfied when

where ∘ is the entrywise product. Each row is one constraint of the form (Σ a_i z_i)(Σ b_i z_i) = Σ c_i z_i: a product of two linear forms equals a third. The constant wire 1 lets constants appear. A boolean wire b is constrained by the single row b · (b − 1) = 0, that is, a = e_b, b = e_b − e₁, c = 0. Any polynomial system can be flattened to this shape by introducing a wire for each intermediate product, which is how a compiler like circom gets from a program to an R1CS. The pairing-based SNARKs consume R1CS after interpolating each column into a polynomial: pick k distinct points r₁, …, r_k, let A_i(X) be the polynomial that passes through the entries of column i of A at those points, and likewise for B and C. The R1CS is then satisfied if and only if the polynomial identity

holds for some quotient H. That is the quadratic arithmetic program, and it is the identity a pairing-based SNARK such as Groth16 checks in the exponent.⁴

Algebraic intermediate representations

A STARK works from an execution trace T with L rows and c columns, one row per step of a machine and one column per register. An AIR is a list of transition polynomials P_i in 2c variables that must vanish on every pair of consecutive rows, plus boundary constraints pinning particular cells. On a multiplicative subgroup H = ⟨ω⟩ of F of order L, each column interpolates to a polynomial T_j(X) with T_j(ω^t) = T[t][j], and the transition constraint becomes divisibility:

The prover commits to the T_j and to the quotients, and a low-degree test does the rest.⁵ For verification the point is that the AIR is a small object, a few dozen polynomials of low degree, while the trace is huge, and the correctness question is about the AIR: does every trace satisfying it correspond to a valid execution of the machine, and does every valid execution produce a satisfying trace? That is ⟦C⟧ = S again, with S the set of statements a correct machine can reach.

PLONKish systems

PLONK and its descendants lay wires out in a table and attach a gate equation to each row, selected by fixed columns:

Setting q_M = 1, q_O = −1 and the rest to zero makes a multiplication gate; other selector patterns make addition or constants. Wires that must be equal across rows are tied by a copy constraint, expressed as a permutation σ on cells with the requirement that the table is invariant under σ. Halo 2 generalizes the gate to arbitrary custom polynomials over cells at fixed row offsets, and adds lookup arguments, which constrain a tuple of cells to lie in a fixed table.⁶ The verification question is unchanged, but the semantics model has to account for three kinds of constraint, gate, copy and lookup, rather than one.

What the three shapes share is that they are finite systems of polynomial equations over a finite field. Satisfiability of such a system is decidable, because the domain is finite, and intractable in general, because deciding whether a quadratic system over F_p has a solution is NP-complete. Verification therefore cannot be brute search, and the techniques in Section 3 are all ways of exploiting structure: the constraints are sparse, most are linear or bilinear, and most gadgets are meant to compute a function of their inputs.

A worked example

The gadget that appears most often in discussions of circuit bugs is the one that tests whether a wire is zero. In circomlib it is written as follows: introduce a witness wire inv, which the honest prover sets to the inverse of in when in ≠ 0 and to 0 otherwise, and impose two constraints.⁷

Take the cases. If in = 0, constraint (i) forces out = 1, and (ii) holds trivially. If in ≠ 0, constraint (ii) forces out = 0, and then (i) forces inv = in⁻¹, which exists. So for every in there is exactly one out that satisfies both, and it is the intended one: the circuit denotes the relation out = [in = 0], and it is sound and complete.

Now drop constraint (ii). When in = 0 nothing changes. When in ≠ 0, the prover may still set inv = in⁻¹ and get out = 0, but may equally set inv = 0 and get out = 1. The circuit accepts the false statement "in is zero" for every nonzero in. Nothing about the honest prover's behavior has changed, every test the honest prover writes still passes, and the denotation has doubled. Add instead the extra constraint in · inv = 1 and the opposite happens: for in = 0 no assignment satisfies it, and the circuit rejects the true statement "0 is zero". Figure 2 draws the first two relations.

The dropped-constraint version violates a property worth naming, because it is the one most automatic tools check. A circuit is properly constrained, or has the uniqueness property, with respect to a designated set of output wires if the inputs determine the outputs:

Uniqueness needs no specification. It is a property of the polynomial system alone, which is what makes it automatable, and the tools Ecne and Picus discussed below check exactly this.⁸ It is also strictly weaker than soundness. A circuit that computes a function deterministically may compute the wrong function; uniqueness says the prover has no freedom, not that the prover's forced answer is right. In practice the two come apart less often than one might expect, because the commonest way to be unsound is to leave a wire free, and that is exactly what uniqueness catches.

3. Techniques

To know a general statement with certainty, it has to be a mathematical statement, knowable by reasoning from consistent assumptions through truth-preserving inferences, without running anything. Given that a bachelor is an unmarried man and that a married man has a spouse, no bachelor has a spouse; no survey of bachelors is required. A proof theory codifies which inferences are truth-preserving, and with pencil and paper one can construct proofs in it. A proof assistant is a program that helps construct such proofs and checks them mechanically, which removes human error from the checking and reduces the labor of the construction. Coq (renamed Rocq in 2025), Agda, Isabelle, ACL2, PVS, Imandra and Lean are the ones that appear in this post.

With a proof assistant

There are two ways to prove a statement about a program with a proof assistant. One is to write the program in the proof assistant's own language and apply its proving facilities directly. The other is to translate a program written in some other language into an object the proof assistant can reason about, and prove things about that object. The second is post hoc verification, and the translation is its weak point: the proof is about the translator's output, and the assumption that the output means the same as the source is unproven unless the translator is itself verified.⁹ The first approach gives more confidence, because the theorem is about exactly the program being executed. What motivates the second is that the proof assistant's language is often not a language one can build the application in.¹⁰

Without a proof assistant

A verified compiler is a compiler with a theorem, checked in a proof assistant, that its output has the same meaning as its input. CompCert is the canonical example: a C compiler proven to emit assembly semantically equivalent to the C.¹¹ A verifying compiler is different: it emits, alongside each compiled program, a proof that this particular output matches this particular input, which can be checked independently. Either way the output is correct by construction, provided the input was correct. Verified compilers do not find bugs in source programs; they promise not to add any.

An automatic proof search algorithm takes statements and returns proofs when it finds them. A static analyzer takes a program and recognizes patterns that always or often indicate a problem, without understanding what the program means. Each has a ceiling. A verified compiler proves only that meaning is preserved, and nothing about whether the meaning was intended. A proof search algorithm is limited by its sophistication and its compute, and no algorithm can prove every true statement, for reasons the footnote spells out with the care a reviewer of the original version insisted on.¹² A static analyzer cannot tell whether a program is correct, only whether it resembles programs that were wrong.

What is different about circuits

For ordinary software these limits bite hard. For circuits, automatic methods reach further than usual, for the reason already given: the objects are finite polynomial systems over F_p, not programs with loops and heaps. Satisfiability modulo a theory of finite fields, with Gröbner-basis and propagation reasoning inside the solver, decides bounded questions about a circuit outright, and uniqueness in particular reduces to a single query: find x, w, w′ with C(x, w) = 0, C(x, w′) = 0 and out(w) ≠ out(w′). If the solver returns unsatisfiable, the circuit is properly constrained. If it returns a model, the model is a concrete exploit. What the automatic route cannot do is supply the specification. Uniqueness and its relatives are spec-free, and once they are exhausted, everything left needs S written down formally, and then either an interactive proof against it or a compiler proven to produce circuits from it. Figure 3 places the techniques and the tools on those two axes.

4. Denotational design

The observation that a circuit denotes a set, and a specification denotes a set, is more useful than it looks, because it turns every verification obligation into an equation between denotations, and equations compose. The methodology has a name, denotational design, and it applies to both subproblems.

Suppose specifications are written in a language Spec and compiled to circuits by a function comp. Each language has a denotation function into subsets of Fⁿ. The compiler is correct when the square in Figure 4 commutes:

Soundness of the compiler is the inclusion ⊆, completeness the inclusion ⊇, and commutation is both. The same square with a single circuit in place of comp(s) is the post hoc obligation of Section 1: a proof that one particular C denotes one particular S.

The proof system's properties are stated against the same denotation. Completeness: for every C and every x ∈ ⟦C⟧ with witness w, the honest prover's proof is accepted. Soundness: for every C and every x ∉ ⟦C⟧, no prover strategy is accepted except with probability ε. Knowledge soundness strengthens this with an extractor E that, given access to any prover P* that convinces the verifier, produces a witness:

None of these mention S. That is the point. The proof system is verified once against ⟦·⟧_Circ, for all circuits. The compiler is verified once against both denotations, for all specifications. An application then consists of writing s, and its correctness follows without an application-specific proof: ⟦comp(s)⟧ = ⟦s⟧ by the compiler theorem, and Π is sound and complete for ⟦comp(s)⟧ by the proof-system theorem. This is the correct-by-construction route, and it is the only route that scales to more circuits than there are people able to write mechanized proofs.

The proof system is verified once against the denotation of circuits. The compiler is verified once against the denotation of specifications. The application is verified by writing it down.

A concrete instance existed in 2022. Morgan Thomas's arithmetization of Σ¹₁ relations takes formulas of the shape

where the f_i range over functions on bounded finite domains and φ is first order, and compiles them to Halo 2 circuits whose denotation is the set of x for which the formula holds. The Orbis Specification Language is a typed front end that compiles to such formulas.¹³ Σ¹₁ is a natural target because it has exactly the strength of an NP relation: the existential function quantifiers are the witness, the first-order body is the check. A specification written in OSL needs no circuit-level reasoning at all once the compiler is proven.

The terminology, stated once. If you write a specification in a high-level formal language and compile it with a verified or verifying compiler, the result is correct by construction. If you take an existing constraint system and prove properties of it, up to and including ⟦C⟧ = S, against a high-level specification, that is post hoc verification.

5. From theorem to executable

There is usually a gap between the theorem one can prove and the code one can run. One can prove a theorem about a specification and write code for it, and not be able to prove the code implements the specification. One can prove a theorem about code and not be able to compile it efficiently. One can compile it and not be able to prove the machine code means what the source meant. Every approach to closing the gap decides which of these to prove and which to trust, and Table 3 records the trusted core for each: the components whose bugs would invalidate the theorem without being caught by it.

The ecosystem in 2022 offered several partial bridges. Coq and Agda extract programs to OCaml or Haskell, to be compiled conventionally, with the extraction trusted and the efficiency of the result often disappointing. ATS combines a proof system with a language that aims at C-level efficiency. Fiat and CertiCoq synthesize efficient binaries inside Coq with the synthesis proven. ACL2 defines a subset of Common Lisp with a full formal logic, so that an executable definition is also a logical one: the same text is compiled to efficient code and reasoned about, and a verifying compiler, ATC, carries ACL2 to C.¹⁴ Imandra does the same for a subset of OCaml. Transpilers from mainstream languages into a proof assistant allow theorems about an extracted model of the source, with the transpiler trusted.¹⁵

Hardware

Proof generation is dominated by number-theoretic transforms, O(n log n) field operations, and multi-scalar multiplications, O(n) group operations with large constants, both of them embarrassingly parallel. Provers are most efficient on GPUs, FPGAs and ASICs, and are mostly written for CPUs, because CPUs are easier to program and the programmers are easier to hire. For a formally verified prover that is also fast, the right target is the specialized hardware, and in 2022 tools for compiling formally verified programs to GPUs, FPGAs or ASICs were, as far as we knew, nonexistent. That has not materially changed. The verification story for provers still stops at the CPU, and the vectorized kernels that do the work sit outside every proof.

6. Where things stood in 2022

Two older bodies of work were adjacent. Decades of research on formally verifying arithmetic circuits exist in the hardware community, with some industrial use, but a hardware arithmetic circuit is a netlist of bit-level gates and a SNARK arithmetic circuit is a polynomial system over a large prime field, and the methods do not transfer directly.¹⁶ Decades of research also exist on proving soundness, completeness and zero knowledge for probabilistic proof systems, on paper: Groth16, Bulletproofs and PLONK each come with such proofs, and they are the starting point for doing the same formally.¹⁷

The efforts directed at circuits themselves were few, and each is best described along four axes: the language used for the specification, the language used to model the circuit, the theorem prover, and the theorems proven, whether soundness, completeness, functional correctness or zero knowledge. Two further questions bear on how much confidence a result deserves: whether the tooling and proofs are open source, since a theorem whose inputs cannot be inspected is hard to trust, and what the trusted core is. Table 4 applies the rubric.

In prose. Kestrel Institute had proved functional correctness of R1CS gadgets in ACL2: they formalized R1CS in ACL2, fetched gadgets from the Bellman implementation with an extraction tool, lifted them into logic with the Axe toolkit, and proved them equivalent to specifications of parts of the Zcash Sapling protocol and of Ethereum's Semaphore, which implies both soundness and completeness of those gadgets.¹⁸ Aleo was building Leo, a language compiling to R1CS, with the aim of a verifying compiler whose per-compilation theorems are generated and checked in ACL2, and had done post hoc verification of gadgets with Axe.¹⁹ Orbis Labs was building the Σ¹₁ compiler and OSL of Section 4, and a toolchain, Miya, aimed at hardware-accelerated verified provers, with a theory of interaction-combinator arithmetization and parsimonious definitions of proof system, soundness and zero knowledge. Bolton Bailey and Andrew Miller were formalizing soundness of a range of SNARKs in Lean, in the algebraic group model.²⁰ Veridise had Medjai, a symbolic evaluator for Cairo; Picus, a symbolic virtual machine for R1CS aimed at automatic proof search; V, a specification language; and Coda, a Coq framework for certifying circuits through a functional DSL.²¹ Ecne, from 0xPARC, was a special-purpose solver that proves an R1CS defines a function, total or partial, and had found real bugs that way.⁸ StarkWare was writing Lean proofs that Cairo programs conform to specifications.²² Alex Ozdemir was adding a finite-field theory to the cvc5 SMT solver, and Lucas Clemente Vella and Leonardo Alt were building a solver for polynomial systems over finite fields.²³ Nomadic Labs had brought Zcash Sapling to Tezos, with some of its R1CS verified by Kestrel, and Anoma was building Juvix as a language-level route to more reliable contracts.²⁴

7. What has happened since

Four years is a long time in a field that had almost nothing. Read against the rubric, the movement sorts into five lines.

Spec-free checking became a product. Picus was published in 2023 as an automated checker for the uniqueness property, combining an SMT solver over F_p with a propagation procedure tuned to the linear and bilinear structure most gadgets have, and it found under-constrained circuits in circomlib and in deployed projects.²⁵ Trail of Bits released Circomspect, a static analyzer for circom that flags the patterns, such as a signal assigned with <-- but never constrained, that produce the IsZero bug of Section 2.²⁶ These are the top-left of Figure 3, and it is now reasonable to expect any serious circuit to have been through them.

The solvers arrived. cvc5 shipped a theory of finite fields in 2023, and a proposal for a standard SMT-LIB theory of finite fields followed in 2024, so the polynomial-solver work that was a research prototype in 2022 is now a standard interface any verification tool can target.²⁷

Specifications got cheaper. Coda, published in 2024, writes circuits in a DSL with refinement types: the type of a gadget carries the relation it is meant to compute, and Coq discharges the resulting obligations, many of them automatically, with the remainder proved by hand. Its authors certified a substantial part of circomlib this way.²⁸ Kestrel wrote up the ACL2 method in 2023, with a formalization of prime-field constraint systems, the lifting of gadgets into logic, and compositional proofs that let a verified gadget be reused inside a larger one without reproving it.²⁹ Both are the bottom-right of Figure 3 moving upward: the same spec-required guarantees at less labor per gadget.

The proof-system subproblem got real work. Bailey and Miller's Lean formalization of soundness for a family of pairing-based SNARKs in the algebraic group model was completed and published, the first mechanized soundness proofs for deployed SNARK constructions.²⁰ In the other direction, Dao, Miller, Wright and Grubbs showed that many deployed proof systems had implemented Fiat–Shamir weakly, omitting the statement from the hash, and that the omission was exploitable. It is a reminder that "assume the proof system is sound" is an assumption about an implementation, not only about a paper.³⁰ The Verified zkEVM effort, started in 2024, is building ArkLib, a Lean 4 library for stating and proving the security of interactive oracle proofs and polynomial commitment schemes, which is the reusable verified abstraction the 2022 list of directions asked for.³¹

Correct by construction at scale. StarkWare and Avigad's group published a proof-producing compiler for Cairo in 2025: the compiler emits, with the compiled program, a Lean proof that the program meets its specification, which is the verifying-compiler pattern of Section 3 applied to circuits that run in production.³² The Verified zkEVM effort maintains Clean, a circuit DSL embedded in Lean in which each gadget is written together with its soundness and completeness proofs and gadgets compose with their proofs, so that the square of Figure 4 commutes by construction for everything written in it.³¹

Table 5 sets the 2022 list of directions against this.

8. What is still open

Three things have not moved, and one new bottleneck has appeared.

The composition of Section 1, circuit theorem plus proof-system theorem plus compiler theorem yielding an application guarantee, has been proven in pieces and, as far as we know, never assembled end to end for a deployed system with a single trusted core. The pieces now live in the same proof assistant more often than not, which was not true in 2022, so the assembly is closer to an engineering project than a research one.

Hardware is untouched. Provers run on GPUs and the proofs stop at the CPU.

Zero knowledge is still the property everyone defers. The simulator-based definition is well understood on paper, and formalizing it for a particular circuit and proof system, so that "the proof reveals nothing beyond x" is a checked theorem, remains rare.

The new bottleneck is specification. When the tools were the limit, the proof was the expensive step. With uniqueness checkers automatic, solvers standard and refinement types discharging much of the rest, the expensive step is writing S: saying, in a formal language, what the circuit is for. Spec-free properties are exhausted at uniqueness. Everything beyond it needs a specification, and specifications are written by people who understand both the application and the logic, which is a small set. Two things help. Executable specifications, in the ACL2 style, can be tested before they are proven, which catches the specification bugs that would otherwise be proven faithfully. And the proof, unlike the specification, no longer has to be written by a person: a proof generated by any means, including a language model, is checked by the same kernel, so the untrusted part of the pipeline can be as unreliable as it likes.

The 2022 version of this post ended by saying that not enough emphasis is placed on formal verification in the security industry. That is less true now, and the reason is the one this post opened with. The bugs are in the circuits, the circuits are polynomial systems, and the correctness of a polynomial system is a theorem or it is nothing.

References