Ethereum's leanVM Achieves End-to-End Formal Verification; Full Post-Quantum Security Transition Targeted for December 2028. According to CryptoBriefing, Ethereum Foundation researcher Justin Drake announced on November 3rd that leanVM has achieved end-to-end formal verification. leanVM is a minimalist zkVM used for efficiently aggregating hash-based post-quantum signatures, packaging multiple signatures into compact proofs. In terms of performance, leanVM can process 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 time for Ethereum's full transition to post-quantum security to December 2028 to allow for the network forks required for the transition.