Every ZK circuit is written twice. The witness generator evaluates the computation and assigns concrete values to the circuit’s signals, and the constraints are polynomial equations that decide whether a given assignment gets accepted. A developer writes both, often on adjacent lines of the same file. The prover runs the witness generator to produce a set of signal values, and the proof system checks only that those values satisfy the constraints, never whether the witness generation logic itself was correct. Whether the two descriptions mean the same thing is left to the developer to get right.

We are releasing LLEQ, an open source equivalence verifier for ZK circuits. It operates on circuits lowered to LLZK and checks whether a circuit’s witness generation agrees with its constraints, reporting the signals it can prove equivalent and producing a counterexample when the two sides disagree. Importantly, while equivalence rules out a large class of circuit bugs, it does not on its own establish that a circuit computes what its developer intended.

TL;DR

• LLEQ proves a circuit’s constraints accept exactly the valuation its witness generator produces.
• Runs on circuits lowered to LLZK. Circom today, Noir in progress.
• Returns ok, counterexample, or unknown, the same shape as Picus.
• Built on deductive verification and static analysis.
• Open source under project-llzk, funded by the Ethereum Foundation.

Where the two descriptions drift apart

A mismatch breaks the circuit in either direction. If the constraints reject a value the witness generator produces, an honest prover cannot prove a true statement. If the constraints accept values the witness generator would never produce, a malicious prover can establish something the intended computation does not support.

Mismatches of this kind are a common source of circuit bugs. The USENIX Security 2024 paper SoK: What Don’t We Know? Understanding Security Vulnerabilities in SNARKs studies 141 disclosed vulnerabilities across the SNARK stack. Of the 99 circuit-level vulnerabilities in that dataset, 34 came from an incorrect translation of program logic into constraints. That is the largest single root-cause category in the paper’s taxonomy, ahead of both missing input constraints and signals assigned but never constrained. The pattern is familiar from our own ZK audits, where constraints regularly say something other than what the developer read them as saying.

A short Circom template shows how little it takes:

The witness assignment computes out by truncating integer division. The constraint requires out * weight to equal inp in the circuit’s prime field. The two agree whenever inp is an exact multiple of weight, which is why the template survives casual reading. In general they describe different computations.

Take inp = 1. The witness generator evaluates 1 \ 10^6 and assigns 0 to out, which fails the constraint, since 0 * 10^6 is not 1. The constraint still has a solution, the multiplicative inverse of 10^6 in the field, and a prover working from the constraints rather than the code can use it to claim a reward far larger than the template appears to permit.

Neither side here is ambiguous. Each pins down one value for out, and the problem is that they pin down different values. Checking whether the constraints are deterministic will not surface that, so the two descriptions have to be compared against each other directly.

The equivalence property

For a fixed set of inputs, the witness generator assigns a value to every signal in the circuit, and the constraints define a set containing every signal assignment the verifier will accept; LLEQ checks that this set contains exactly the assignment the witness generator produces. More formally:

Let W(x) denote the complete signal valuation produced by the witness generator on inputs x, and let C(x, s) mean that valuation s satisfies the constraints. For every valid input x, LLEQ checks:

The two directions of that equality correspond to the two failure modes. Requiring W(x) to belong to the set establishes that the witness satisfies the constraints. Requiring the set to contain nothing else rules out alternative satisfying valuations.

This is stronger than ordinary functional equivalence, which compares the outputs of two deterministic programs without demanding that every internal signal take a unique value. The extra strength is useful because the formulation also exposes nondeterminism: constraints that permit two values for a signal can match at most one witness valuation. Where witness generation permits multiple valuations, LLEQ can pair one of them against a different valuation that satisfies the constraints, which is a candidate counterexample.

How LLEQ verifies a circuit

LLEQ verifies an LLZK struct in two stages. A symbolic store handles signals whose witness and constraint expressions match syntactically, and deductive verification reasons about signals whose expressions differ syntactically while still carrying the same meaning.

Resolving direct matches

Many signals follow the same pattern: the witness generator assigns an expression to a signal, and the constraints equate that same signal with the same expression. LLEQ records symbolic expressions for signal values on both sides and compares them. Where the expressions match, the signal is settled without asking an SMT solver to derive the same fact. Array-valued signals need element-wise comparison plus a check that both sides write and constrain the same set of indices.

