算术电路形式化验证框架比较

序言：Proof Market

2014 年，我运营着一个名为 Proof Market 的网站。在那里，你可以用 Bitcoin 为待证明的数学命题设置赏金；当你在 Rocq 中完成证明后，就可以领取这些 Bitcoin。我想构建一个非托管版本的 Proof Market。为此，zkVM 会非常有用。我更希望用于证明检查的 zkVM 是经过形式化验证的。我正在验证 arithmetic circuits，因为我想建立一个面向定理证明者和定理证明 AI 的市场，这样我就可以轻松地把 arithmetic circuits 的验证外包出去！

什么

当你把一个问题（Proof Market 中要证明的内容，或者更一般地说某个需要通过的验证）编码成一个求解 polynomial equations 的 puzzle 时，密码学家会提供一些简洁的方法来证明这个 puzzle 有解（succinct arguments）。

在一些密码学假设下，succinct argument 的接收者将能够以非常高的概率检查出这个 polynomial puzzle 确实有解。然后，接收者还会希望确保 polynomial puzzle 的解对应于原始问题的解（soundness）。此外，对于 succinct argument 的发送者来说，原始问题的任何解都能被编码成 polynomial puzzle 的解，这一点通常也非常关键（completeness）。

当人们编写 polynomial puzzles（arithmetic circuits）时，他们脑中通常已经有了 soundness 和 completeness 的数学证明。数学证明可以通过白板和讨论来传递，但（i）发送和接收这些数学思想的双方都要付出很多努力，而且（ii）在检查 40 个 case 中的前 5 个之后，每个人都会感到厌倦。他们会逐渐习惯某些重复模式并失去注意力（不过我有一个假设：也许可以通过展示涉及 40 个 case 的证明，来区分理论计算机科学家和数学家）。有时，人们会在第 6 个（共 40 个）case 中漏掉一个轻微错误，而这很重要，因为攻击者可以研究那个 case 来寻找实现中的漏洞。

有一些计算机语言可以用来编写和检查数学证明，它们也可以用于推理硬件和软件系统。对于 arithmetic circuits，软件是用 polynomial 来写的，所以我们又回到了数学。人们已经使用这些工具来检查 arithmetic circuits 的 soundness 和 completeness。下面我来比较一下这些工具。

注意

对于密码学家：在这篇博客里，我忽略了 argument of knowledge。下面提到的项目似乎都没有明确说明 prover 对解具有 polynomial-time access。这里讨论的都是解的存在性。

免责声明：我有偏见

我正在开发 Clean，这是一个以某种模块化方式证明 arithmetic circuits 正确性的框架。Clean 用 Lean Language 编写（属于 Lean FRO 的 TM）。

我在工作中用了多年 Rocq。在早期的 smart contracts 形式化验证 中，我使用了 Isabelle。我也时不时在小项目中使用 ACL2。我和这些工具的开发者聊过，但我不属于任何工具开发的核心圈子。

模板

• 现有示例（在线可用的）有多先进？
  • Level 1：涉及最多十几个 finite field 元素的简单示例
  • Level 2：像 hash functions 或 risc vm instructions 这样的实用组件
  • Level 3：像对 risc vm executions 的刻画这样的端到端结果
• 我能复现结果吗？需要多长时间？
  • 不赶时间，保持我平常悠闲的生活节奏。
  • 在 2025 年配备 16 GB 内存的 Macbook Air M4 上
• Claude Code 能验证 IsZero circuit 吗？
• Claude Code 能验证 weighted-sum circuit 吗？
  • 我先从这句话开始：“让我们试试另一个 gadget。它包含 65 个 field elements。前 32 个和后 32 个要做 inner-product，并且结果应与最后第 65 个元素匹配。”

总结比较

下面是结果总结。注意，Level 0 示例只涉及公开可用的示例。这些项目有不同的目标。其中两个，acl2-jolt 和 sp1-lean，着眼于现有 zkVM 实现中棘手的方面。其他项目则旨在成为通用框架。有些尝试从其他语言导入 circuits 并进行验证，有些则旨在成为前端。所有这些项目都包含可复用的组件。

由 ChatGPT 生成的图像

ACL2 (r1cs)，就像 ACL2 book 里那样

