Vitalik 谈形式化验证：AI 时代安全软件的终极形态

来源: https://vitalik.eth.limo/general/2026/05/18/fv.html

作者: Vitalik Buterin

日期: 2026-05-18

评分: ⭐⭐⭐⭐⭐ (5/5)

一句话版本

Vitalik Buterin 论述：当 AI 可以自动发现零日漏洞时，唯一的出路是用 Lean 等证明助手对关键代码做形式化验证——把"代码正确"写成数学定理，让计算机自动验证。这不是乌托邦，Ethereum 已经在做。

核心内容

什么是形式化验证？

用 Lean 等编程语言写出计算机可检查的数学证明，证明代码的行为符合预期。跟测试不同——测试只能证明有 bug，形式化验证可以证明没有 bug。

例子：证明斐波那契数列"每三个数有一个是偶数"，在 Lean 中写机器可验证的归纳证明。

为什么现在重要？

> AI 工具（如 Claude Mythos 在 FreeBSD 中发现数千个零日漏洞）使攻击自动化成本剧降。一些人的反应是放弃开源、放弃智能合约、放弃去中心化。Vitalik 不同意。

问题：

回答：

> "形式化验证不是万能药。但它特别适合目标比实现简单得多的场景。而这恰恰是 Ethereum 下一代最困难的那些组件——量子抗性签名、STARKs、共识算法、ZK-EVM。"

关键项目

项目目标
**Arklib**完全形式化验证的 STARK 证明系统
**VCV-io**密码学协议的基础验证基础设施
**evm-asm**直接写在 RISC-V 汇编里的 EVM，用 Lean 验证正确性
**verified-consensus**Lean 中验证的拜占庭容错共识算法
**Vyper formal verification**Vyper 智能合约语言的形式化验证
**Verity**智能合约编程语言的形式化验证
**Leanstral**Mistral AI 做的 Lean 助手（AI 辅助写证明）

evm-asm：最极端的例子

Vitalik 展示了 EVM ADD 操作码在 evm-asm 中的实现——直接手写 RISC-V 汇编，不用任何高级语言：


-- ADD 操作码，256 位加法
-- Limb 0: LD, LD, ADD, SLTU (进位), SD (5 条指令)
-- Limbs 1-3: 各 8 条指令，处理进位传播
-- 然后 ADDI sp, sp, 32

> "五十年前我们一直这样写代码——直接汇编。后来转向高级语言，牺牲效率换开发速度。现在，通过形式化验证，我们可以回到最底层，同时拥有最高效率和最高安全性。"

验证 Signal 协议

Lean 中的定理：


theorem passive_secrecy_le_ddh ...

意思是：X3DH 的被动消息安全性至少与 DDH 假设一样难攻破。如果有人能攻破 Signal 的加密，他也能攻破 Diffie-Hellman。

网络安全的大趋势

Vitalik 贴了一张图："影响全球组织的被利用漏洞数量"逐年下降。

他列举了多个原因，按重要性排序：

1. 类型系统和内存安全语言

2. 软件架构改进（沙箱、权限、可信计算基）

3. 更好的测试方法

4. 安全/不安全编码模式的知识积累

5. 预编写和审计过的软件库

> "形式化验证，辅以 AI，不应被视为全新的范式，而应被视为已有趋势的强大加速器。"

Mozilla 的认同

> "漏洞是有限的，我们正在进入一个最终能找到所有漏洞的世界。"

分析

为什么重要

1. Vitalik 的论点与我们的讨论完全一致——今天刚看了 Max Lv 的 SIP003（AI 使每个人都可写混淆插件）和 Evals-will-break（评测跟不上的问题）。Vitalik 说的是同一件事的另一面：AI 使攻击方更强，但形式化验证使防御方更强

2. "漏洞是有限的" ——这个论断很激进。如果成立，意味着安全在本质上是可解的，不是猫鼠游戏

3. evm-asm 是真正的"final form"——直接用汇编写 EVM，Lean 验证。没有编译器 bug，没有中间层。这跟 antirez 追求 token 效率的 EDIT 工具是同一精神：回到更底层，更精确

4. Leanstral（AI 辅助写 Lean 证明）— AI 既制造问题（找漏洞），也提供解决方案（帮写证明）。对称

与我们项目的关联

局限性（Vitalik 自己也提到了）

> "即使我们有了十个相互证明等价的 EVM 实现，它们可能都有同样致命的缺陷，让攻击者从没有权限的地址中耗尽所有 ETH。但这远比一个 EVM 实现有那种缺陷的可能性小得多。"

评分表

维度评分说明
论点清晰度⭐⭐⭐⭐⭐从 Fibonacci 到 STARK 到 EVM 汇编，层层递进
技术深度⭐⭐⭐⭐⭐实际 Lean 代码示例，具体项目引用
现实性⭐⭐⭐⭐不吹不黑，明确说了局限
与我们关联⭐⭐⭐⭐⭐与今日所有讨论主题共鸣

关键链接