Introducing clean, a formal verification DSL for ZK circuits in Lean4
We're diving into our new project called **clean**, aimed at creating an embedded DSL and formal verification framework for Zero Knowledge (ZK) circuits using Lean4. Imagine being able to not only define ZK circuits but also formally prove their correctness. Sounds like a game-changer, right? We'll walk you through our process of building a robust library of reusable, verified circuit gadgets, focusing on the importance of soundness and completeness. Plus, you'll get a peek at some cool examples like 8-bit addition and how we're tackling ZKVM design with techniques borrowed from Fibonacci sequences. It's exciting stuff, and if you're curious about how we're paving the way for bug-free ZK circuits, this is a read you won't want to miss!
