# A Soundness Bug in cvc5's Finite Field Split Solver

*How a misplaced overflow check could invalidate the formal verification of Zero-Knowledge programs*

---

Our team at [TBTL](https://tbtl.com/) has discovered and fixed a bug in cvc5's finite-field split solver while testing our formal verifier [NAVe](https://github.com/pedrotbtl/nave); see [PR #12457](https://github.com/cvc5/cvc5/pull/12457). SMT solvers are amazing tools at the core of many formal verification frameworks. They discharge proof obligations to prove that a program works as intended. cvc5 is, arguably, the most well-suited and popular SMT solver for the verification of practical Zero-Knowledge (ZK) programs (circuits, systems, etc), given its performant solvers targeting its theory of finite fields. So, a bug in one of these finite-field solvers can have far-reaching repercussions. A verification framework can erroneously report that a ZK program (circuit, system, etc) is safe when it is not. If a thought-to-be-correct-but-flawed ZK program (circuit, system, etc) is exploited, aside from possibly compromising digital assets or sensitive information that this program was meant to protect, it could significantly undermine the trust in ZK technology and formal verification.

## The Stakes: When Formal Verification Tools (for ZK Technology) Fail

ZK proof systems are among the most security-critical components in modern cryptographic infrastructure. They underpin privacy-preserving blockchains, anonymous credentials, and verifiable computation protocols that collectively secure billions of dollars in value and protect sensitive data. Many applications of ZK technology have emerged in the Web3 space. Ethereum's [lean consensus roadmap](https://leanroadmap.org/) relies heavily on ZK technology for a number of improvements on this platform. Ethereum Layer 2 (L2) solutions -- such as ZKSync, Aztec, Starknet, to name a few -- and protocols like [tornado cash](https://tornado.cash/) also use ZK technology to ensure privacy and/or scalability. Just to illustrate the risks involved, several of these L2 solutions have hundreds of millions of dollars in total value secured, a metric associated with the value of the tokens protected by them. Also, ZK proofs are being used in the privacy-preserving identity verification -- see projects like [ZK passport](https://zkpassport.id/). So, personal information is at stake too.

To ensure that these vast sums of digital assets and sensitive information are well protected, formal verification techniques have been applied to guarantee that ZK technology (program, circuit, VM, protocols, etc) behaves correctly. These techniques use mathematical models to *prove* that ZK programs (circuits, systems, etc) correctly encode the intended computation. [Bugs found in the wild](https://bugs.zksecurity.xyz/) demonstrate the necessity of audits and the use of formal verification to ensure their correctness. With the growth of the ZK ecosystem -- driven, especially, by Web3 applications -- tools to formally analyse ZK technology started emerging, and they will likely play a key role in protecting this ecosystem. To name a few examples: [Picus](https://github.com/Veridise/Picus) is a formal verifier for ZK circuits, [CirC](https://github.com/circify/circ) is a compiler infrastructure that can be used to reason about ZK circuits, [NAVe](https://github.com/pedrotbtl/nave) -- our tool -- is a formal verifier ZK programs written in Noir, and [CertiPlonk](https://github.com/NethermindEth/CertiPlonk) is a framework formally verifying constraint systems from the Plonky3 zkDSL. All of them rely on cvc5 to reason about ZK technology; Picus (at least the open-source version) and NAVe use the split solver -- we discovered (and fixed) this bug while testing NAVe.

The promise of formal verification is that a passing verdict is trustworthy: if the tool says a program is correct, then it must be so. When the formal verification tool itself contains a soundness bug, however, that promise is broken in the most dangerous possible way. The tool may report that a flawed circuit is safe, without any indication that something has gone wrong, and the flaw may be exploited to compromise digital assets or personal data, undermining the trust in both the ZK ecosystem and formal verification. Using formal verification in this space is a must, and we must also work towards ensuring these tools (and their reasoning engines, i.e. SMT solvers) are sound.

## SMT Solvers: The Engines of Automated Formal Verification

Satisfiability Modulo Theories (SMT) solvers are general-purpose automated reasoning engines that sit at the heart of a vast ecosystem of formal verification tools. They employ a number of decision procedures with performant heuristics to tackle challenging computational problems. Years of research and engineering achievements have culminated in these highly optimised solvers. Their importance for the area of automated formal verification cannot be overstated: they are absolutely indispensable.

Given a logical formula -- say, representing a property of a program, a circuit, or a system -- an SMT solver will either produce a model demonstrating that the formula can be satisfied, or a proof that it cannot. This makes them invaluable for checking safety properties: if you can express "there exists an input for which this program is wrong" as an SMT formula and the solver returns *unsatisfiable*, you have a machine-checked proof of correctness.

[cvc5](https://cvc5.github.io/) is one of the most capable and actively maintained SMT solvers. Developed by a collaboration of leading academic institutions and industrial research labs, it has consistently ranked among the top performers in international SMT competitions. Its open architecture, rich API, and breadth of supported theories make it a natural building block for verification tools targeting domains from software verification to cryptography.

## Finite Fields and ZK Program Verification

The constraints that capture the behaviour of a ZK program are given by a system of polynomial equations over a finite field $F$. For instance, a very basic example is the definition of a boolean variable in a ZK program: `let b : bool`, which can be captured by constraint $B \equiv w_b(w_b-1) = 0$, where the notation $X \equiv eq$ means that $X$ is a short name for the equation $eq$ and $B$ stands for behaviour. The *witness* $w_b \in F$ captures the value of the program variable `b`; the values of the program variables at different program points are captured by these witness variables. This equation ensures that out of all the possible elements in the finite field, this witness can only be 0 or 1. Each statement in a ZK program leads to such a constraint (or a set of these), which combine to create a system of equations defining the program's behaviour.

A safety property of a ZK program can then be encoded as such a constraint too, using even propositional connectors and inequalities. For instance, the property that `b` must be either 0 or 1 could be checked by trying to find a counterexample for it: a value of `b` that is neither 0 nor 1. This could be encoded as the constraint $P \equiv w_b \neq 0 \land w_b \neq 1$ with respect to the witness $w_b$; $P$ stands for property. With constraints $B$ and $P$, we can check the satisfiability of $B \land P$. If this SMT formula is satisfied, there exists a value of $w_b$ that violates our property. If this formula is unsatisfiable, as it is the case, we have proven that the only two possible values for $w_b$ are 0 and 1. This satisfiability checking can be carried out by an SMT solver like cvc5, with its theory of finite fields. ZK programming and property languages are quite expressive. Here, we present a very contrived example for the sake of simplifying our presentation.

## Finite Field Solvers in cvc5

cvc5 is one of the first general-purpose SMT checkers capable of reasoning natively about finite field arithmetic. The *gb* solver described in [Ozdemir et al. (2023)](https://eprint.iacr.org/2023/091.pdf) was cvc5's first finite field solver; its name is derived from [*Gröbner basis*](https://en.wikipedia.org/wiki/Gr%C3%B6bner_basis): a representation of a system of polynomials that allows for efficient computations. Simply put, this solver takes a set of polynomial equations over a finite field and establishes whether the set of solutions for this system is empty; a key procedure in reasoning about a finite-field-theory formula. If it is not, it provides a solution: a mapping of witnesses to values that satisfies the system. The key insight presented in the corresponding paper and implemented in this solver is that the very large order of prime fields used by practical systems (like the ones behind ZK proof systems) makes the typical way of checking for emptiness not very performant. It relies on the computation of the Gröbner basis for the system extended with field equations of the form $w^p - w$ for each witness variable, where $p$ is the prime order of the field. Instead, this solver uses a combination of the Gröbner basis calculation for the (unextended) system with a technique called *model construction*, where the space of potential solutions is explored with a carefully designed heuristic.

<!-- The key insight presented in the corresponding paper and implemented in this solver is that for practical systems where the order of a prime field is very large (like the ones behind ZK proof systems), the typical way of checking for emptiness -- i.e. computing the Gröbner basis for the system extended with field equations of the form $w^p - w$ for each witness variable, where $p$ is the prime order of the field -- is not very performant, thanks to the large orders. -->

A follow-up work, [Ozdemir et al. (2024)](https://eprint.iacr.org/2024/572.pdf), has introduced the *split* solver variant: a solver that was designed to target bitsum-heavy programs. A *bitsum* expression $bitsum(b_0,\ldots,b_n)$ denotes the sum $\sum^n_{i=0} b_i*2^i$. Each $b_i$ is *intended* to represent a single bit but, despite what its name may suggest, this expression alone does not impose this restriction; separate bit constraints of the form $b_i(b_i-1) = 0$ are necessary to enforce that. These types of constraints can capture the bit-decomposition of a finite-field value, which can, in turn, encode bit-level operations, for instance. The Gröbner-basis computation for these constraints is very demanding: the time to compute them grows exponentially with the number of bits/elements in the bitsum. The key insight was to use a *split* Gröbner basis: a combination of easier-to-calculate Gröbner bases that approximate the basis for the full system. Computing a basis for a bitsum expression *combined with* its bit constraints is expensive, as we discussed. However, analysing the bitsum expression and the bit constraints separately can be much cheaper. The split solver maintains a split basis with two Gröbner bases, one linear and one sparse, propagating information between them to accelerate convergence. They are carefully designed so that a bitsum expression and the corresponding bit constraints are always in separate bases.

## Bug Discovery During NAVe Testing

We encountered the bug described here in the course of testing [NAVe](https://arxiv.org/pdf/2601.09372), our formal verifier for programs written in [Noir](https://noir-lang.org/) -- the domain-specific language used to author ZK circuits for the Aztec protocol. NAVe uses the Noir language infrastructure (parser, compiler, etc) to translate Noir programs into ACIR (Abstract Circuit Intermediate Representation). It then encodes ACIR opcodes into SMT-LIB constraints that are analysed by cvc5 and its finite field solvers; in our paper, we describe the formal semantics we propose for ACIR. During the testing of NAVe against a suite of Noir programs, we observed that cvc5's split solver was returning an *unsatisfiable* verdict for a satisfiable formula. This failure in the underlying solver means that NAVe, and any other tool relying on cvc5's *split* finite field theory solver, could in principle report a circuit as verified when it is not.

## Minimising the Error to a Regression Test

Isolating a solver bug requires reducing a potentially large, complex formula down to the smallest possible instance that still triggers the erroneous behaviour. This minimisation process is as much art as science: it involves an iterative cycle of pruning variables, simplifying constraints, and re-running the solver to check that the bug is still reproducible. After this process, we reduced the failing case to a five-line SMT-LIB 2 formula that became the regression test accompanying our fix:

(set-logic QF_FF)
(define-sort FF () (_ FiniteField 21888242871839275222246405745257275088548364400416034343698204186575808495617))
(declare-const _0 FF)
(declare-const _1 FF)
(assert (= (ff.add (ff.mul (as ff-2 FF) _0) (ff.mul (as ff-1 FF) _1) (as ff4 FF)) (as ff0 FF)))
(check-sat)

This asserts that $-2w_0 − w_1 + 4 = 0$, i.e. that $2w_0 + w_1 = 4$, over a prime finite field of large order. In the SMT-LIB constraint, the constant `_i` denotes the witness variable $w_i$ and `(as ffi FF)` denotes the field element $i$. This linear equation has $w_0 = 0$ and $w_1 = 4$ as a solution or $w_0 = 2$ and $w_1 = 0$, among others. So, this formula is unequivocally satisfiable. The original split solver returned *unsat*; the unsatisfiable veredict.

## The Flaw: A Premature Overflow Check

The bug lives in the `BitProp::getBitEqualities` method in `src/theory/ff/split_gb.cpp`, which we present below. The split solver tracks bitsum expressions. The solver checks whether any of the Gröbner bases in the split basis has reduced a bitsum to a constant, i.e. it derived a constraint of the form: $bitsum(b_0,\ldots,b_{n-1}) = C$. If this bitsum of $n$ elements evaluates to a constant $C$ such that $C \geq 2^n$, then the bits cannot all be 0 or 1 while summing to $C$ -- an impossibility that causes the solver to return *unsat*. This overflow check is carried out on line 412.

Polys BitProp::getBitEqualities(const SplitGb& splitBasis)
{
  Polys output{};

  std::vector<Node> bitConstrainedBitsums{};

  std::vector<Node> nonConstantBitsums{};
  for (const auto& bitsum : d_bitsums)
  {
    // does any basis know `bitsum = k`?
    bool isConst = false;
    for (const auto& b : splitBasis)
    {
      Poly normal = b.reduce(d_enc->getTermEncoding(bitsum));
      if (CoCoA::IsConstant(normal))
      {
        // this basis b knows that bitsum is a constant
        Integer val =
            d_enc->cocoaFfToFfVal(CoCoA::ConstantCoeff(normal)).getValue();
        if (val >= Integer(2).pow(bitsum.getNumChildren()))
        {
          output.clear();
          output.push_back(CoCoA::one(d_enc->polyRing()));
          return output;
        }

        // check that all inputs are bit-constrained
        if (std::all_of(bitsum.begin(), bitsum.end(), [&](const Node& bit) {
              return isBit(bit, splitBasis);
            }))
        {
        ... 

The critical precondition for this reasoning is that the summands actually *are* bits. The overflow check is only meaningful if every element of the bitsum is known to be 0-or-1 constrained. In the original code, however, the overflow check was executed *without* verifying that the summand elements are bit-constrained. Coincidentally, a check of whether the elements of the bitsum are bit-constrained (using the method `isBit`) came right after in line 420, guarding a separate propagation step. So, although a constraint of the form $bitsum(b_0,\ldots,b_{n-1}) = C$ can always be satisfied for any $C$ -- a solution is found by setting $b_0 = C$ and all other $b_i$s to $0$ -- this erroneous check would cause this constraint to be unsatisfiable for any $C \geq 2^n$. Also, note that it would only take a single such constraint to possibly generate an unsat veridict for the entire input formula.

### How the Regression Triggers an Unsound Unsat Output

The regression test is analysing the satisfiability of the constraint $2w_0 + w_1 = 4$, which can be rewritten as $RW \equiv bitsum(w_1,w_0) = 4$; the solver does this rewriting to derive as much information as possible from bitsum constraints, even if they were not originally encoded explicitly as such. These witness variables are unconstrained finite field elements -- they carry no bit constraints whatsoever. The split solver, in the context of the bit propagation pass, identifies the rewritten bitsum constraint $RW$ and proceeds to the flawed overflow check. Given that this bitsum has 2 elements, it proceeds to validate the overflow condition $4 \geq 2^2$, and it propagates this information into an unsound unsat output.

### The Fix: Moving the Overflow Check Inside the Right Guard

The repair is small: a careful rearrangement of the existing logic. In the fixed code, the overflow check is moved inside the branch that first confirms all bitsum elements are bit-constrained. Only after `isBit` has been verified for every summand does it make sense to assert that a constant value exceeding $2^n$ represents a genuine contradiction. The fixed code is presented below.

Polys BitProp::getBitEqualities(const SplitGb& splitBasis)
{
  Polys output{};

  std::vector<Node> bitConstrainedBitsums{};

  std::vector<Node> nonConstantBitsums{};
  for (const auto& bitsum : d_bitsums)
  {
    // does any basis know `bitsum = k`?
    bool isConst = false;
    for (const auto& b : splitBasis)
    {
      Poly normal = b.reduce(d_enc->getTermEncoding(bitsum));
      if (CoCoA::IsConstant(normal))
      {
      
        // check that all inputs are bit-constrained
        if (std::all_of(bitsum.begin(), bitsum.end(), [&](const Node& bit) {
              return isBit(bit, splitBasis);
            }))
        {
          // this basis b knows that bitsum is a constant
          Integer val =
              d_enc->cocoaFfToFfVal(CoCoA::ConstantCoeff(normal)).getValue();

          if (val >= Integer(2).pow(bitsum.getNumChildren()))
          {
            output.clear();
            output.push_back(CoCoA::one(d_enc->polyRing()));
            return output;
          }
          ...

This restores the correct precondition: the overflow check is only invoked when the solver has established that it is working with genuine boolean summands. The fix was small, consisting of moving six lines of code, but it is the difference between a sound and an unsound verdict. Also, the quality of the code simplified the task of identifying the bug and implementing the fix. The fix was reviewed and approved by Alex Ozdemir, one of the original authors of the split solver, who confirmed the bug and fix before the PR was merged into cvc5 main on February 27, 2026.

## The Expertise Required

Understanding and fixing this bug demanded expertise across several technical domains. At the mathematical level, one needs a solid grasp of algebra in what concerns the analysis of a system of polynomial equations over a finite field of prime order and its set of solutions -- for instance, how Gröbner bases can be used to determine the existence of a solution in this specific context. These are the mathematics required to understand both the gb and split solver papers. At the systems level, one needs to understand the architecture of a production SMT solver -- how theories are modularised, how the DPLL(T) loop interacts with theory solvers, and how propagation and conflict detection work in the finite field backend specifically. Finally, one needs the analytical skills to work backwards from an incorrect verdict through a chain of solver decisions to identify a misplaced condition -- without which the fix would be inaccessible even to an expert who understood each component in isolation. The difficult task of identifying and correcting the bug was considerably simplified by the documentation available and the code quality of the finite field solvers. We are grateful to the cvc5 team for their receptiveness, rapid review, and the impressive work that supports this entire ecosystem of high-assurance verification.