币圈界报道：

以太坊推进低级代码安全验证：形式化技术成新焦点

以太坊联合创始人维塔利克·布特林近日披露，社区正在开展一项前沿实验，利用Lean等数学化验证工具，对以太坊虚拟机的字节码及RISC-V架构下的汇编语言实现进行精确性与安全性的系统性审查。

核心系统安全检验的新范式：从经验到证明

布特林表示，形式化验证可覆盖加密通信协议、共识机制以及EVM底层实现等关键组件的安全评估。在人工智能日益擅长自动挖掘漏洞的背景下，该方法为防御方提供了基于逻辑严密性的主动防护能力。

验证边界与未来架构演进：技术仍需理性看待

他同时提醒，当前验证体系受限于建模完整性，未纳入的假设条件、侧信道攻击路径以及未被覆盖的代码模块，依然可能成为安全隐患。展望未来，布特林认为软件生态或将趋向围绕极少数经验证的安全内核构建，而人工智能则将在代码生成环节扮演主导角色。