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

序言：证明市场

2014 年，我运营着一个名为 Proof Market 的网站，你可以在上面悬赏比特币来证明数学命题，当你在 Rocq 中证明了这些命题，就可以获得比特币。我想构建一个非托管版本的 Proof Market。为此，zkVM 非常有用。我更希望证明检查 zkVM 能够被形式化验证。我正在验证算术电路，因为我想要一个定理证明人员和定理证明 AI 的市场，这样我就可以轻松地卸载算术电路的验证工作！

是什么

当你将一个问题（Proof Market 中需要证明的东西，或者通常情况下需要通过的一些验证）编码为一个求解多项式方程的难题时，密码学家会给你一些简洁的方式来证明这个难题有解（简洁论证）。

简洁论证的接收者将能够检查，在给定一些密码学假设的情况下，以非常高的概率，多项式难题存在一个解。然后接收者也会想确保多项式难题的解对应于原始问题的解（可靠性）。此外，对于简洁论证的发送者来说，原始问题的任何解都可以编码为多项式难题的解（完整性）通常至关重要。

当人们编写多项式难题（算术电路）时，他们通常在脑海中对可靠性和完整性有数学证明。数学证明可以通过白板和讨论来传递，但是（i）这需要发送者和接收者双方付出大量的努力，以及（ii）每个人在检查 40 个案例中的 5 个后都会感到厌烦。他们会习惯一些重复的模式并失去注意力（尽管我有一个假设，即可以通过向理论计算机科学家展示涉及 40 个案例的证明来区分他们和数学家）。有时人们会错过 40 个案例中的第 6 个案例中的一个小错误，这很重要，因为攻击者可以研究该案例以找到实现中的漏洞。

有一些计算机语言可以用来编写和检查数学证明，它们也可以用来推断硬件和软件系统。对于算术电路，软件是用多项式编写的，所以我们又回到了数学。人们已经使用这些语言来检查算术电路的可靠性和完整性。让我比较一下这些语言。

注意

对于密码学家：我在这篇博文中忽略了知识论证。下面提到的任何项目似乎都没有说明证明者可以以多项式时间访问解决方案。这完全是关于解决方案的存在性。

免责声明：我带有偏见

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

我在工作中使用了 Rocq 多年。对于早期时代的 智能合约形式化验证，我使用了 Isabelle。我不时地使用 ACL2 做一些小项目。我曾经与开发这些工具的人交谈过，但我不属于任何工具开发的内部圈子。

模板

• 现有的例子（在线提供）有多先进？
  • 级别 1：涉及最多十几个 有限域 元素的简单例子
  • 级别 2：有用的组件，如哈希函数或 risc vm 指令
  • 级别 3：端到端的结果，如 risc vm 执行的特征
• 我可以重现结果吗？需要多长时间？
  • 不匆忙，保持我平常悠闲的生活。
  • 在配备 16 GB 内存的 Macbook Air M4 上，2025 年款
• Claude Code 可以验证 IsZero 电路吗？
• Claude Code 可以验证加权和电路吗？
  • 我从这里开始："让我们尝试另一个小工具。它需要 65 个域元素。前 32 个和后 32 个应该取内积，并且它应该与最后一个 65th 元素匹配。"

总结比较

这是结果的总结。请注意，级别 0 的示例仅关于公开可用的示例。这些项目有不同的目标。其中两个，acl2-jolt 和 sp1-lean，旨在解决现有 zkVM 实现的棘手方面。其他项目旨在成为通用框架。有些尝试从其他语言导入电路并验证它们。有些旨在成为前端。所有项目都包含可以重用的组件。

由 ChatGPT 生成的图像

ACL2 (r1cs)，如 ACL2 书籍

人们使用 ACL2 来验证算术电路。一个例子是 ACL2 书籍中的 页面。该框架位于 ACL2 书籍 中，一些应用似乎是专有的。

R1CS 是一种流行的多项式方程格式。ACL2 (r1cs) 库似乎也可以处理其他类型的多项式方程。

• 现有的例子（在线提供）有多先进？
  • 级别 2？我很难找到示例列表。我可能错过了最有趣的项目。
  • 一篇论文 提到了 BLAKE2，但我无法在线找到源代码。
  • MIMC 哈希 规范在线可用。关于某些组件的证明 也在网上。
• 我可以重现结果吗？需要多长时间？
  • 是的，三个小时。
  • 根据我之前的经验，我知道在最新的 Mac 上最好的方法是遵循 本指南，并使用 sbcl。我只是做了 brew install sbcl 来安装 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 电路吗？
  • 是的，但我认为它在某种程度上遵循了现有的类似小工具。
  • Claude Code 问我 "R1CS or PFCS"。这很聪明，因为 ACL2 书籍至少包含两种制定多项式电路验证问题的方法。PFCS 代表 素域约束系统。
• Claude Code 可以验证加权和电路吗？
  • 是的。
  • 它即将放弃证明，所以我提出了建议，比如 "也许可以有一个提示来引导证明引擎使用已证明的子引理，而不是展开定义"。
  • Claude Code 很有帮助，因为我不记得 ACL2 的确切提示语法。整个过程花了 30 分钟。

我喜欢 ACL2 (r1cs)（如 ACL2 书籍）的地方

算术电路的形式化是直接且易于理解的。有一个方程列表，其中明确写出了左侧和右侧。

(define make-rel-iszero ()
  :returns (def definitionp)
  (make-definition
   :name 'rel-iszero
   :para '(x out)
   :body (list
          ;; Constraint 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)))
          ;; Constraint 2: out * x = 0
          (make-constraint-equal
           :left (expression-mul
                  (expression-var 'out)
                  (expression-var 'x))
           :right (expression-const 0)))))

ACL2 不需要以通常的方式编写策略。你可以给证明器提示，而这只是关于命名相关的引理。这可能对人类以及 LLM 更容易。

我对 ACL2 (r1cs)（如 ACL2 书籍）的剩余期望

ACL2 的安装需要一些反复试验，尽管这已经是我的第三次了。我试图使用安装指南中提到的特定 gcl 版本，但 ./configure 脚本不起作用等等。一些在线文档页面返回 403 错误。与 Lean 安装（安装 VSCode 插件并按 "ok" 几次）相比，这是一个真正的障碍。

我 vs Claude Code

在处理 ACL2 (r1cs)（如 ACL2 书籍）方面，Claude Code 比我更厉害。我相信使用 Claude Code 声明和证明正确性定理的速度比我单独完成快 100 倍。

ACL2 (PFCS)，如 ACL2 书籍

• 现有的例子（在线提供）有多先进？
  • 级别 1：几个域元素 (rel-select)
  • 研究论文表明 PFCS 方法被用于验证 snarkVM 的许多小工具。但是，我无法在线找到这些高级示例。
• 我可以重现结果吗？需要多长时间？
  • 在完成上面的 ACL2 (r1cs) 过程后，没有花费时间。
• Claude Code 可以验证 IsZero 电路吗？
  • 是的。一次性完成。
• Claude Code 可以验证加权和电路吗？
  • 是的，但是非常冗长。
  • 我不得不告诉它 "不要放弃" 一次。

我喜欢 ACL2 (PFCS)（如 ACL2 书籍）的地方

PFCS 是一种合理地打包算术电路的方法。

我对 ACL2 (PFCS)（如 ACL2 书籍）的剩余期望

该框架值得更多关注。它缺乏公开可用的高级示例。

有些数据类型可以编码为域元素的向量，允许将这些作为参数可能是一个有趣的方向。

我 vs Claude Code

不清楚是我更好还是 Claude Code 更擅长处理 ACL2 (PFCS)。当 Claude Code 即将放弃时，我更好地把握了情况，但我坚持继续。

ACL2，如 acl2-jolt

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

• 现有的例子有多先进？
  • 级别 2
• 我可以重现结果吗？需要多长时间？
  • 在 Mac 上不行。
  • 是的，在 Ubuntu 24.04.3 LTS 上在一定程度上可以
  • 在作者的一些建议后，我可以验证 ACL 文件 (PR)。
  • 我无法检查与 Jolt 的 Rust 实现的对应关系（因为一个依赖项没有被固定，并且需要 Rust 的较新版本）
• Claude Code 可以验证 IsZero 电路吗？
  • 并不真正适用。
  • 反映了 Jolt 的 lookup-singularity 方法，这种验证方法也专注于验证子表并将子表组合成指令。

我喜欢 ACL2（如 acl2-jolt）的地方

该项目正在验证一个真实的实现。部分代码库有很好的文档记录。代码库非常统一，并且已证明的语句简短易懂。

我对 ACL2（如 acl2-jolt）的剩余期望

