Verified-zkEVMClean

Lean circuit DSL

Clean logo

Clean

Chat on Telegram Ask DeepWiki

clean is an embedded Lean DSL for writing zk circuits, targeting popular arithmetizations like AIR, PLONK and R1CS.

Check out our blog post for an introduction: https://blog.zksecurity.xyz/posts/clean

clean is developed by zkSecurity, currently as part of a Verified-zkEVM grant.

We intend to build out clean into a universal zk framework that produces formally verified, bug-free circuits for the entire ecosystem. See the roadmap.

Community

Public Telegram group to discuss clean: t.me/clean_zk

Please join if you want to use clean, or contribute, or if you have any questions!

We always welcome contributors! Check out our good first issues.

Using the repo

Follow official instructions to install elan (the package manager) and Lean4.

Clone this repo, and test that everything works by building:

lake build

After that, we recommend open the repo in VSCode to get immediate inline feedback from the compiler while writing theorems.

Make sure to install the lean4 extension for VSCode!

Documentation

We are actively working on creating proper documentation for clean. In the meantime, we recommend checking out our AI-generated DeepWiki.

⚠️ Disclaimer: The wiki may contain inaccuracies or outdated details. Please take all information with a grain of salt until the official documentation is released.

Code Style

We follow standard Lean/Mathlib conventions with some local variations. See doc/conventions.md for details.

Roadmap

The following is a rough, longer-term roadmap for clean. Note that some of the bullets below could be multi-month projects!

Reach out on TG if you are looking for long-term contribution opportunities and you are interested in any of these!

  • More general lookups + VM-like table ensembles
  • Polish plonky3 backend, generate constraint evaluation Rust code
  • clean documentation
  • Witness generation: compile (subset of) Lean to IR, to generate fast WG code in backends
  • Create clean circuits from LLZK
    • this gives us frontends like Circom
    • subproject: demonstrate actual e2e extraction from Circom
  • Verifier challenges https://github.com/Verified-zkEVM/clean/issues/162
    • prove lookup protocols end to end
    • should be optional, should be able to abstract
  • Explore if we can compose with ArkLib to get e2e verification
  • More backends
    • stwo?
    • some R1CS
  • Support PLONK circuits with custom gates
  • Good AGENTS.md / CLAUDE.md
  • AIR table foundation, more low-level, no monad
    • different entry points for different kinds of tables
  • Support Binius
  • Proof automation:
    • circuit_proof_start should handle vectors and general ProvableTypes
    • circuit_proof_start could detect subcircuits to unfold (in the right places)
    • better automation for localLength_eq, subcircuitsConsistent etc
  • Advanced: Mixed proof systems like Longfellow-ZK
  • MORE GADGETS
  • MORE INTEGRATIONS