Formally Verifying Noir Zero Knowledge Programs with NAVe

TL;DR

This work addresses the difficulty of ensuring Noir ZK programs faithfully enforce the intended relation $R(X,W)$ by formalising a subset of ACIR in SMT-LIB and implementing NAVe, an open-source verifier integrated with Nargo. It introduces two SMT encodings (finite-field and integer) to model ACIR opcodes and supports verification goals via verify_assert, using cvc5 to detect underconstrained or otherwise incorrect program behavior. The evaluation on Noir test programs reveals that some constraints, notably range checks, are expensive to verify and that the two encodings can complement each other, motivating concurrent solver use and future abstractions. Overall, NAVe provides automated, architecture-aware verification for high-level ZK languages and offers a path toward scalable formal verification of Noir programs and similar DSLs targeting ACIR.

Abstract

Zero-Knowledge (ZK) proof systems are cryptographic protocols that can (with overwhelming probability) demonstrate that the pair $(X, W)$ is in a relation $R$ without revealing information about the private input $W$. This membership checking is captured by a complex arithmetic circuit: a set of polynomial equations over a finite field. ZK programming languages, like Noir, have been proposed to simplify the description of these circuits. A developer can write a Noir program using traditional high-level constructs that can be compiled into a lower-level ACIR (Abstract Circuit Intermediate Representation), which is essentially a high-level description of an arithmetic circuit. In this paper, we formalise some of the ACIR language using SMT-LIB and its extended theory of finite fields. We use this formalisation to create an open-source formal verifier for the Noir language using the SMT solver cvc5. Our verifier can be used to check whether Noir programs behave appropriately. For instance, it can be used to check whether a Noir program has been properly constrained, that is, the finite-field polynomial equations generated truly capture the intended relation. We evaluate our verifier over 4 distinct sets of Noir programs, demonstrating its practical applicability and identifying a hard-to-check constraint type that charts an improvement path for our verification framework.

Figures (4)

• Figure 1: Noir programs: constrained vs unconstrained.
• Figure 2: Overview of NAVe formal verifier.
• Figure 3: Basic example program.
• Figure 4: Regression test programs without (excerpt of $\textit{prv}_{13}$ with range check removed) and with ($\textit{prv}_{14}$) range-check opcode, respectively.