Formal Verification and the $20M zkEVM Initiative

The Protocol Snarkification team at the Ethereum Foundation, led by Alex Hicks, is formally verifying the SNARK primitives that underpin post-quantum signature aggregation.

What formal verification means in practice

Formal verification is the process of mathematically proving that a piece of software behaves exactly as its specification defines. Unlike testing, which checks specific cases, formal verification covers all possible inputs and execution paths.

Why it matters for the PQ transition

The post-quantum transition introduces new cryptographic machinery — particularly the SNARK-based aggregation system that replaces BLS. If this machinery contains subtle bugs, the consequences range from consensus failures to exploitable vulnerabilities.

The $20M initiative

The zkEVM Formal Verification Project is a $20M initiative dedicated to formally verifying critical cryptographic components. This includes the SNARK circuits used in leanMultisig, the hash function implementations used in leanSig, and the virtual machine specification of leanVM.

Ensuring correctness

This work ensures that the machinery we build behaves exactly as mathematically defined, with no room for deviant execution. In a system securing hundreds of billions of dollars, this level of assurance is not optional.