Ethereum Foundation researcher Justin Drake announced on November 3 that leanVM, a minimal zkVM designed to aggregate hash-based post-quantum signatures, has completed end-to-end formal verification. The verification confirms the implementation conforms to its specification, marking a key milestone in Ethereum's preparation for quantum-resistant security. leanVM processes over 1,000 leanXMSS aggregations per second, with leanXMSS serving as the planned replacement for BLS signatures at the consensus layer. At Devcon 8, Drake adjusted the target date for Ethereum's full transition to post-quantum security to December 2028, allowing room for required network forks. The migration plan relies on three open-source projects—leanVM, leanXMSS, and leanSpec—with the Foundation advancing formal verification while incentivizing innovation through programs such as the Poseidon Prize.