以太坊leanVM完成端到端形式化验证，全面后量子安全过渡目标定于2028年12月
TREE NEWS 报道， 以太坊基金会研究员Justin Drake于11月3日宣布，leanVM已实现端到端形式化验证。leanVM是一种极简zkVM，用于高效聚合基于哈希的后量子签名，将多签名打包为紧凑证明。
性能上，leanVM每秒可处理超过1000次leanXMSS聚合；leanXMSS是计划在共识层替代BLS的基于哈希的签名方案。形式化验证确保了zkVM的实现从数学上保证正确执行，这对于共识关键基础设施至关重要。
行业分析与影响
这一成果解决了区块链网络面临的最紧迫的长期风险之一：量子计算机可能破解当前椭圆曲线密码学的潜力。尽管能够攻击ECDSA和BLS签名的大规模量子计算机尚未出现，但这一威胁被认为足够可信，以至于主要协议已开始规划迁移。
以太坊的方法值得注意的是其对形式化验证的重视。通过证明leanVM电路和实现的正确性，基金会降低了过渡期间可能危及安全的细微漏洞的风险。这一点尤其重要，因为共识层变更需要极高的可靠性。
使用leanXMSS等基于哈希的签名是一种刻意选择。基于哈希的方案被认为能抵抗量子攻击，但会产生更大的签名，需要聚合才能保持实用性。leanVM每秒聚合超过1000个签名的能力表明性能开销可能是可控的。
Drake还将以太坊全面后量子过渡的时间线调整至2028年12月，理由是需要为必要的网络分叉留出时间。这一时间线比一些早期估计更为保守，反映了升级一个活跃去中心化网络的复杂性。
前瞻性视角
leanVM的形式化验证是基础性的一步，但仍有许多挑战。过渡需要客户端、验证者和更广泛生态系统的协调升级。它还引发了关于向后兼容性以及现有资产和智能合约迁移的问题。
如果成功，以太坊的后量子过渡可能为其他区块链树立先例。形式化验证与基于哈希的密码学的结合可能成为抗量子共识的蓝图。然而，2028年的目标留下了一个窗口期，在此期间量子进展可能加速，行业将密切关注进一步的里程碑。
