A friendly framework to formally verify zero-knowledge circuits 🍀
It is a common consensus that, in order to be ready for the Ethereum L1, zkVMs must be formally verified. This includes verifying the circuit constraints, which are one of the most critical parts of a zkVM. With Garden, we provide a friendly framework in the Rocq formal system to make sure that the three main properties of a circuit hold:
- Determinism: only one possible trace for each input;
- Functional correctness: the circuit computes the right output (typically the RISC-V semantics);
- Completeness: the circuit never blocks.
You can get more details about the properties to verify in our blog post 🦄 What to verify in a zkVM. The list of zkVMs with their formal verification status is maintained on Ethproofs.org.
The Garden framework aims to be:
- Effective: the formal verification of circuits must be efficient, as this is a competitive space;
- Maintainable: no black magic;
- Tied to the code: the formal model must be tied to the code generating the circuits, not the low-level constraints themselves.
We provide several examples (many of which are Work in Progress at the moment) about:
- The verification of pre-compiles (Blake3, Keccak, and Sha256);
- The verification of an OpenVM chip (BranchEq)
We handle circuits at the implementation level in:
Our biggest example is the formal verification of the implementation of Keccak in Plonky3. You can find:
- The verification in Garden/Plonky3/keccak/proofs/air.v
- The constraints snapshot in Garden/Plonky3/keccak/air.snapshot, that we generate to make sure we have the same definition as in the implementation in Plonky3
- The source implementation of Keccak in Plonky3: https://github.com/Plonky3/Plonky3/tree/main/keccak-air/src
You can look at the build instructions in the BUILD.md file.
For more information or to discuss security, please get in touch with us at [email protected]!
Here are some related projects:
You can make a pull request to add your project if we are missing something!
