PANews 11月4日消息，據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月仍是目標而非承諾。
