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

Check out the Clean Website for more information

Development

The clean framework is developed by zkSecurity, currently funded by the Verified-zkEVM grant.

Community

The Clean website explains how anyone can get started with Clean.

If you have questions, or want to contribute, please join our Public Telegram group t.me/clean_zk. We are happy to answer any questions or just discuss!

We love 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.

Proof Finding Guide

Some heuristics for finding proofs are in doc/proving-guide.md.

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
  • main refactor merged as https://github.com/Verified-zkEVM/clean/pull/328
  • subproject (TODO): support in plonky3 backend
• Polish plonky3 backend, generate constraint evaluation Rust code
  • currently worked on by zkSecurity https://github.com/Verified-zkEVM/clean/pull/192
• clean documentation
  • will be worked on by zkSecurity
• ✅ Witness generation: compile (subset of) Lean to IR, to generate fast WG code in backends
  • solved by moving to a witness generation IR https://github.com/Verified-zkEVM/clean/pull/403
• 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

Attribution

The Lean name and logo are trademarks of Lean FRO.