Formal Verification of ZK Circuits in ACL2: Kestrel's R1CS and PFCS Approach

"Formal Verification of Zero-Knowledge Circuits" by Alessandro Coglio, Eric McCarthy and Eric W. Smith was posted to arXiv as 2311.08858 on 2023-11-15 and published in the ACL2-2023 workshop proceedings (EPTCS 393, pp. 94–112). The authors work at Kestrel Institute; Coglio and McCarthy are also at Aleo Systems. It reports work, across several projects, on proving that circuits mean what they are supposed to mean. The proofs are done in the ACL2 theorem prover and in Axe, a toolkit built on ACL2.

The problem: does the circuit say what the program says?

A ZK proof only proves the statement its circuit encodes. The paper defines a circuit as equality constraints over variables, using only addition and multiplication modulo a large prime. That is a low-level form PL of the predicate. The prover and verifier think in terms of a higher-level description PH. The authors note that if PL and PH do not denote the same predicate, "the zero-knowledge proof may not quite prove what is expected."

Their framework makes this precise. With a chosen variable ordering, an R1CS gadget defines a relation R over all its variables. Existentially quantifying the internal variables gives a relation eR over the external (input/output) variables, and eR is the gadget's semantics. Given a specification relation S, correctness is eR = S, which splits into:

Soundness, eR ⊆ S: every solution of the constraints satisfies the specification. An under-constrained circuit fails this.
Completeness, S ⊆ eR: every valid instance of the computation has a solution. Completeness proofs have to handle the existential quantifier, usually by giving witnesses for the internal variables.

Soundness alone is not enough: a gadget with no solutions is trivially sound.

Approach 1: whole-gadget proofs over extracted R1CS

The authors built an ACL2 prime-fields library and an ACL2 model of R1CS. Gadgets are pulled out of real systems and converted into that model:

Semaphore (Ethereum Foundation-funded): Circom's compiler can export constraints as JSON, and an ACL2 converter reads that JSON.
Zcash Jubjub elliptic-curve circuits (Tezos Foundation-funded): the Rust gadget code was instrumented, with help from the Zcash team, to emit s-expressions.
Aleo snarkVM: the Rust code was instrumented to emit JSON.

The paper says plainly that extraction is currently trusted. A bug in the instrumentation or conversion "may cause us to unwittingly verify a different gadget from the real one."

Direct ACL2 proofs worked on Semaphore sub-gadgets but became harder as gadgets grew. The authors then built R1CS-specific versions of the Axe lifter and prover. Axe stores terms as DAGs, and the prover alternates rewriting with batched variable substitution. With this they verified soundness, and in some cases completeness, of Semaphore and Zcash sub-gadgets: fixed-size integer operations, elliptic-curve operations, MiMC instances and parts of BLAKE2s. They also verified soundness of the BLAKE2s gadget from an earlier snarkVM version. That one proof "took several person-days to develop and takes several machine-hours to run."

The main limitation of this method is that a flat constraint list loses the gadget hierarchy. Compiler optimisations in Circom and snarkVM blend gadgets together, which "may greatly complicate, or defeat altogether" attempts to recover sub-gadgets during proofs.

Approach 2: compositional proofs ("detached proof-generating extension")

The second method re-implements each gadget construction as an ACL2 function that takes variable names and returns R1CS constraints. The function call hierarchy then mirrors the gadget hierarchy. Each construction is proved correct for a generic prime p and, for families such as n-bit addition, for every n. Sample gadgets extracted from the real library are then checked against the ACL2 output with ground theorems. The authors say this validation currently "amounts to testing" their constructions against the libraries.

Using this method they verified most of the snarkVM gadgets for boolean, field and integer operations, and found two bugs that have since been fixed:

The field-to-bits gadget did not constrain the bits' integer value to be below the prime. The field element 0 could therefore decompose either to all-zero bits or to the bits of p.
The square-root gadget accepted both the positive and the negative root.

Both are non-determinism bugs: one input admits more than one witness. The paper notes that the Aleo mainnet had not launched at that point, so neither bug affected real applications or assets. The authors also found optimisations that save "a large number of constraints in some cases."

PFCS: making internal variables local

Compositional R1CS proofs still have trouble with internal variables. Their names become parameters of every gadget above them, and completeness theorems have to talk about them. Prime Field Constraint Systems (PFCS) is the authors' own formalism and fixes this in two ways. It allows any equality between polynomial expressions, and it adds named, parameterised relations that can be called like functions. A relation's parameters are its external variables. The semantics existentially quantifies the other variables in the relation's body, so a proved sub-gadget can be rewritten directly to its specification inside a larger proof. A lifter turns the deeply embedded PFCS relations into ACL2 predicates for fixed-size gadgets. For parameterised gadgets this step is still done by hand. The authors call the PFCS work "still somewhat preliminary" and were porting the verified snarkVM gadgets to it.

How it compares with automated tools

The paper compares itself with QED2, an SMT solver for finite fields, and Ecne. According to the paper, those tools check whether outputs are uniquely determined by inputs. Kestrel's approach proves full correctness against a specification, and determinism follows from soundness. Kestrel's approach also covers completeness and verifies parameterised circuit families once rather than each instance separately. The authors put the tradeoff as "automation versus generality."

Limits, as stated by the authors

The specifications are written in ACL2 and are not shown to provers or verifiers. Trust in them depends on reviewing the formalisation.
Extraction is trusted. Checking constructions against the library is sample testing for now.
The snarkVM ACL2 work was not open-source when the paper was written.
Planned work includes a proof-generating PFCS-to-R1CS flattener, proof-generating transformations that match snarkVM's optimisations, and verification of the compilers from Aleo instructions to R1CS and from Leo to Aleo instructions.
The conclusion warns that circuit verification is decidable in principle but "practically undecidable" at scale. In the authors' words, larger circuits hit "the program verification wall."

What it means for teams shipping circuits

Both snarkVM bugs were under-constrained decompositions: a bit decomposition with no range check against p, and a square root with no sign constraint. Neither was caught before formal verification. The paper's framework shows why: a circuit can satisfy every honest test vector and still fail soundness, because soundness is a claim about all solutions, not only the intended one. The paper's broader conclusion is that proofs scale only when the circuit structure is kept rather than recovered afterwards. Its stated route is to replicate gadget constructions in a prover and check the replicas syntactically against the real library output.

Timeline

Before mainnet (per the paper): two snarkVM gadget bugs found by compositional verification and fixed.
2023-11-15: arXiv 2311.08858v1 submitted. Published in EPTCS 393 (ACL2-2023), doi:10.4204/EPTCS.393.9.