DROPS

Document

DOI: 10.4230/OASIcs.FMBC.2026.3

Isabelle/EVM: A Novel Formalization of the EVM in Isabelle/HOL

Authors: Ashley Card and Diego Marmsoler

Published in: OASIcs, Volume 142, 7th International Workshop on Formal Methods for Blockchains (FMBC 2026)

Abstract

Smart contracts deployed on the Ethereum blockchain execute on the Ethereum Virtual Machine (EVM) and handle financial operations such as payments, asset transfers, and auctions. Given the high value they control, correctness in these contracts is critical, as errors and vulnerabilities have led to losses totalling hundreds of millions of dollars. To address this problem, we develop a novel formalization of the EVM. Compared to existing formalizations, our formalization is in Isabelle/HOL, covers all current EVM opcodes, and formalizes cross-contract execution. Thus, it allows us to express properties which are out of scope for other formalizations. To allow for the execution of our formalization, we implement a code generator, allowing it to be exported as a stand-alone Haskell program. We then validate the semantics by executing νmprint{25000} test cases from the official Ethereum test suite. Our formalization can be used to verify concrete smart contracts but also to reason about the correctness of tools and techniques which manipulate bytecode, such as compilers or optimizers.

Cite as

Ashley Card and Diego Marmsoler. Isabelle/EVM: A Novel Formalization of the EVM in Isabelle/HOL. In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{card_et_al:OASIcs.FMBC.2026.3,
  author =	{Card, Ashley and Marmsoler, Diego},
  title =	{{Isabelle/EVM: A Novel Formalization of the EVM in Isabelle/HOL}},
  booktitle =	{7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
  pages =	{3:1--3:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-424-6},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{142},
  editor =	{Bartoletti, Massimo and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.3},
  URN =		{urn:nbn:de:0030-drops-257005},
  doi =		{10.4230/OASIcs.FMBC.2026.3},
  annote =	{Keywords: Ethereum Virtual Machine, Isabelle/HOL, Smart Contracts}
}

Search Results

Documents authored by Card, Ashley

Isabelle/EVM: A Novel Formalization of the EVM in Isabelle/HOL

Abstract

Cite as

Thanks for your feedback!

Could not send message