Vitalik Buterin 在最新文章中表示，以太坊前沿研发中正兴起一种新范式：直接使用 EVM 字节码、汇编或 Lean 编写代码，并用 Lean 中可自动检查的数学证明验证其正确性。AI 辅助形式化验证有望同时提升代码效率与安全性，尤其适用于 STARK、ZK-EVM、抗量子签名和共识算法等安全核心模块。但他也强调，形式化验证并非万能，仍可能因证明范围不完整、规格错误、硬件侧信道等问题失效；未来软件或将分化为“安全核心”和“非安全边缘”，以太坊将成为重要安全核心之一。https://wublock123.com/news/vitalik-ai-assisted-formal-verification-ethereum-security-61259(吴说区块链)