以太坊联合创始人详述:AI辅助形式化验证将如何重塑安全软件构建范式
以太坊联合创始人维塔利克·布特林近日发表深度论述,指出AI辅助的形式化验证可能从根本上改变安全软件的构建方式。这一观点旨在回应网络安全界日益增长的悲观论调——随着AI驱动攻击能力的增强,无信任系统是否还能存续。
“许多人声称,在AI辅助漏洞挖掘的时代,编写安全代码将变得不可能。”布特林写道,“但我对此持更为乐观的态度,而AI辅助的形式化验证正是关键原因所在。”
形式化验证的本质
形式化验证是指为代码编写数学证明,并通过计算机自动检验的过程。开发者不再依赖测试并期望不出现漏洞,而是通过数学证明确保代码在所有条件下都能严格按预期运行。
该技术虽已存在数十年,却始终局限于小众领域,因为手工编写证明极其困难且耗时。布特林认为,AI将彻底改变这一局面——AI既能编写代码也能生成证明,人类仅需验证所证明的命题是否符合软件的实际功能需求。
他将这种模式称为研究者Yoichi Hirai所言的“软件开发的终极形态”。
对以太坊生态的意义
布特林列举了形式化验证已在以太坊开发生态中应用的多个领域:抗量子签名、STARK证明系统、共识算法以及ZK-EVM。这些领域的安全特性易于定义,但底层代码极为复杂。
Arklib等项目正致力于实现完全形式化验证的STARK系统;evm-asm项目则直接使用RISC-V汇编语言构建完整EVM,并通过数学验证确保其与可读参考实现的一致性;拜占庭容错共识协议也正在Lean定理证明器中接受形式化规范与验证。
核心洞见在于:对于这些系统,代码行为与预期目标之间的鸿沟可以通过数学确定性(而非概率性测试)来弥合。
技术局限的审慎思考
布特林谨慎指出形式化验证存在实际局限性:证明可能仅覆盖系统部分模块,关键漏洞藏匿于未验证区域;开发者可能遗漏重要属性规范;形式化规范本身可能存在错误;侧信道攻击等硬件漏洞甚至可以绕过数学层面正确的软件。
“可证明正确性并不等同于人类通常理解的正确性。”他强调。形式化验证的真正价值在于,允许开发者以多种冗余方式表达设计意图,并自动检验这些表达之间的一致性。
未来生态架构展望
布特林描绘了一个分层的软件架构愿景:非安全边缘层处理低风险功能,在沙箱环境中以最小权限运行;安全核心层则管理所有关键组件,包括以太坊协议本身、操作系统内核及敏感物联网基础设施。
安全核心将被刻意保持精简,并接受严格的形式化验证。AI提供的大规模计算能力使验证具备实践可行性。最终目标并非创造零漏洞软件,而是让最关键组件获得数学层面的可信保障,而非寄托于概率性期望。
“防御者终于有机会获得决定性胜利。”他总结道,并援引Mozilla通过强化代码库抵御AI辅助攻击工具的实践案例佐证这一观点。
ETH

交易所
交易所排行榜
24小时成交排行榜
人气排行榜
交易所比特币余额
交易所资产透明度证明
去中心化交易所
资金费率
资金费率热力图
爆仓数据
清算最大痛点
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
ETF追踪
索拉纳ETF
瑞波币ETF
香港ETF
比特币持币公司
加密资产反转
以太坊储备
HyperLiquid钱包分析
Hyperliquid鲸鱼监控
大额转账
链上异动
比特币回报率
稳定币市值
期权分析
新闻
文章
财经日历
专题
钱包
合约计算器
账号安全
资讯收藏
自选币种
我的关注