Clean

Direct answerClean is an embedded Lean 4 language for writing zero-knowledge circuits in which every gadget carries a machine-checked proof of both soundness (any satisfying witness meets the specification) and completeness (every valid input has a satisfying witness). Created and maintained by zkSecurity, it targets AIR-style tables with lookups, PLONK and R1CS, composes verified gadgets into larger verified circuits, and since June 2026 models cross-table interactions so that whole multi-table systems such as zkVMs can be proved sound.

Maintainer: zkSecurity (hosted under Verified-zkEVM)
Website: https://clean.zksecurity.xyz
Repository: https://github.com/Verified-zkEVM/clean
Category: ZK circuit verification
Targets: AIRPLONKR1CSzkVM chipsPlonky3-style tables
Approach: Embedded Lean 4 DSL; proof assistant; soundness and completeness theorems per gadget, composed without re-proving
Access: Open source (MIT)
Status (2026-09-13): Active, funded by an Ethereum Foundation Verified zkEVM grant
First public release: 2025-03-27 (public introduction)

Last reviewed 2026-09-13 by the sorryfree editors.

What Clean does

A Clean circuit is built from four operations: Witness (allocate a cell), Assert (add a constraint), Lookup (table membership) and Subcircuit (call a previously verified gadget). A FormalCircuit bundles input and output shapes, assumptions, a specification, a soundness proof and a completeness proof. Because the specification is stated over ordinary Lean values rather than field elements, a proof that a SHA-256 gadget is sound is a statement about the real SHA-256 function from Mathlib-style definitions, not about a re-encoding of it.

Requiring completeness as well as soundness is the design decision that separates Clean from most other circuit frameworks. Soundness alone is satisfied by an unsatisfiable circuit, so a soundness-only proof does not tell you the circuit works. The pairing is what makes it safe to accept circuits written by untrusted parties, including LLM agents, which is the model behind zk.golf.

Verified gadgets published by zkSecurity include Keccak-f, SHA-256, BLAKE3, circomlib's Poseidon (arity 1, sound and complete, with BN254 primality discharged by a Pratt certificate in CompPoly), U32 and U64 arithmetic, and a Fibonacci VM ensemble demonstrating the multi-table Channel primitive announced at ZKProof 8 in June 2026. Succinct's sp1-lean expresses SP1 Hypercube's RISC-V chip constraints in Clean and proves them against the Sail RISC-V model. The roadmap lists a Plonky3 backend with Rust code generation, LLZK integration for a Circom frontend, Stwo and Binius backends and custom-gate PLONK.

Where it is strong

Only circuit framework on this index whose default deliverable is both soundness and completeness for every gadget.
Compositional: verified gadgets are reused as subcircuits without re-proving, so large circuits and multi-table zkVMs are tractable.
Active ecosystem: sp1-lean, zk.golf, published verified hash gadgets, and a documented agent workflow for LLM-assisted proving.

Limits and caveats

Circuits are written in Clean; verifying an existing Circom or Halo2 codebase means porting, modelling or waiting for the LLZK frontend.
Backend code generation (Plonky3 Rust) is on the roadmap; until it ships, the correspondence between the Lean circuit and the deployed constraints is a review item.
Proof engineering in Lean 4 has a learning curve; zkSecurity's own comparison rates the Lean frameworks as the most sophisticated but heaviest on tactics.

When to choose it

Choose Clean when you are writing new circuits or a zkVM instruction set and want a verified artifact you can keep extending, when completeness matters (a wallet or bridge that must never reject a valid proof), or when you plan to let AI agents optimise circuits under a fixed specification. The maintainer, zkSecurity, takes verification engagements built on it.

Who works with Clean

zkSecurity.

Top-listed for circuit verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website

sp1-lean, zkLean, Halva, Picus, LLZK, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).

Sources

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt