leanVM完成端到端形式化验证
以太坊基金会研究员 Justin Drake 于 2026 年 11 月 3 日宣布，面向后量子签名方案的轻量级零知识虚拟机 leanVM 已完成端到端形式化验证。该工具用于聚合基于哈希的后量子签名，减少共识层逐一验证签名的负担。
项目披露的性能指标是每秒可处理超过 1,000 次 leanXMSS 聚合。leanXMSS 是以太坊计划在共识层替代现有 BLS 签名的方案；BLS 目前用于验证者对链状态进行证明。性能数据说明聚合能力，但单凭这一指标不能推断其已具备部署条件。
验证覆盖范围不等于设计本身无误
形式化验证通过数学证明检查软件是否符合既定规格。端到端验证意味着证明覆盖 leanVM 整体工具链，而不只是个别组件；但它证明的是实现符合规格，并不自动证明规格或底层密码学选择没有缺陷。因此，leanSpec 等设计规范的质量仍是安全判断的一部分。
从这些安排看，leanVM 的验证降低了实现层面的一类不确定性，却不能单独代表以太坊后量子迁移已经完成。签名方案更换还涉及验证者软件、客户端实现及配套工具，网络升级也需要协调推进。
完整迁移目标定于2028年12月
Drake 在孟买举行的 Devcon 8 上将以太坊全面转向后量子安全的目标调整为 2028 年 12 月。路线图还包括 leanXMSS 与 leanSpec，并预计迁移需要后续多次网络分叉；以太坊基金会正在开发开源实现和推进形式化验证，也通过 Poseidon Prize 等激励支持相关工作。
这个日期应理解为规划目标，而非完成承诺。迁移时间表的实际约束不仅是聚合性能，还包括规范与实现的验证、客户端适配以及多次分叉的协调。现阶段公布的信息支持“关键工具已完成验证、迁移仍在推进”的判断，不能据此认定全网已经具备后量子安全性。
