Home > Resources > papers > BM23-Formalizing-SNARK-Soundness

Formalizing Soundness Proofs of SNARKs (Bailey, Miller 2023)

Last modified: 2026-10-27

URL: https://eprint.iacr.org/2023/656

Summary

Mechanizes soundness proofs of SNARK constructions in the Lean theorem prover, so that a proof system's security argument can be machine-checked rather than only reviewed by hand. Cited in BL26-SoK-AnonCreds as ongoing work towards formal verification of proof systems, which it considers essential given the complexity of general-purpose ZKPs.

Related resources

• Compositional Formal Verification of Zero-Knowledge Circuits (Coglio, McCarthy, Smith, Chin, Gaddamadugu, Dellepere 2023) (paper, 2023)
• SoK: What Don't We Know? Understanding Security Vulnerabilities in SNARKs (Chaliasos, Ernstberger, Theodore, Wong, Jahanara, Livshits 2024) (paper, 2024)