本文介绍了clean,一个为零知识电路(ZK circuits)构建的嵌入式DSL和形式验证框架,目标是使用Lean4定义电路、指定属性并进行形式化验证。clean通过将电路定义、规范和正确性证明置于一处,旨在创建一个可重用的、经过形式验证的电路组件库,并以AIR算法为目标,最终发展成通用的零知识证明框架。文章还提供了一个8位加法的具体例子,展示了如何使用clean来定义、验证电路的正确性