Home > Resources > papers > CMSCGD23-ZK-Circuit-Verification

Compositional Formal Verification of Zero-Knowledge Circuits (Coglio, McCarthy, Smith, Chin, Gaddamadugu, Dellepere 2023)

Last modified: 2026-10-27

DOI: 10.4204/eptcs.393.9 · URL: https://eprint.iacr.org/2023/1278

Summary

Presents a compositional approach to formally verifying that R1CS circuits (as generated by the Leo/snarkVM toolchain) correctly implement their intended specification, using the ACL2 theorem prover. Correctness proofs of gadgets are reused when proving larger circuits. Cited in BL26-SoK-AnonCreds as work towards tool-supported verification of circuits, needed because under-constrained circuits are a major source of forgery bugs.

Related resources

• Formalizing Soundness Proofs of SNARKs (Bailey, Miller 2023) (paper, 2023)
• SoK: What Don't We Know? Understanding Security Vulnerabilities in SNARKs (Chaliasos, Ernstberger, Theodore, Wong, Jahanara, Livshits 2024) (paper, 2024)