eprint.iacr.org will be offline for approximately an hour for routine maintenance at 11pm UTC on Tuesday, April 16. We lost some data between April 12 and April 14, and some authors have been notified that they need to resubmit their papers.

Paper 2023/656

Formalizing Soundness Proofs of SNARKs

Bolton Bailey, University of Illinois Urbana-Champaign
Andrew Miller, University of Illinois Urbana-Champaign

Succinct Non-interactive Arguments of Knowledge (SNARKs) have seen interest and development from the cryptographic community over recent years, and there are now constructions with very small proof size designed to work well in practice. A SNARK protocol can only be widely accepted as secure, however, if a rigorous proof of its security properties has been vetted by the community. Even then, it is sometimes the case that these security proofs are flawed, and it is then necessary for further research to identify these flaws and correct the record. To increase the rigor of these proofs, we turn to formal methods. Focusing on the soundness aspect of a widespread class of SNARKs, we formalize proofs for six different constructions, including the well-known Groth '16. Our codebase is written in the Lean 3 theorem proving language, and uses a variety of techniques to simplify and automate these proofs as much as possible.

Available format(s)
Cryptographic protocols
Publication info
SNARKsFormal Methods
Contact author(s)
boltonb2 @ illinois edu
soc1024 @ illinois edu
2023-05-11: approved
2023-05-09: received
See all versions
Short URL
Creative Commons Attribution


      author = {Bolton Bailey and Andrew Miller},
      title = {Formalizing Soundness Proofs of SNARKs},
      howpublished = {Cryptology ePrint Archive, Paper 2023/656},
      year = {2023},
      note = {\url{https://eprint.iacr.org/2023/656}},
      url = {https://eprint.iacr.org/2023/656}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.