Paper 2025/916
Automated Verification of Consistency in Zero-Knowledge Proof Circuits
, The University of Texas at Austin, Veridise Inc, Veridise Inc, The University of Texas at Austin, Veridise IncAbstract
Circuit languages like Circom and Gnark have become essential tools for programmable zero-knowledge cryptography, allowing developers to build privacy-preserving applications. These domain-specific languages (DSLs) encode both the computation to be verified (as a witness generator) and the corresponding arithmetic circuits, from which the prover and verifier can be automatically generated. However, for these programs to be correct, the witness generator and the arithmetic circuit need to be mutually consistent in a certain technical sense, and inconsistencies can result in security vulnerabilities. This paper formalizes the consistency requirement for circuit DSLs and proposes the first automated technique for verifying it. We evaluate the method on hundreds of real-world circuits, demonstrating its utility for both automated verification and uncovering errors that existing tools are unable to detect.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Published elsewhere. Minor revision. CAV'25
- Keywords
- Zero KnowledgeVerificationConsistencyAutomated Verification
- Contact author(s)
-
jon @ cs utexas edu
shankara @ veridise com
isil @ cs utexas edu - History
- 2025-05-23: approved
- 2025-05-21: received
- See all versions
- Short URL
- https://ia.cr/2025/916
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2025/916,
author = {Jon Stephens and Shankara Pailoor and Isil Dillig},
title = {Automated Verification of Consistency in Zero-Knowledge Proof Circuits},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/916},
year = {2025},
url = {https://eprint.iacr.org/2025/916}
}
