火星财经消息，5 月 19 日，以太坊联合创始人 Vitalik Buterin 发文深度解析形式化验证（Formal Verification）技术的现状与前景，认为结合 AI 的形式化验证将成为「软件开发的终极形态」，也是在强大 AI 对手面前守住网络安全底线的关键路径。Vitalik 指出，形式化验证的核心是将代码的正确性转化为可被计算机自动检验的数学定理，从而以数学证明的方式保障软件安全，而非依赖传统测试或人工审计。他认为这一范式尤其适用于「目标远比实现简单」的场景——例如量子抗性签名、STARK 证明系统、拜占庭容错共识算法和 ZK-EVM，这些恰恰是以太坊下一阶段升级的核心技术组件。 然而，Vitalik 也坦承形式化验证并非万能。常见失效模式包括：仅对部分代码进行验证而遗漏关键缺陷、安全规范本身存在疏漏，以及软硬件边界处的旁路攻击难以被现有证明模型捕捉。他强调，「可证明的正确性」在本质上验证的是不同意图表达之间的内在一致性，而非对照人类真实意图的绝对正确。 对于 AI 带来的网络安全挑战，Vitalik 持审慎乐观态度。他认为，AI 辅助的形式化验证将推动软件架构向「安全核心与不安全边缘」的模式演进：边缘组件在沙箱中运行，被授予最小权限；安全核心则通过形式化方法持续强化，承载社会数字化进程中最高级别的信任负担。以太坊将成为这一安全核心的重要组成部分。