内容摘要与导读： 一种软件开发的新范式：使用AI代理直接编写RISC-V汇编代码，并在Lean证明助手中进行形式化验证，确保zkVM的guest程序无bug。由于RISC-V汇编易于推理，且AI代理能自动编写代码和证明，这种方法比使用Rust、C等高级语言更可靠，避免了编译器优化带来的不确定性和未定义行为。
这篇文章终结了软件开发。我找到了最终形态。从历史意义上讲是最终的，从范畴论意义上讲也是最终的。别担心——这很有趣。
我在葡萄牙的一家咖啡馆里喝着饮料，思考人生，与此同时，拉取请求自动弹出。它们添加新的 Lean 定理或重构现有的 Lean 证明。CI 变绿通常意味着正确。我可以在手机上浏览代码并点击合并。
— @pirapira
别告诉我在手机上构建最快的 EVM 实现 😎
— @butta_eth
译者注：Lean 是一种兼具函数式编程语言与定理证明器（Theorem Prover） 双重身份的现代化语言。它的核心设计目标是帮助人们实现"数学形式化"以及"软件形式化验证"，但同时它也是一种通用编程语言，具有极高的灵活性和性能。
我经常在手机上做这件事，每天产生 200 到 600 次提交。在不久的将来，我认为我甚至不需要在手机上操作。有时智能体会犯错，但当证明卡住时，它们自己会注意到错误。在 云栈社区 的技术讨论中，我们经常探讨这类自动化开发的边界问题。
zkVM 需要可靠的客户程序
有一些 RISC-V 虚拟机可以产生简洁的知识论证（zkVM），通过密码学方式证明一个带有特定输入的 RISC-V 程序会产生特定的输出。当客户程序出现 bug 时会发生什么？某天，验证器接受了一个用于 zkVM 执行的密码学证明，从而引发了问题。你试图找出哪里出了问题。从公开可用的信息中，你得到了一些密码学承诺以及这些承诺的一些打开值。这些通常是无意义的数字。要弄清楚哪里出了问题，需要花费大量时间，甚至可能是不可能的。因此，知道 zkVM 的客户程序没有 bug 非常重要。
方法
我的方法是让 AI 智能体（目前是 Claude Code 的 /loop 命令）编写 RISC-V 汇编代码，并在证明辅助工具 Lean 中证明其正确性。没有 Rust，没有 C，没有 C++，只有 RISC-V 汇编代码和 Lean 证明。
这是一种已知的方法：汇编代码的形式验证是一个古老的话题。我目前的方法基于一篇 2013 年的研究论文，名为 "Coq: 世界上最好的宏汇编器？"。我大约十年前看到了这篇论文。我曾想尝试这种方法，但手动编写 Rocq（从 Coq 改名而来）证明似乎消耗太多时间，所以我从未尝试。在 2025 年，机器已经开始在证明辅助工具（如 Rocq 和 Lean）中编写证明，因此现在使用证明辅助工具作为汇编器是合理的。
这很简单：RISC-V 汇编非常容易推理。这比 Rust、C 和 C++ 容易得多。当我们编写关于这些编程语言的证明时，我们需要跟踪作用域中的变量、内存中的对象、已构造的内容、虚方法、有符号整数加法可能是未定义行为等等。RISC-V 没有这些，只有寄存器和内存中的值。此外，由于 AI 智能体自己编写汇编代码，它们已经知道汇编代码在做什么以及如何工作。这比从编译器获得优化输出并进行侦探工作容易得多。
这有效：你可以看看 evm-asm 仓库。以太坊虚拟机的某些部分已经用 RISC-V 汇编代码编写，并且有关于这些 RISC-V 汇编代码的已验证规范。我的 AI 智能体（目前是 Claude Code 的 /loop 命令）目前正在进行大量的重构，并开发一个复杂的除法算法。我认为一旦 zkVM 可以接收提示输入，我就不需要复杂的除法算法了，但看着它很有趣。
看起来是怎样的
代码只是一连串的指令。这实现了 EVM 中的 256 位加法。
def evm_add : Program :=
-- Limb 0 (5 条指令)
LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;
ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;
-- Limb 1 (8 条指令)
LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;
-- Limb 2 (8 条指令)
LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;
-- Limb 3 (8 条指令)
LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;
-- sp 调整
ADDI .x12 .x12 32
该程序的规范看起来像这样：
cpsTriple base (base + 120) code
(-- 寄存器 + 内存
(.x12 ↦ᵣ sp) ** (.x7 ↦ᵣ v7) ** (.x6 ↦ᵣ v6) ** (.x5 ↦ᵣ v5) ** (.x11 ↦ᵣ v11) **
evmWordIs sp a ** evmWordIs (sp + 32) b)
(-- 寄存器 + 内存（更新后）
(.x12 ↦ᵣ (sp + 32)) ** (.x7 ↦ᵣ result3) ** (.x6 ↦ᵣ carry3b) **
(.x5 ↦ᵣ carry3) ** (.x11 ↦ᵣ carry3a) **
evmWordIs sp a ** evmWordIs (sp + 32) (a + b)) := by
重要的是 b 被替换为 a + b。这里的 a + b 是以 256 位数字相加的。同时 sp 移动到 sp + 32。这个变化表明一个 EVM 字从 EVM 栈中被弹出。
在这个规范之后，有 20 行晦涩的代码（称为 Lean 证明）。这仅仅是为了让 Lean 内核相信该规范总是成立。我碰巧能在一定程度上阅读 Lean 证明，但我怀疑这正在变成一项过时的技能；如果你给他们喂 一个链接，你的编码智能体可能可以解释。
其他选项
我从事程序验证大约十年了，所以我可以列出一些知道没有 bug 的方法。很简单：创建正确的源代码，并将其转化为正确的机器码。
形式验证的编译器
有一个经过形式验证的 C 编译器叫做 CompCert。一种方法是对 C 源代码进行形式验证，然后将得到的正确 C 代码通过 CompCert 转化为正确的 RISC-V 代码。
我认为这种方法有效。唯一的问题是生成代码的性能：
CompCert 生成的代码运行速度至少是 GCC 无优化（gcc -O0）生成代码的两倍，并且比 GCC 4 在优化级别 1（gcc -O1）下慢约 10%，在优化级别 2（gcc -O2）下慢约 15%，在优化级别 3（gcc -O3）下慢约 20%。
— compcert.org
在性能至上的情境中，人们正试图让 zkVM 证明者在几秒钟内为整个以太坊区块生成密码学证明，这是一个障碍。
还有另一个经过形式验证的编译器叫做 CakeML。CakeML 可以编译 StandardML。CakeML 有一个 RISC-V 后端。生成的 RISC-V 代码会执行垃圾回收。当人们努力缩短 zkVM 的证明时间时，为垃圾回收的执行生成证明并不那么有吸引力。
那 Rust 呢？
对于系统级开发，Rust 是由熟悉程序验证的人设计的。Rust 有很多程序验证工具。瓶颈似乎在于将"正确"的 Rust 代码转化为正确的汇编程序（要么通过形式验证的编译器，要么在每次编译后将汇编与源代码进行比较）。
为什么我要在"正确"的 Rust 代码上加引号？这是因为我不完全确定 Rust 程序的含义。Rust 的语言规范仍在开发中。目前，Rust 编译器决定了 Rust 程序的含义。Rust 编译器本身也是用 Rust 编写的，因此 Rust 编译器的含义是由 Rust 编译器自身决定的。所以，你最终会去查看汇编代码或机器码。
尽管如此，可以在证明辅助工具中编写自己的 Rust 语义，并将其作为中间步骤，使汇编代码得到形式验证。也许从长远来看，这是正确的道路。当你在 Lean 中完成所有步骤时，这种方法可以通过规范的方式转化为"仅汇编代码和 Lean"的方法。这就是使得"仅汇编代码和 Lean"在范畴论意义上成为最终方法的典型变换。
C 和 C++ 呢？
C 和 C++ 有编程语言规范。编程语言规范充当编译器和程序员之间的接口。这些语言规范规定，当某些情况发生时（有符号整数溢出、指针加指针、计算超出数组一个元素以上的指针、访问错误的指针等），程序的行为是未定义的。当你对 C 或 C++ 进行程序验证时，大部分工作都花在证明这些事情永远不会发生上。未定义行为对编译器很有帮助，特别是在它们优化输出代码时。我做出了一个权衡。我不想推理缺少未定义行为的情况，所以我放弃了编译器。得益于 LLM，可以直接生成汇编代码。
更多学术项目
有一些小型编程语言可以编译为 RISC-V，比如 bedrock2 和 Jasmin。这些语言在 Rocq 中有规范，并带有形式验证的编译器。Jasmin 专注于密码学。也许它可以被改编用于 EVM 实现。
Bedrock2 更具通用性。Bedrock2 的方法很有启发性。Bedrock2 的卖点是软件和硬件的整体协同验证。在验证 zkEVM 的背景下，以整体方式组织对 zkVM 和客户程序的形式验证非常重要。evm-asm 的程序逻辑与 Bedrock2 类似，这在 计算机基础 相关的底层软件开发中具有借鉴意义。
由于 zkVM 的性能特征与 RISC-V 硬件非常不同，所需的汇编代码可能也非常不同，所以我将尝试直接进行汇编编程。此外，我们可能想修改目标 zkVM 以偏离 RISC-V（也许 更多寄存器）。
为什么是最终形态
有大量的编程语言和编译器。它们有很好的抽象和很好的优化技术。所有这些都可以转化为汇编 + Lean 范式。这就是为什么汇编 + Lean 范式是软件开发的最终形态。
图片由 ChatGPT 生成。语法、风格和摘要生成由 Claude Code 协助。
zkSecurity 为包括零知识证明、MPC、FHE 和共识协议在内的密码学系统提供审计、研究和开发服务。
发表于 1 小时前
|
查看: 3|
回复: 0
