We provide a generic framework for formally verifying cryptographic proof systems that are compiled from interactive (oracle) proofs via the Fiat-Shamir transform and (polynomial) commitment schemes.
In the first stage of the project, we formalize interactive (oracle) proofs, and prove information-theoretic completeness and soundness for the class of multilinear-based proof systems.
In particular, we aim to formalize the sum-check protocol and Spartan, both as polynomial IOPs. We also plan to formalize the tensor-based polynomial commitment scheme (PCS), underlying Ligero, Brakedown, and Binius, and prove that Spartan when composed with such a PCS forms a complete & sound interactive proof system.
For each protocol mentioned above, we aim to provide:
- A specification based on (multivariate) polynomials from
Mathlib, - An implementation of the prover and verifier using computable representations of polynomials (see
Data), similar to Rust implementations, - Proofs of completeness and round-by-round soundness for the specification, and proof that the implementation refines the specification.
In future stages, we plan to extend the set of proof systems formalized using our framework, including other hash-based SNARKs based on univariate PCS (e.g. STARKs with FRI / STIR), and other proof systems based on discrete-log or pairings (e.g. Plonk, Spartan with Hyrax, or Nova).
See ROADMAP (somewhat outdated), and the list of issues.
We welcome outside contributions to the library! If you're interested in working on any of the items mentioned in the list of issues or the roadmap, please contact the authors or open a new issue.