We are really excited to share our initial steps towards building clean, an embedded DSL and formal verification framework for ZK circuits in Lean4. As we recently shared, Zero Knowledge circuits are full of bugs, but fortunately, techniques like formal verification can provide a huge confidence boost in the correctness of ZK circuits. Clean enables us to define circuits in Lean4, specify their desired properties, and – most importantly – formally prove them! This work is part of the zkEVM Forma...