币圈界报道：

布特林擘画智能时代软件安全新图景：AI赋能形式化验证

以太坊联合创始人维塔利克·布特林近日发布深度文章，系统阐述在人工智能威胁加剧背景下，如何借助形式化验证与智能工具协同构建更可靠的数字基础设施。他认为，未来防御体系的核心将转向由机器辅助完成的数学级代码正确性证明。

低级代码亦可实现可验证的正确性保障

布特林指出，开发者无需仅限于高级语言，即便是EVM字节码或汇编层级的程序，也可借助Lean等逻辑语言进行形式化描述，并生成机器可读的数学证明。人工智能在此过程中扮演加速器角色，能同步生成优化代码与对应证明，大幅降低人工介入成本。

形式化方法正从理论走向复杂系统落地

尽管形式化验证已有数十年历史，但其真正突破点在于人工智能能够承担繁琐且反直觉的细节推导任务。该方法特别适用于密码学协议和共识机制这类目标清晰但实现复杂的领域。布特林列举了包括抗量子签名、STARK证明系统、ZK-EVM以及核心共识算法在内的多个实际应用场景，当前已有Arklib等项目在推进基于形式化验证的可验证实现。

分层架构应对智能攻击的双重挑战

面对日益强大的AI漏洞挖掘能力，布特林主张采用分层防护策略：对关键“安全核心”组件实施全面形式化验证，而对非核心功能则置于受控沙箱中运行。这种设计既保证了核心系统的可信度，又兼顾灵活性与性能。类似理念已开始渗透至加密钱包开发，推动自动化与安全性双提升。

布特林强调，即便代码通过形式化验证，也不能等同于现实世界绝对安全。潜在风险涵盖规范定义不完整、验证工具本身存在缺陷，以及核心与外围模块之间的接口隐患。他提醒：“可证明的正确性并不等于人类所理解的正确。”真正的目标应是建立多层冗余机制，尽可能缩小预期意图与实际行为之间的偏差。

行业共识渐成，重塑去信任化技术根基

这一思想与以太坊长期追求的安全性与效率提升方向高度一致。布特林持续关注人工智能带来的治理挑战，支持开展相关长期研究。随着技术实践逐步深入，若成功落地，AI辅助的形式化验证不仅将强化智能合约安全，更可能彻底改变关键软件的构建范式，使“去信任化”从口号变为坚实的技术基础。