Formalization of SNARKs
This repository implements a formal verification of a variety of SNARK proof systems, using the Lean Theorem Prover, in the Algebraic Group Model. This is a work in progress.
As of now there are 6 complete soundness proofs. The full proofs of these theorems can be found at the end of knowledge_soundness.lean in their respective directories.
There is also a file snark_transformations containing various functions for manipulating SNARKs.