以太坊基金会：leanVM 完成端到端形式化验证，全面后量子安全过渡目标定于 2028 年 12 月

ChainCatcher 消息，据 CryptoBriefing 报道，以太坊基金会研究员 Justin Drake 于 11 月 3 日宣布，leanVM 已实现端到端形式化验证。leanVM 是一种极简 zkVM，用于高效聚合基于哈希的后量子签名，将多签名打包为紧凑证明。性能上，leanVM 每秒可处理超过 1000 次 leanXMSS 聚合；leanXMSS 是计划在共识层替代 BLS 的基于哈希的签名方案。

在 Devcon 8 上，Drake 将以太坊全面过渡至后量子安全的目标时间调整至 2028 年 12 月，以便为过渡所需的网络分叉留出空间。该计划依赖 leanVM、leanXMSS 和 leanSpec 三个开源项目，以太坊基金会正开发开源实现并推进形式化验证，同时通过 Poseidon Prize 等激励鼓励创新。报道指出，leanVM 的形式化验证证明了代码符合规范，但 2028 年 12 月仍是目标而非承诺。