# AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs

arXiv: https://arxiv.org/abs/2403.15676 · HTML: https://mlsanity.com/paper/2403.15676/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 69 references that are in the map.
- First posted on arXiv 23 Mar 2024.

## Builds on (most cited first, 6 of 6)

- [SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics](https://mlsanity.com/paper/1907.04408/) (2019)
- [Certifying Zero-Knowledge Circuits with Refinement Types](https://mlsanity.com/paper/2304.07648/) (2023)
- [SMT Solving over Finite Field Arithmetic](https://mlsanity.com/paper/2305.00028/) (2023)
- [Data-Flow-Based Normalization Generation Algorithm of R1CS for Zero-Knowledge Proof](https://mlsanity.com/paper/2309.04274/) (2023)
- [Formal Verification of Zero-Knowledge Circuits](https://mlsanity.com/paper/2311.08858/) (2023)
- [MCSat-based Finite Field Reasoning in the Yices2 SMT Solver](https://mlsanity.com/paper/2402.17927/) (2024)

## Abstract (arXiv)

Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This paper introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system. The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC4, is proposed to represent the implementation of the method. Experiments show that AC4 demonstrates a increase in the solved rate, showing a 29% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.