人们使用 ACL2 来验证 arithmetic circuits。一个例子是 ACL2 book 中的一个 页面。这个框架位于 ACL2 book 中，一些应用似乎是专有的。

R1CS 是一种流行的 polynomial equations 格式。看起来 ACL2 (r1cs) 库也能处理其他类型的 polynomial equations。

• 现有在线示例有多先进？
  • Level 2？我很难找到这些示例的列表。我可能错过了最有趣的项目。
  • 一篇 论文 中提到了 BLAKE2，但我没能在网上找到源代码。
  • MIMC hash 的规范可以在网上找到。关于某些组件的证明 也可以在线查看。
• 我能复现结果吗？需要多长时间？
  • 是的，三个小时。
  • 根据我之前的经验，我知道在较新的 Mac 上最好的方法是遵循 这个指南，并使用 sbcl。我只是为了安装 sbcl 执行了 brew install sbcl。
  • 然后，我本该运行 cd books; make ACL2=/<snip>/acl2-sources/saved_acl2 -j 8 kestrel/ethereum/semaphore/top.cert。
  • 但我因为等待 make ACL2=/<snip>/acl2-sources/saved_acl2 -j 8 kestrel/ethereum 一段时间而浪费了一些时间。
• Claude Code 能验证 IsZero circuit 吗？
  • 是的，但我认为它在某种程度上参考了一个已有的类似 gadget。
  • Claude Code 问我：“R1CS 还是 PFCS？”这很聪明，因为 ACL2 Book 至少包含两种表述 polynomial circuit verification 问题的方法。PFCS 代表 prime field constraint systems。
• Claude Code 能验证 weighted-sum circuit 吗？
  • 是的。
  • 它几乎要放弃证明了，所以我给了类似这样的建议：“也许可以有一个 hint，引导 proof engine 使用已证明的 sublemmas，而不是展开定义。”
  • Claude Code 很有帮助，因为我不记得 ACL2 的精确 hint 语法。整个过程花了 30 分钟。

我喜欢 ACL2 (r1cs)，就像 ACL2 book 里那样

arithmetic circuits 的形式化很直接，也很容易跟上。这里有一组方程，左边和右边都写得很清楚。

