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!

Using Clean as a dependency

Every Lean toolchain bump on main creates a release tagged with the toolchain version, e.g. v4.34.1. Newer main commits on the same toolchain are released by hand as v4.34.1-patch1, v4.34.1-patch2, etc. Each release carries a prebuilt Clean library, which Lake downloads instead of compiling Clean when your project pins the release tag:

require Clean from git "https://github.com/Verified-zkEVM/clean" @ "v4.34.1"

The prebuilt library only works with the release's exact toolchain. A project that pins a main commit without a release tag builds Clean from source; Lake then warns that it found no release, which fails lake build --wfail.

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 Verified-zkEVM#328
  • subproject (TODO): support in plonky3 backend
• Polish plonky3 backend, generate constraint evaluation Rust code
  • currently worked on by zkSecurity Verified-zkEVM#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 Verified-zkEVM#403
• Create clean circuits from LLZK
  • this gives us frontends like Circom
  • subproject: demonstrate actual e2e extraction from Circom
• Verifier challenges Verified-zkEVM#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.