以太坊基金會：leanVM 完成端到端形式化驗證，全面後量子安全過渡目標定於 2028 年 12 月

据 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 月仍是目標而非承諾。