币圈界报道：

布特林：人工智能驱动形式化验证实现加密系统安全跃升

以太坊联合创始人维塔利克·布特林近期阐述了人工智能在增强加密安全方面的潜力，指出其可通过形式化验证技术辅助开发者以数学方式精确确认程序行为，突破传统依赖人工审计与测试的局限。

数学化验证正成为软件可信性基石

布特林阐明，形式化验证利用可被计算机自动检验的数学逻辑，确保代码在预设条件下的正确执行。这一方法使开发者不再仅依赖运行测试，而是能从理论上证明程序功能无误。

尽管手动构建验证证明长期面临效率瓶颈，人工智能有望通过同步生成代码、验证逻辑与测试框架，大幅降低开发成本。他援引研究者平井洋一的观点，认为该模式或将成为未来软件工程的终极范式，但同时提醒人类必须确保初始规范本身具备准确性。

已有多个以太坊生态项目率先实践此路径，涵盖抗量子签名方案、STARK证明系统、拜占庭容错共识机制以及ZK-EVM基础设施。部分团队正探索基于形式化验证的STARK实现，另有研发组尝试以RISC-V汇编语言构建可数学验证的以太坊虚拟机原型。

安全边界扩展：智能系统需应对潜在验证盲区

布特林坦言，形式化验证并非万能。若初始规范存在缺陷，或验证范围未覆盖全部运行场景，即便经过验证的代码仍可能产生错误行为。但他强调，该方法能有效缩小预期行为与实际执行之间的差距。

他进一步指出，人工智能可在生成大量验证证明、测试用例及独立实现版本方面提供支持，从而增强系统整体鲁棒性。此外，他构想未来软件架构应划分为高安全核心层与低风险外围模块，前者负责关键基础设施，后者在受限环境中运行。

以太坊安全体系迈向深度验证时代

布特林将此次讨论置于以太坊基础设施演进的大背景下，认为随着人工智能生成软件日益普及，共识协议与密码学组件等核心系统亟需更深层次的形式化保障。

他相信防御方将借助更先进的验证工具，有效抵御由人工智能赋能的新型攻击手段，并引用Mozilla公司内部部署自动化漏洞挖掘系统的经验作为佐证。当前去中心化金融平台频繁遭遇智能合约漏洞与底层缺陷引发的安全事件，凸显了强化验证机制的紧迫性。