The symbolic store stays useful when it cannot finish the proof on its own, since the equalities it discovers are handed to the deductive verifier as assumptions, reducing what the solver has to establish. On circuits built mostly from the write-then-constrain pattern, the store can carry the whole proof. We expect large circuits such as Poseidon to verify quickly for that reason once subcomponent support improves.

Searching for a disagreement

The query is built by weakest-precondition reasoning. Starting from the equality it wants to prove, LLEQ works backward through assignments, assertions, branches, and other operations to obtain conditions sufficient for that equality to hold. The resulting verification condition is discharged using Z3 and cvc5. An unsatisfiable disagreement formula rules out any counterexample the model can express, and a satisfiable one hands back values under which the two sides diverge.

Encoding stays in the theories of integers and arrays rather than bitvectors, to avoid fixing a bitwidth. LLEQ does not currently support encoding into the theory of finite fields, since witness computation regularly contains operations with no natural expression in field arithmetic. Truncating division is one. Ordered comparison is another.

Loops and invariant inference

Loops complicate this because LLEQ has to work out which iteration of the witness computation corresponds to which iteration of the constraints. It aligns the two loops into a product program, then tries to infer an invariant summarizing which values stay equal after each iteration; a typical invariant states that corresponding array elements agree at every index the loop has processed so far.

Invariant inference is necessarily heuristic: LLEQ can fail to find an invariant that exists, instead finding one that is valid but too weak to prove the final equality. The overall procedure is therefore incomplete, and LLEQ can return unknown on a circuit that is in fact equivalent.

When inference stalls, LLEQ can unroll the loop, scalarize array accesses, and verify the loop-free struct directly. That path needs a concrete instantiation, since loop bounds are often governed by struct parameters; thus it establishes the property only for that instantiation.

For a fuller walkthrough of this design, including a live demo, see Raghav’s talk.

Why LLEQ works on LLZK

ZK circuit languages differ in syntax and in programming model, and implementing LLEQ separately for each would mean a verification frontend per language, duplicating most of the analysis underneath. LLEQ instead operates on LLZK, the shared intermediate representation for ZK programs we released as V1.0 in April. Circuits are lowered to LLZK first, and LLEQ works on the result. This decouples language support from equivalence verification: a new circuit language needs an LLZK frontend rather than a new verifier. Circom circuits can be lowered and checked today, and Noir support is in progress. Building on MLIR also brings its analyses and transformations along.

Verification could instead run over a low-level constraint representation such as R1CS, at the cost of discarding most of the structure that makes verification tractable. LLZK retains struct and component boundaries, parameters, control flow, and the separation between computation and constraints, so LLEQ reasons about one struct at a time rather than treating a circuit as one flattened collection of equations. That is what puts modular and parametric verification within reach as subcomponent support improves.

Operating on LLZK introduces one challenge: separating witness computation from constraints means LLEQ has to recover which loops and operations correspond to one another. Circom naturally produces code where both sit in the same loop, already lined up, while LLZK splits them into a compute function and a constrain function. A poor product alignment can stop LLEQ from proving a correct circuit equivalent, which makes alignment quality one of the practical limits of the current verifier.

Interpreting LLEQ’s results

LLEQ returns one of three results.

• ok means no counterexample exists within the encoded model, so the equivalence property holds.
• counterexample means LLEQ found values under which the witness computation and constraints disagree, with a model showing what each side assigns.
• unknown means LLEQ could neither prove equivalence nor produce a counterexample.

An unknown result does not mean the circuit is incorrect. It could result from a solver timeout, an unsupported construct, a poor product alignment, or an invariant too weak to close the proof.

A counterexample carries a caveat when the proof depends on an inferred loop invariant. LLEQ can report one because the invariant it built was too weak, not because the circuit is actually broken, which makes that particular counterexample a false positive. Loop-free circuits carry no such risk. Any counterexample there is a true positive.

Results are also scoped to the LLZK program handed to LLEQ and to the semantics the verifier models. LLEQ does not check that a source-language frontend translated the circuit correctly, and it proves nothing about the underlying proof system or the surrounding application. Within that scope, an ok result rules out witnesses the constraints would reject, along with satisfying valuations outside the range of the witness generator.

