Clean (zkSecurity): Lean 4 formal verification framework for ZK circuits, sound and complete
================================================================================

Clean 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
Category: ZK circuit verification
Targets: AIR, PLONK, R1CS, zkVM chips, Plonky3-style tables
Approach: Embedded Lean 4 DSL; proof assistant; soundness and completeness theorems per gadget, composed without re-proving
Access: Open source (MIT)
Status: Active, funded by an Ethereum Foundation Verified zkEVM grant
Strengths: 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: 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.
Firms using it: zkSecurity
Sources: https://clean.zksecurity.xyz | https://blog.zksecurity.xyz/posts/clean/ | https://blog.zksecurity.xyz/posts/clean-verified-zkvms/ | https://blog.zksecurity.xyz/posts/poseidon-clean/ | https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/

Source page: https://sorryfree.com/frameworks/clean/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13