深潮 TechFlow 消息，5 月 19 日，Vitalik Buterin 个人博客发文，形式化验证（Formal Verification）正在以太坊研发圈及更广泛的计算领域迅速兴起。该技术通过在 Lean 等数学证明工具中编写可自动检验的数学证明，来验证代码的正确性，被研究者称为"软件开发的终极形态"。文章指出，形式化验证尤其适用于目标简单但实现复杂的场景，包括量子抗性签名、STARKs、共识算法及 ZK-EVM 等以太坊核心技术。V 神同时强调，形式化验证并非万能，其局限性在于无法完全捕捉人类意图，且存在规范遗漏、部分代码未被覆盖等风险。

对此，他提出乐观展望：AI 与形式化验证的结合将形成互补——AI 负责高效生成大量代码，形式化验证则确保其准确性，未来软件安全将形成"安全核心+不安全边缘沙盒"的架构模型，以太坊将成为其中重要的安全核心之一。