Verifying zkEVMs: Making Large Scale Formal Verification Work (Invited Talk)

Hicks, Alexander

doi:10.4230/OASIcs.FMBC.2026.2

Document

Verifying zkEVMs: Making Large Scale Formal Verification Work (Invited Talk)

Author Alexander Hicks

Part of: Volume: 7th International Workshop on Formal Methods for Blockchains (FMBC 2026)
Part of: Series: Open Access Series in Informatics (OASIcs)
Part of: Conference: Workshop on Formal Methods for Blockchains (FMBC)
License: Creative Commons Attribution 4.0 International license
Publication Date: 2026-05-20

PDF

File

PDF

OASIcs.FMBC.2026.2.pdf

Filesize: 318 kB
1 pages

Document Identifiers

DOI: 10.4230/OASIcs.FMBC.2026.2
URN: urn:nbn:de:0030-drops-256995

Subject Classification

ACM Subject Classification

Software and its engineering → Formal software verification

Keywords

Formal Verification
Zero-Knowledge Virtual Machines

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Document

0

Metadata

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.

Cite As Get BibTex

Alexander Hicks. Verifying zkEVMs: Making Large Scale Formal Verification Work (Invited Talk). In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/OASIcs.FMBC.2026.2

Author Details

Alexander Hicks

Ethereum Foundation, London, UK

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail