Introduction
Zero-Knowledge in all its forms is a strong suit for Veridise. In addition to auditing some of the largest infrastructure ZK projects and dapps, we actively contribute to academic research on zero-knowledge proofs.
We recently published a paper at the Computer Aided Verification (CAV) Conference 2024 titled: Split Gröbner Bases for Satisfiability Modulo Finite Fields.
This paper was authored by Alex Ozdemir (Stanford University, Veridise), Shankara Pailoor (Veridise), Alp Bassa (Veridise), Kostas Ferles (Veridise), Clark Barrett (Stanford University) and Işil Dillig (Veridise).
Abstract of the paper
Satisfiability modulo finite fields enables automated verification for cryptosystems. Unfortunately, previous solvers scale poorly for even some simple systems of field equations, in part because they build a full Gröbner basis (GB) for the system. We propose a new solver that uses multiple, simpler GBs instead of one full GB. Our solver, implemented within the cvc5 SMT solver, admits specialized propagation algorithms, e.g., for understanding bitsums. Experiments show that it solves important bitsum-heavy determinism benchmarks far faster than prior solvers, without introducing much overhead for other benchmarks.
A more approachable introduction
Recall that a ZK circuit is a set of polynomial equations over a finite field. As such, most of our SMT (Satisfiability Modulo Theory) based tools reduce questions about circuit correctness to the question of whether certain polynomial equations have solutions or not.
For example, given a circuit C(x̄ , ȳ) with inputs x̄ and ȳ, we can check C is underconstrained by discharging the following query to an SMT solver:

If there is a solution, then there is a high chance the circuit has an underconstrained bug.
Solving these polynomial equations is a classical problem, occupying mathematicians for a long time (even centuries, depending on how you interpret the questions). Recent efforts in this direction have been going on under the names computer algebra/computational commutative algebra/computational algebraic geometry.
One of the main tools is Gröbner Bases
Gröbner Bases basically allow you to do the following: given a set of equations, you turn them into a new set of equations (called a Gröbner Basis) that is more amenable for computations and formal reasoning. They form the fundamental tool for many computational problems involving polynomials.
There is a classical algorithm, called the Buchberger Algorithm, to compute Gröbner Bases, which does not scale well as the number of constraints grow. Unfortunately, this poses a problem, as most ZK circuits you might want to verify tend to be huge, consisting of many equations in many variables.
Moreover, most circuits involve some bit operations (operations on bit representations), which are not very easy to deal with for Gröbner Bases algorithms. Even if there are no bitwise operations, often range constraints in ZK circuits (statements like x is between the values 0 and 63, for instance) are expressed using bit operations (x can be written using a binary representation with 8 bits). This difficulty of Gröbner Basis engines with bit operations (which by themselves are not necessarily too difficult) causes many tools to reach their limits quickly.
Split Gröbner Bases
In the research paper, we introduce something called split Gröbner Bases.
Rather than computing a Gröbner Basis for the whole system, we separate it into smaller chunks with different characteristics, each of which can be dealt with more easily by themselves. This helps push the limits of what can be done with the tools quite a lot.
Here a figure form the paper, demonstrating the gains in efficiency when splitting the Gröbner Basis.

In the graph above, the x-axis is the difficulty of the problem being considered. The y-axis is the amount of time needed. The turquoise graphs are the previous monolithic solver that does not split the problem into parts. You can see that the required time grows exponentially as a function of problem size, making tools based on these solvers unusable once the problem exceeds a certain size. However, as you can see, once the problem is split the right way, the runtime is nearly instantaneous! This does not apply to all benchmarks; a few of them, like bvudiv and bvurem, are waiting to be tackled in future work 🙂
Download the paper
Split Gröbner Bases for Satisfiability Modulo Finite Fields.
Download the paper here:
https://eprint.iacr.org/2024/572 (Cryptology ePrint Archive)
Other ZK research by Veridise team members

Beyond the paper covered in this article, Veridise team members have published and collaborated on many research papers related to zero-knowledge proofs, such as:
- Certifying Zero-Knowledge Circuits with Refinement Types
- Automated Detection of Under-constrained Circuits in Zero-Knowledge Proofs
- Practical Security Analysis of Zero-Knowledge Proof Circuits
You can read more about our ZK research and these paper in a separate blog post.
Author:
Alp Bassa, Head of Cryptography at Veridise