Today we’ll introduce “Satisfiability Modulo Finite Fields” (SMFF): a recent research paper that promises to make verifying ZK systems easier.
The paper is authored by Alex Ozdemir from Stanford University, who’s currently doing an internship at Veridise, and by Gereon Kremer (Stanford University), Cesare Tinelli (University of Iowa) and Clark Barrett (Stanford University).
But back to SMFF.
SMFF is exciting because it allows traditional verification techniques to be applied to the ZK domain.
Let’s start with traditional program verification. As we explained in a previous article, an automated verification tool usually has two parts: the Verification Condition (VC) generator and the automatic theorem prover.
The generator compiles a program and a specification for what that program should do into VCs: logical formulas (also known as theorems) that are true if and only if the program is correct. These VCs are then checked using the automatic theorem prover, typically an SMT Solver.
This approach is effective, but it relies on a key assumption: that the SMT solver understands the primitive types used by the program.
For most programs and programming languages, this assumption is true because SMT solvers understand many different types: Booleans, arbitrary-precision integers, machine integers, arrays, strings, algebraic data types, and more. For example, this approach works well for programs compiled to LLVM, where all operations are done with machine integers: integers modulo a power of two.
However, ZK programming languages use an unusual primitive type. As we discussed in another previous article, their primitive type is a finite field. For instance, if the ZK system uses the BLS12–381 elliptic curve, then its finite field is the set of integers {0, 1, 2, …, p − 1} modulo a large prime p¹. Moreover, the only primitive operations are addition and multiplications modulo p.
Finite fields are hard for verification, because existing SMT solvers don’t support them.
Of course, when the finite field is just the integers modulo p, one natural approach is to encode field elements as integers, and have the SMT reduce modulo p after every operation.
In theory, this works: you can use either arbitrary-precision integers, or machine integers with at least 2 • ⌈ log p⌉ bits. But unfortunately, this is inefficient in practice. Modular reduction for integers is complex: the SMT solver struggles to reason efficiently about it, so the program verifier doesn’t finish on complex programs.
This is where SMFF comes into play: the idea is simply to teach an SMT solver how to understand finite fields.
In the recent paper “Satisfiability Modulo Finite Field”, Alex Ozdemir et al. add native finite-field reasoning to an SMT solver. They use a number of tools from computer algebra (Groebner bases, triangular decomposition, and minimal polynomials) to extend the cvc5 SMT solver to finite-fields.
Their experiments show that the field-native solver is better for verification than previous approaches. In the experiments, they apply their new solver to some basic VCs related to ZK systems.
They find that cvc5 with field reasoning (“ff-cvc5”, “ff-cvc5-nocore”) can verify VCs far faster than SMT with an integer encoding of field operations (“nia-cvc5”, “nia-z3”), SMT with a machine-integer encoding of field operations (“bv-bitwuzla”), or computer algebra tools without SMT (“pureff-cvc5”).
At Veridise, we’re very excited about Satisfiability Modulo Finite Fields. In fact, we’ve been using cvc5’s new field reasoning engine inside many of our ZK verification tools.
If you’re working on ZK verification too, you definitely want to check out Alex’s SMFF paper:
