以太坊核心安全新实验：形式化验证加速落地

核心提要：以太坊联合创始人维塔利克·布特林披露，社区正推进基于Lean工具的形式化验证实验，聚焦虚拟机与低级代码的安全性检验，旨在提升系统底层防御能力。

以太坊启动低级代码形式化验证实验，强化核心基础设施安全

以太坊联合创始人维塔利克·布特林近日透露，社区正开展一项前沿技术试验，利用Lean等形式化验证框架，对以太坊虚拟机的字节码及RISC-V汇编语言实现进行精确性与安全性审查。

核心系统安全检验迎来新范式，验证覆盖关键协议层

布特林表示，该技术可广泛应用于加密通信机制、共识算法逻辑以及虚拟机底层实现等高风险组件的可靠性评估。在人工智能持续增强漏洞挖掘能力的背景下，形式化验证为防御方提供了可量化的安全保障路径。

验证边界仍存挑战，未来架构或将趋向安全核心化

尽管前景广阔，布特林也提醒，当前方法受限于建模完整性，未纳入假设条件、侧信道攻击路径及非验证模块仍可能引入未知风险。他预测，未来软件体系或将以少数经过严格验证的核心组件为基础构建，而人工智能将逐步接管代码生成任务。