Abstract Bio

Verifying zkEVMs: Making Large Scale Formal Verification Work

Alexander Hicks ORCID Ethereum Foundation, London, UK
Abstract

The effort to formally verify core parts of zkVMs for their deployment on the Ethereum L1 has been ongoing for over a year now, with many teams involved and progress across several axes. This talk will focus on formally verifying such a large, complex, and unstable stack, the lessons learned, and the remaining challenges.

Keywords and phrases:
Formal Verification, Zero-Knowledge Virtual Machines
Category:
Invited Talk
Copyright and License:
[Uncaptioned image] © Alexander Hicks; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Software and its engineering → Formal software verification
DOI:
10.4230/OASIcs.FMBC.2026.2
Event:
7th International Workshop on Formal Methods for Blockchains (FMBC 2026)
Editors:
Massimo Bartoletti and Diego Marmsoler
Series and Publisher:
OASIcs Logo Open Access Series in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Bio

Alexander Hicks is a researcher at the Ethereum Foundation where he leads the Protocol Snarkification team focusing on formal verification. As part of this he oversees the verified-zkevm.org project to formally verify critical components of zkVMs ahead of their deployment on the Ethereum L1.