验证在每个指令处停止。程序执行的概念尚未形式化。大多数用户关心程序的执行，因此电路表示程序执行非常重要。

代码库中存在一些令人困惑的方面。一些子表由 257x257 维度制成，带有 (create-tuple-indices (expt 2 8) (expt 2 8))。其他子表由 256x256 维度制成，带有 (create-tuple-indices (1- (expt 2 8)) (1- (expt 2 8)))。我几乎可以肯定这无关紧要，但类似的事情可能很重要。

我 vs Claude Code

Claude Code 在处理 acl2-jolt 方面比我更厉害。我正在用 256x256 表替换 257x257 表，并且 Claude Code 在我理解为什么它们被破坏之前就修复了证明。

Garden

Garden 是一个用于验证用 Rocq 编写的算术电路的框架。

• 现有的例子（在线提供）有多先进？
  • 级别 2，多个计数。
  • Garden 可以从多种语言导入电路。
• 我可以重现结果吗？需要多长时间？
  • 是的，20 分钟。包括提交了关于构建说明的 一个很小的 PR。
• Claude Code 可以验证 IsZero 电路吗？
  • 最终可以。
  • Claude Code 搞不清楚如何分解 A /\ B /\ C，并且它抱怨说 "这令人难以置信地沮丧。" 我很遗憾听到这个。
  • 大部分困难来自当前 对乘法逆元的公理化处理。
  • Claude Code 添加了一些关于 UnOp.inv 的公理（因为逆运算没有定义，只是假设存在，参见 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 Import。这限制了 Claude Code 的 IDE 访问选项。
• Claude Code 可以验证加权和电路吗？
  • 是的。需要一些干预，因为 Claude Code 告诉 Rocq 接受一些不必要的语句，没有证明。

我喜欢 Garden 的地方

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

我对 Garden 的剩余期望

仅可解决的问题：

• 有时场运算被定义为整数模 p，而且非常容易分心。
• 目前语法对于眼睛来说相当嘈杂（但这对于自动翻译的目标来说可能是一个合理的选择）。

