Ethereum Foundation: leanVM has completed end-to-end formal verification, with the comprehensive post-quantum security transition goal set for December 2028

According to CryptoBriefing, Ethereum Foundation researcher Justin Drake announced on November 3 that leanVM has achieved end-to-end formal verification. leanVM is a minimalist zkVM designed for efficiently aggregating hash-based post-quantum signatures, packaging multi-signatures into compact proofs. In terms of performance, leanVM can handle over 1000 leanXMSS aggregations per second; leanXMSS is a hash-based signature scheme planned to replace BLS at the consensus layer.

At Devcon 8, Drake adjusted the target date for Ethereum's full transition to post-quantum security to December 2028, in order to allow space for the network forks needed for the transition. This plan relies on three open-source projects: leanVM, leanXMSS, and leanSpec. The Ethereum Foundation is developing open-source implementations and advancing formal verification, while also encouraging innovation through incentives like the Poseidon Prize. The report noted that the formal verification of leanVM proves that the code meets specifications, but December 2028 remains a target rather than a commitment.