Ethereum's leanVM Tool Reaches Formal Verification Milestone

leanVM, a minimal, hash-based zero-knowledge virtual machine designed to aggregate post-quantum signatures for Ethereum validators, has been formally verified. The verification marks a milestone in the tool's development.

The project is designed to aggregate leanXMSS signatures, a hash-based alternative being developed for validator signing. leanVM is intended to combine those signatures.

Earlier coverage of leanVM's post-quantum signature design described end-to-end formal verification as in progress.

Estimates for Q-Day have accelerated. Quantum computing poses a potential risk to cryptographic security.