IsZero 电路看起来像这样

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
  (* Constraint 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
  (* Constraint 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

我比 Claude Code 更擅长处理 Garden 代码。

zk-lean

zk-lean 是一个用于验证用 Lean 编写的算术电路的框架。

• 现有的例子（在线提供）有多先进？
  • 级别 1，只是比较两个场元素
  • 然而，框架本身似乎更具功能性。
• 我可以重现结果吗？需要多长时间？
  • 是的，不到十分钟。
• Claude Code 可以验证 IsZero 电路吗？
  • 不，它无法弄清楚如何处理 free monad 的绑定。我也无法。我们无法弄清楚如何使用该机制。

我喜欢 zk-lean 的地方

现在说还为时过早。代码库结合了一些非常基本的例子和一些复杂的机制。我需要看到复杂的机制在工作才能说些什么。

我对 zk-lean 的剩余期望

我想会提供更多有趣的例子。Jolt 仓库有 一个导出一些 Lean 定义的功能 用于 zk-lean，因此可能会有一些基于此的努力。

我 vs Claude Code

对于我和 Claude Code，关于处理 zk-lean 代码，打成平手。两者都未能理解如何推断语法。我放弃的点是当我看到 FreeM.bind 的定义是 protected 时。我猜我不应该展开定义（展开是用它的定义替换 FreeM.bind 的行为），但除此之外呢？

sp1-lean

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

• 现有的例子（在线提供）有多先进？
  • 级别 2：risc vm 指令
• 我可以重现结果吗？需要多长时间？
  • 部分可以。我还没有将 Rust 约束转换为 Lean 代码。关于 LB 指令的一些证明似乎在发布当天的提交中 丢失了。文件 LoadByteChip.lean 在发布当天的 提交 中添加。它尚未在默认构建 lake build 中。
  • Lean 代码的构建在不到两小时内用 lake build 成功完成（在与 公告 同一天作出的 提交 上）。
  • 公告没有提到 git 提交，所以我猜了这个提交。
• Claude Code 可以验证 IsZero 电路吗？
  • 不适用。一个实验是在 Sail 规范中添加一个 iszero 指令并实现它并验证它，但这将不是一个公平的比较。

我喜欢 sp1-lean 的地方

公告 非常透明地说明了团队做了什么以及他们没有做什么。我特别欣赏 "假设和注意事项" 部分。透明度水平是一个值得效仿的例子。

该努力旨在验证所有相关的指令。

如果你熟悉 RISC-V zkVM（将 VM 执行编码为算术电路的方式），那么定义和语句很容易理解。

我感到相当多的定理证明功夫被有针对性地应用来完成这项工作。该 repo 包含很酷的 Lean 技术（使用高级属性和巧妙调整的自动策略调用），使证明脚本的大小保持在，比如，我所期望的朴素方法的 1/5 以下。

我对 sp1-lean 的剩余期望

公告 没有指定证明工件的 git 提交。公告时最新的提交 不包含 LB 正确性的完整证明。先前的提交 包含关于 LB 指令的定理。

缺少完整性。例如，correct_add 说 "如果约束成立，则会发生一些事情"。我找不到另一个定理说 "如果发生了某些事情，则可以满足约束"。

关于定义，有一些棘手的地方。缓解措施将涉及约束开发框架中的一些设计变更：

• Main[6] 和 Main[14] 是 AddChip 的输入，Main[21] 是输出。
• Sp1 特定约定（如何制作 ByteOperation 相关表）和通用 Air 约束约定的结果是混合的。
• 多重性的发送和接收被神奇地处理，因此不会注意到多重性溢出。
• MemoryAccessInShardTimestamp 仅包含低位，这对于什么目的来说是安全的，等等，这些都不是 repo 中验证的一部分。
• 我认为我没有注意到所有的事情。

这些证明看起来很容易受到约束数量等变化的影响。也许编码代理能够更新这类事情。

Clean

Clean 是一个以模块化方式证明算术电路正确性的框架，用 Lean 编写。

• 现有的例子（在线提供）有多先进？
  • 级别 2：Keccak 和 BLAKE3 哈希函数，还有一个带有可靠性的小型 VM
• 我可以重现结果吗？需要多长时间？
  • 不适用，因为我正在开发这个项目。请 尝试 并告诉我们你的想法。
• Claude Code 可以验证 IsZero 电路吗？
  • IsZero 已经存在，因此不适用。
• Claude Code 可以验证加权和电路吗？
  • 不，它开始做其他事情。
  • Claude Code 忘记约束内积的变量。
  • Claude Code 试图证明可靠性，但不能，所以它添加了一个假设，说结果是预期的值，而不是修复电路。
  • 我能够完成可靠性证明。

我喜欢 Clean 的地方

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

Clean 提供了以可组合的方式验证子电路的方法。

将所有内容视为场变量无限磁带上的谓词，这在概念上很简单。

电路语法可以作为前端语言传递（在我看来）。这是 Clean 项目中的一个 IsZeroField.lean（在这个实验之前编写）：

def main (x : Var field F) : Circuit F (Var field F) := do
  -- When x ≠ 0, we need x_inv such that x * x_inv = 1
  -- When x = 0, x_inv can be anything (we use 0)
  let xInv ← witness fun env =>
    if x.eval env = 0 then 0 else (x.eval env : F)⁻¹

  let isZero <== 1 - x*xInv -- If x is zero, isZero is one
  isZero * x === 0  -- If x is not zero, isZero is zero

  return isZero

我对 Clean 的剩余期望

必须记住不同类型的电路：Circuit、ElaboratedCircuit、Subcircuit、FormalCircuit、FormalAssertion 和 FormalGeneralCircuit，这很麻烦。

当我使用子电路时，我在目标状态中看到 (something_complicated).output，而不是子电路输出的单个变量。这通常无关紧要，因为我有子电路的规范告诉我关于 (something_complicated).output 的信息。既然我永远不需要查看复杂术语的结构，我可以只看到一个变量，而不是这个。

我 vs Claude Code

我比 Claude Code 更擅长使用 Clean。

一些休眠项目

Coda 和 risc0-lean4 有一些用于算术电路的 Lean 代码。上次更新是在几年前，所以我没有在比较中包括这些项目。

未来

这个领域会发生什么？在短期内，将出现更多框架。有人会想到多项式电路就像 effectful lenses/relation-oriented programming/representation theory。在中期，除了手工制作的优化电路，人们将停止自己编写电路。大多数多项式电路将自动生成。一些形式验证技术将以越来越少的人工干预来使用。评估验证工作的结果仍然是一个挑战。

zkSecurity 为包括零知识证明、MPC、FHE 和共识协议在内的加密系统提供审计、研究和开发服务。

了解更多 →

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