How LLEQ and Picus divide the work

Picus proves determinism, meaning that a circuit’s outputs are uniquely determined by its inputs. That rules out a large class of soundness bugs, and Picus is mature at proving it, which is why it is the verifier we reach for on zkVM circuits, including SP1 and RISC Zero. Equivalence is the wider property, and Reward is an example of a circuit that passes a determinism check and fails equivalence. The two verifiers are complementary, they report results in the same three-way shape, and both take LLZK as input, so a circuit compiled once can be given to either.

For a team using AuditHub, the intended workflow has the same shape as the rest of the platform. Compile the circuit to LLZK, submit it, and LLEQ runs over the result as one of the available verifiers. That integration is the plan rather than a shipped feature today.

Where LLEQ stands today

Implementation began in Q4 2025 and finished at the end of Q2 2026, with Raghav Malik as project lead and Alexander Hicks at the Ethereum Foundation collaborating on the project.

Lookup tables are not supported. Encoding a table directly as a solver object is possible, though the version worth having summarizes the lookup as a formula, and that work is not done.

Algebraic reasoning beyond field arithmetic is out of reach. Run against circomlib’s BabyAdd, which performs point addition on the Baby Jubjub curve, LLEQ proves the four intermediate signals equivalent and then stalls on the output coordinates. Settling those requires curve identities an integer solver has no path to discovering, and the result comes back unknown rather than a counterexample, since the circuit is correct. This is a boundary of the technique, not a tuning problem.

Subcomponent calls and multidimensional arrays need work. Verification runs one struct at a time, and aligning calls into other structs can require manual intervention today. Multidimensional arrays are not yet handled well either.

Loops with loop-carried dependencies are hard. Inferring the right invariant there means inferring an arbitrary recurrence relation, which is difficult in general rather than merely unimplemented.

The dominant bottleneck is finite field arithmetic in an integer solver. Query size matters less than whether the solver has to rediscover a field identity to make progress. Proving a single signal inductive can time out on that alone, and cutting down how often values are reduced modulo p is where current optimization work sits.

Everything described here lives on a public release branch, pending code review before it merges to main. Development finished recently and the tool still has rough edges.

Trying LLEQ

LLEQ is available in the public project-llzk/LLEQ repository, with example Circom circuits and scripts for collecting verification results. A circuit has to be lowered to LLZK through the appropriate frontend before LLEQ can analyze a struct in the resulting program. The README covers the current workflow and its dependencies. It is not a proprietary Veridise tool. Issues and pull requests are welcome.

What’s ahead

Subcomponent reasoning has the most room to improve. Stronger support will let LLEQ verify a component using properties already established about the components it calls, instead of requiring the whole computation to be flattened or analyzed at once. Product alignment heuristics come next, pairing more witness and constraint loops automatically and handing invariant inference a better product program to work from.

Integration with the LLZK specification language is the change with the widest reach. Preconditions can express assumptions such as valid input ranges or nonzero divisors, ruling out counterexamples that only arise from cases a developer already knows cannot occur. Postconditions can summarize a verified component for its callers, so knowing that Num2Bits enforces a range constraint on its input helps prove equivalence for anything built on top of it. Range preconditions are often inferable from range analysis without the spec language. Relational constraints need it. Ian Neal and Daniel Domínguez Álvarez cover the verif dialect connecting the spec language to SMT solvers in this talk.

Development was supported by the Ethereum Foundation, and this first release covers one precise property, that a circuit’s witness generator and its constraints describe the same computation.

---

What is ZK circuit equivalence checking? The Takeaway

ZK circuit equivalence checking proves that a circuit’s constraints accept exactly the signal assignment its witness generator produces. LLEQ verifies this property for circuits lowered to LLZK, returning a proof or an explicit counterexample. Circuits that pass have a large class of soundness bugs ruled out.

---

Working on a similar protocol?

If a circuit’s witness generator uses truncating division or ordered comparisons, operations that mean something different once they are interpreted over a prime field, its constraints can end up expressing a different function than the code appears to compute. The pattern is hard to catch in review because both halves are deterministic and a constraint sitting under an assignment reads as though it checks that assignment.

If you want a second pair of eyes on your circuits before your next deploy, talk to us.