币圈界报道：

布特林展望：人工智能驱动加密系统形式化验证新纪元

以太坊联合创始人维塔利克·布特林近日发表观点，认为人工智能在形式化验证工具的加持下，有望实现对加密系统更深层次的安全保障。他指出，借助数学方法对代码行为进行严格推导与证明，可有效弥补传统审计与测试手段的局限性，尤其适用于以太坊底层基础设施、共识机制、密码学算法及零知识技术等核心领域。

自动化数学验证正成为开发新范式

布特林阐述，形式化验证通过计算机可验证的数学逻辑，确保程序在特定条件下始终按预期运行。这使得开发者不再仅依赖运行时测试，而是能够从理论上确认代码正确性。然而，人工编写验证证明长期面临效率低下与复杂度高的挑战。

为此，人工智能被赋予新角色——同步生成代码、验证证明及配套测试结构，大幅降低开发门槛。布特林援引研究者平井洋一的观点，称此模式或将成为软件工程的终极形态，但强调人类仍需确保初始规范本身无误。

多类以太坊核心项目已落地实践

目前已有多个以太坊相关项目启动形式化验证应用，涵盖抗量子数字签名方案、基于STARK的证明系统、拜占庭容错共识协议以及支持零知识证明的EVM兼容架构。部分团队正推进针对STARK的完整形式化验证流程，另有研究组尝试基于RISC-V指令集构建可数学验证的以太坊虚拟机原型。

安全边界认知深化：风险与应对并行

布特林承认，形式化验证并非万能。若初始规范存在缺陷，或验证范围未覆盖全部逻辑路径，则即便通过验证的代码仍可能出错。但他强调，该方法显著缩小了预期行为与实际执行之间的偏差空间。人工智能在此过程中可加速生成更多验证案例、测试用例及独立实现版本，增强系统鲁棒性。

他进一步设想未来软件架构应划分为高安全核心与低风险外围模块。前者将仅包含经深度验证的关键组件，运行于最小权限环境；后者则在受控条件下处理非敏感任务。

以太坊安全体系迈向纵深防御阶段

布特林将上述讨论置于以太坊整体安全演进背景下。随着人工智能生成代码日益普及，共识机制与密码基础设施亟需更高阶的验证能力。他认为，防御方终将掌握更强大的工具，以对抗智能化攻击。他引用Mozilla公司内部使用自动化工具挖掘系统漏洞的经验，佐证这一趋势的可行性。

当前去中心化金融生态频繁遭遇智能合约漏洞引发的资产损失事件，促使行业对深层安全机制的需求愈发迫切，而形式化验证与AI协同正是回应这一挑战的重要方向。