币圈界报道：

以太坊推进低级代码形式化验证，强化底层安全

以太坊联合创始人维塔利克·布特林近日透露，社区正在启动一项实验性项目，采用Lean等先进形式化验证框架，对以太坊虚拟机的字节码及RISC-V汇编语言实现进行精确校验，以提升系统在底层逻辑层面的可靠性。

核心基础设施安全检验迎来新范式

布特林表示，形式化验证可有效应用于加密通信协议、共识机制以及虚拟机实现等关键组件的安全评估。在当前人工智能已能自动识别代码缺陷的背景下，该方法为防御方提供了更强的理论保障与可证明的安全边界。

验证边界与未来架构演进的深层思考

他同时提醒，该技术存在明显局限——若模型未覆盖全部运行假设、或涉及侧信道攻击路径，仍可能遗漏潜在风险。布特林展望，未来软件体系或将围绕极少数经过严格验证的核心模块构建，而人工智能将逐步接管代码生成任务，形成“可信核心+智能生成”的新型开发范式。