Vitalik：AI 辅助形式化验证是“软件开发终极形态”，以太坊成为安全核心

以太坊联合创始人 Vitalik Buterin 于 5 月 18 日发布深度分析，探讨形式化验证（Formal Verification）技术的现状与前景，认为 AI 辅助的形式化验证将成为“软件开发的最终形态”，并指出以太坊将成为未来“安全核心”架构的重要组成部分。



## 形式化验证的核心原理与适用场景

根据 Vitalik 文章确认，形式化验证特别适用于“目标远比实现简单”的场景，他明确列出以太坊下一阶段升级的四类核心技术组件：



量子抗性签名：已有 SPHINCS 签名变体的形式化验证工作

STARK 证明系统：Arklib 项目致力于创建完全形式化验证的 STARK 实现

拜占庭容错共识算法：目前正致力于正式规定和证明 Lean 共识的安全属性

ZK-EVM：evm-asm 项目旨在建立完整的形式化验证 EVM 实现（直接用 RISC-V 汇编语言编写）

Vitalik 引用平井洋一的说法，将此方法称为“软件开发的最终形态”。



## Vitalik 描述的“安全核心”架构演进方向

根据 Vitalik 文章确认，他描述了未来软件架构的演进模式：



安全核心：通过形式化方法持续强化，承载最高信任；Vitalik 明确表示以太坊、作业系统核心和物联网相关应用将成为安全核心。



不安全边缘：边缘组件在沙箱环境中运行，被授予完成工作所需的最低权限；若边缘组件故障，安全核心提供保护。



## 形式化验证的确认限制与失败模式

Vitalik 坦承形式化验证并非万能，援引 Nadim Kobeissi（Cryspen）等研究者的工作，确认的三类主要失败模式：部分验证遗漏（仅验证部分代码，而未验证的部分存在关键缺陷）；规范疏漏（安全规范本身错误或证明中包含错误假设）；旁路攻击（软硬件边界处的侧通道攻击难以被现有模型捕捉）。



Vitalik 强调，“可证明的正确性”在本质上验证的是不同意图表达之间的内在一致性，而非与人类真实意图的绝对对应。



## AI 辅助形式化验证的确认工具

根据 Vitalik 文章确认的可用工具：Lean（数学证明语言，可自动验证定理）；Claude 和 Deepseek 4 Pro（Vitalik 确认足以用于编写 Lean 证明）；Leanstral（1190 亿参数开放权重模型，专门针对 Lean 编写微调，可在本地运行，基准测试表现优于许多规模更大的通用模型）。



## 常见问题

#### Vitalik 为何认为以太坊应成为“安全核心”？
根据 Vitalik 的文章，以太坊与作业系统核心类似，承载着社会数字化过程中的最高级别的信任。他指出，安全核心的设计目标是让其安全性达到不允许漏洞代码泛滥的标准，并将所有 AI 带来的额外算力投入到提升安全核心的安全性上。



#### 形式化验证为何特别适合 STARK、ZK-EVM 等技术？
根据 Vitalik 的分析，这些技术的共同特点是“目标远比实现简单”——其安全属性可用数学语言清晰定义，但具体实现极为复杂，恰恰是形式化验证最能发挥作用的场景。



#### Vitalik 如何建议开发者实际使用 AI 辅助形式化验证？
根据 Vitalik 的文章，他建议让 AI 编写 Lean 代码和数学证明，用户最终只需核查被证明的语句是否符合预期，而无需自行编写繁琐的底层证明代码。他确认 Claude、Deepseek 4 Pro 和 Leanstral 是目前可用的主要工具。