In this blog post, we present our work to formally verify the determinism of the Keccak precompile ZK circuits in Plonky3 using our 🍀 Garden framework.
Concretely, this means that:
- This complex circuit is safe for use with all the zkVMs based on Plonky3.
- The 🍀 Garden framework is very expressive and can verify arbitrary circuits, as optimized precompiles are one of the most complex ZK circuits.
The formal verification of the determinism of ZK circuits is important, as this is one of the main sources of critical bugs in zkVMs, and these bugs cannot be found by other means, like testing, while most of the unverified zkVMs have at least one such bug.