(define make-rel-iszero ()
  :returns (def definitionp)
  (make-definition
   :name 'rel-iszero
   :para '(x out)
   :body (list
          ;; 约束 1: x * x_inv = 1 - out
          (make-constraint-equal
           :left (expression-mul
                  (expression-var 'x)
                  (expression-var 'x-inv))
           :right (expression-sub (expression-const 1)
                                  (expression-var 'out)))
          ;; 约束 2: out * x = 0
          (make-constraint-equal
           :left (expression-mul
                  (expression-var 'out)
                  (expression-var 'x))
           :right (expression-const 0)))))

ACL2 在正常用法下不要求编写 tactics。你可以给 prover 提示，而这基本上只是点出相关 lemma 的名字。这对人类和 LLM 可能都更容易。

我对 ACL2 (r1cs)，就像 ACL2 book 里那样，剩下的愿望

安装 ACL2 花了一些反复试错的时间，尽管这已经是我第三次这么做了。我试着使用安装指南里提到的特定 gcl 版本，但 ./configure 脚本无法工作，等等。一些在线文档页面返回了 403 错误。和 Lean 的安装相比，这确实是个障碍（安装一个 VSCode 插件并点击几次“ok”就行）。

我 vs Claude Code

Claude Code 在处理 ACL2 (r1cs)（就像 ACL2 book 里那样）方面比我更强。我相信，陈述并证明正确性定理的速度比我自己做快了 100 倍。

ACL2 (PFCS)，就像 ACL2 book 里那样

• 现有在线示例有多先进？
  • Level 1：几个 field elements（rel-select）
  • 研究论文表明，PFCS 方法被用于验证 snarkVM 的许多 gadget。然而，我没能在网上找到这些更高级的示例。
• 我能复现结果吗？需要多长时间？
  • 完成上面的 ACL2 (r1cs) 过程后，没有再花额外时间。
• Claude Code 能验证 IsZero circuit 吗？
  • 可以，一次成功。
• Claude Code 能验证 weighted-sum circuit 吗？
  • 可以，但非常啰嗦。
  • 我不得不提醒它一次“不要放弃”。

我喜欢 ACL2 (PFCS)，就像 ACL2 book 里那样

PFCS 是一种包装 arithmetic circuits 的合理方式。

我对 ACL2 (PFCS)，就像 ACL2 book 里那样，剩下的愿望

这个框架值得更多关注。它受限于缺少公开可用的高级示例。

有一些数据类型可以编码为 field elements 的向量，而允许这些作为参数可能会是一个有趣的方向。

我 vs Claude Code

至于我和 Claude Code 谁更擅长处理 ACL2 (PFCS)，目前还不清楚。Claude Code 快要放弃时，我坚持继续，因此我对整体把握得更好。

ACL2，就像 acl2-jolt 里那样

另一个使用 ACL2 的项目是 GitHub 上可用的 acl2-jolt。

• 现有示例有多先进？
  • Level 2
• 我能复现结果吗？需要多长时间？
  • 在 Mac 上不行。
  • 在 Ubuntu 24.04.3 LTS 上可以在一定程度上复现。
    • 在作者的一些建议之后，我可以认证 ACL 文件（PR）。
    • 我无法检查它与 Jolt 的 Rust 实现之间的对应关系（因为一个依赖没有固定版本，并且要求使用更新版本的 Rust）。
• Claude Code 能验证 IsZero circuit 吗？
  • 不太适用。
  • 反映了 Jolt 的 lookup-singularity 方法，这种验证方式也侧重于验证 subtables，并把 subtables 组合成 instructions。

我喜欢 ACL2，就像 acl2-jolt 里那样

这个项目验证的是一个真实实现。代码库的一部分文档很好。代码库非常统一，并且已证明的命题很短，也很容易读。

我对 ACL2，就像 acl2-jolt 里那样，剩下的愿望

验证止步于每条 instruction。程序执行的概念还没有形式化。大多数用户关心的是程序执行，所以 circuits 能表示程序执行这一点很重要。

代码库中有一些令人困惑的地方。有些 subtables 用 (create-tuple-indices (expt 2 8) (expt 2 8)) 构造成 257x257 维度。其他 subtables 则用 (create-tuple-indices (1- (expt 2 8)) (1- (expt 2 8))) 构造成 256x256 维度。我基本确定这不重要，但某些类似的问题可能会很重要。

我 vs Claude Code

Claude Code 在处理 acl2-jolt 方面比我更强。我当时在把 257x257 table 替换成 256x256 table，而 Claude Code 在我还没理解为什么证明会出问题之前，就已经在修复它们了。

Garden

Garden 是一个用 Rocq 编写、用于验证 arithmetic circuits 的框架。

• 现有示例（在线可用的）有多先进？
  • Level 2，有多个。
  • Garden 可以从多种语言导入 circuits。
• 我能复现结果吗？需要多长时间？
  • 可以，20 分钟。包括提交一个关于构建说明的小 PR。
• Claude Code 能验证 IsZero circuit 吗？
  • 最终可以。
  • Claude Code 对如何分解 A /\ B /\ C 感到困惑，还抱怨说：“This is incredibly frustrating.” 我很遗憾听到这个。
  • 主要困难来自当前对乘法逆元的 公理化处理。
    • Claude Code 为 UnOp.inv 添加了一些公理（因为 inverse operation 没有定义，而只是被假定存在，见 M.v）。
    • 但它忘了添加一个公理，说明 UnOp.inv _ 小于 p。
    • Claude Code 花了很多时间来回整理 mod，比如在 H_out: (1 mod p - ((x * (self.inv mod p)) mod p) mod p) mod p = 0 这样的式子里。
  • 我遇到一种情况：coqide 可以工作，但 VsRocq 不行，因为它不知为何没有按照唯一的 _CoqProject 找到 Require Imports。这限制了 Claude Code 的 IDE 访问选项。
• Claude Code 能验证 weighted-sum circuit 吗？
  • 可以。需要一些干预，因为 Claude Code 告诉 Rocq 接受了一些不必要且没有证明的命题。

我喜欢 Garden

它可以验证用流行 DSL 编写的 circuits。

我对 Garden 剩下的愿望

只有可解决的问题：

• 有时 field operations 被定义为整数模 p，这很容易让人分心。
• 目前 syntax 看起来相当嘈杂（但对于自动翻译的目标来说，这也许是合理的选择）。

IsZero circuit 看起来像这样

Definition constrain {p} `{Prime p} (arg_fun_0 : IsZero.t) (arg_fun_1 : Felt.t) : M.t unit :=
  let var_out : Felt.t := arg_fun_0.(IsZero.out) in
  let var_inv : Felt.t := arg_fun_0.(IsZero.inv) in
  let var_felt_const_1 : Felt.t := UnOp.from 1 in
  let var_felt_const_0 : Felt.t := UnOp.from 0 in
  (* 约束 1: out = 1 - x * inv *)
  let var_prod : Felt.t := BinOp.mul arg_fun_1 var_inv in
  let var_out_expr : Felt.t := BinOp.sub var_felt_const_1 var_prod in
  let* _ : unit := M.AssertEqual var_out var_out_expr in
  (* 约束 2: x * out = 0 *)
  let var_prod2 : Felt.t := BinOp.mul arg_fun_1 var_out in
  let* _ : unit := M.AssertEqual var_prod2 var_felt_const_0 in
  M.Pure tt.

我 vs Claude Code

在处理 Garden 代码方面，我比 Claude Code 更强。

zk-lean

zk-lean 是一个用 Lean 编写、用于验证 arithmetic circuits 的框架。

• 现有示例（在线可用的）有多先进？
  • Level 1，只是比较两个 field elements。
  • 不过，这个框架本身看起来功能更丰富。
• 我能复现结果吗？需要多长时间？
  • 可以，不到十分钟。
• Claude Code 能验证 IsZero circuit 吗？
  • 不行，它无法弄清楚如何处理 free monad 的 binds。我自己也不行。我们都没能弄明白如何使用这些机制。

我喜欢 zk-lean

现在还太早，难以下定论。这个代码库由一些非常基础的示例和一些复杂的机制组合而成。在看到那些复杂机制真正发挥作用之前，我还不能说太多。

我对 zk-lean 剩下的愿望

我猜会有更多有趣的示例出现。Jolt repository 有一个 为 zk-lean 导出某些 Lean 定义的功能，所以在这之上可能会有一些工作。

我 vs Claude Code

至于我和 Claude Code 在处理 zk-lean 代码上的比较，算是平局。两者都没能理解如何对 syntax 进行推理。我放弃的时点是当我看到 FreeM.bind 的定义是 protected。我猜我不应该展开这个定义（unfolding 是用定义替换 FreeM.bind 的动作），但那还能做什么呢？

sp1-lean

Succinct 宣布了 Sp1 Hypercube 的形式化验证。这是一个值得注意的成就。

• 现有示例（在线可用的）有多先进？
  • Level 2：risc vm instructions
• 我能复现结果吗？需要多长时间？
  • 部分可以。我还没有把 Rust constraints 转换成 Lean 代码。关于 LB instruction 的某些证明似乎在公告当天的那个 commit 里 缺失了。文件 LoadByteChip.lean 是在公告当天的 那个 commit 中添加的。它还没有进入默认构建 lake build。
  • 用 lake build 构建 Lean 代码在不到两个小时内成功了（基于一个与 公告 同一天做出的 commit）。
  • 公告没有提到 git commit，所以我是猜的。
• Claude Code 能验证 IsZero circuit 吗？
  • 不适用。一个实验是把 iszero instruction 加到 Sail specification 里并实现、验证它，但那样就不算公平比较了。

我喜欢 sp1-lean

公告 对团队做了什么、没做什么，讲得非常透明。我尤其欣赏 “Assumptions and Caveats” 部分。这样的透明度是一个值得效仿的例子。

这项工作旨在验证所有相关 instructions。

如果你熟悉 RISC-V zkVMs（把 VM executions 编码到 arithmetic circuits 中的方式），那么这些定义和命题都很容易理解。

我感觉这里运用了相当多的 theorem-proving kung-fu，并且是以非常有针对性的方式完成工作的。这个 repo 包含一些很酷的 Lean 技巧（使用高级 attributes 和巧妙调整的 automatic tactics 调用），使 proof scripts 的体量降到了比如说不到我预期朴素方法的 1/5。

我对 sp1-lean 剩下的愿望

公告 没有说明证明工件对应的 git commit。公告时刻最新的 commit 并不包含 LB 正确性的完整证明。更早的一个 commit 包含一个关于 LB instruction 的定理。

Completeness 缺失。例如 correct_add 说的是“如果约束成立，那么某些某些东西”。我找不到另一个定理说“如果某些某些东西，那么约束可以被满足”。

关于定义有一些棘手之处。缓解办法将涉及 constraint development framework 的一些设计变更：

• AddChip 的输入是 Main[6] 和 Main[14]，输出是 Main[21]。
• Sp1 特定约定（ByteOperation 相关 tables 的构造方式）和通用 Air constraint 约定混在一起了。
• 发送和接收 multiplicities 被神奇地处理了，因此 multiplicity overflow 不会被注意到。
• MemoryAccessInShardTimestamp 只包含 low limbs；为什么这是安全的、对哪些用途安全，等等，都不是 repo 里验证的一部分。
• 我觉得我还没有注意到所有问题。

这些证明看起来对 constraints 数量等变化很脆弱。也许 coding agents 能够更新这类东西。

Clean

Clean 是一个用 Lean 编写、以模块化方式证明 arithmetic circuits 正确性的框架。

• 现有示例（在线可用的）有多先进？
  • Level 2：Keccak 和 BLAKE3 hash functions，另外还有一个带 soundness 的小 VM
• 我能复现结果吗？需要多长时间？
  • 不适用，因为我正在这个项目上工作。请 尝试 并告诉我们你的看法。
• Claude Code 能验证 IsZero circuit 吗？
  • IsZero 已经存在，所以不适用。
• Claude Code 能验证 weighted-sum circuit 吗？
  • 不行，它开始做别的事情了。
  • Claude Code 忘了为 inner product 约束一个变量。
  • Claude Code 试图证明 soundness，但没成功，于是它添加了一个假设，声称结果就是预期值，而不是修复 circuit。
  • 我能够完成 soundness 证明。

我喜欢 Clean

整个开发都在 Lean 中完成，所以没有任何东西会在翻译中丢失。

Clean 提供了以可组合方式验证 sub-circuits 的方法。

把一切都看作无限 field variables 纸带上的一个谓词，这在概念上有某种简洁性。

在我看来，这个 circuit syntax 作为前端语言是可以接受的。下面是 Clean 项目中的一个 IsZeroField.lean（在这次实验之前写的）：

def main (x : Var field F) : Circuit F (Var field F) := do
  -- 当 x ≠ 0 时，我们需要 x_inv，使得 x * x_inv = 1
  -- 当 x = 0 时，x_inv 可以是任何值（我们使用 0）
  let xInv ← witness fun env =>
    if x.eval env = 0 then 0 else (x.eval env : F)⁻¹

  let isZero <== 1 - x*xInv -- 如果 x 为零，isZero 就是一
  isZero * x === 0  -- 如果 x 不是零，isZero 就是零

  return isZero

我对 Clean 剩下的愿望

记住不同种类的 circuits 很麻烦：Circuit、ElaboratedCircuit、Subcircuit、FormalCircuit、FormalAssertion 和 FormalGeneralCircuit。

当我使用一个 sub-circuit 时，在 goal state 中看到的是 (something_complicated).output，而不是表示 sub-circuit 输出的单独变量。通常这并不重要，因为我有 subcircuits 的 specification，它们会告诉我关于 (something_complicated).output 的信息。既然我从不需要查看那个复杂项的结构，我本可以直接看到一个变量，而不是这样。

我 vs Claude Code

在使用 Clean 方面，我比 Claude Code 更强。

一些沉寂的项目

Coda 和 risc0-lean4 有一些关于 arithmetic circuits 的 Lean 代码。最后更新都是几年前了，所以我没有把这些项目纳入比较。

未来

这个领域接下来会发生什么？短期内，会出现更多框架。会有人提出 polynomial circuits 类似于 effectful lenses / relation-oriented programming / representation theory 的想法。中期来看，除了手工优化的 circuits 之外，人们将不再自己编写 circuits。大多数 polynomial circuits 都会被自动生成。某些形式化验证技术将越来越少地需要人工干预。评估验证工作成果仍然会是一个挑战。

zkSecurity 提供加密系统的审计、研究和开发服务，包括 zero-knowledge proofs、MPCs、FHE 和 consensus protocols。

了解更多 →

• 原文链接： blog.zksecurity.xyz/post...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～