Vitalik：AI 辅助形式化验证有望同时提升代码效率与安全性

Foresight News 消息，Vitalik Buterin 发文探讨形式化验证在区块链安全领域的应用前景。文章指出，以太坊前沿研发中正兴起一种新范式，直接使用 EVM 字节码、汇编或 Lean 编写代码，并用 Lean 中可自动检查的数学证明验证其正确性，研究者 Yoichi Hirai 将这一范式称为「软件开发的最终形态」。Vitalik 认为，AI 辅助形式化验证有望同时提升代码效率与安全性，尤其适用于 STARK、ZK-EVM、抗量子签名和共识算法等安全核心模块。文章同时强调形式化验证并非万能，仍可能因证明范围不完整、规格错误、硬件侧信道等问题失效；未来软件或将分化为「安全核心」与「非安全边缘」，以太坊将成为重要安全核心之一。