Document Open Access Logo

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

Authors Ashley Card , Diego Marmsoler

PDF

File

Thumbnail PDF
PDF
OASIcs.FMBC.2026.3.pdf
  • Filesize: 0.8 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Ethereum Virtual Machine
  • Isabelle/HOL
  • Smart Contracts

Metrics

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 Get BibTex

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) https://doi.org/10.4230/OASIcs.FMBC.2026.3

Author Details

Ashley Card
  • Department of Computer Science, University of Exeter, UK
Diego Marmsoler
  • Department of Computer Science, University of Exeter, UK

Funding

This work was supported by the Engineering and Physical Sciences Research Council [grant number EP/X027619/1].

Supplementary Materials

References

  1. Hayden Adams, Moody Salem, Noah Zinsmeister, Sara Reynolds, Austin Adams, Will Pote, Mark Toda, Alice Henshaw, Emily Williams, and Dan Robinson. Uniswap v4 Core [Draft], June 2023. Accessed: 2025-12-04. URL: https://raw.githubusercontent.com/jtriley-eth/v4-core/main/whitepaper-v4-draft.pdf.
  2. Asad Ahmed and Diego Marmsoler. Isabelle/Solidity: A tool for the verification of solidity smart contracts (tool paper). In Diego Marmsoler and Meng Xu, editors, 6th International Workshop on Formal Methods for Blockchains, FMBC 2025, Hamilton, Canada, May 4, 2025, volume 129 of OASIcs, pages 12:1-12:9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/OASIcs.FMBC.2025.12.
  3. Wolfgang Ahrendt and Richard Bubel. Functional Verification of Smart Contracts via Strong Data Integrity. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Applications, pages 9-24, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-61467-6_2.
  4. Elvira Albert, Samir Genaim, Daniel Kirchner, and Enrique Martin-Martin. Secure Optimizations on Ethereum Bytecode Jump-Free Sequences. IEEE Transactions on Dependable and Secure Computing, 22(4):3676-3691, 2025. URL: https://doi.org/10.1109/TDSC.2025.3536803.
  5. Sidra Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. Towards verifying ethereum smart contract bytecode in Isabelle/HOL. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pages 66-77, Los Angeles, CA, USA, 2018. ACM. URL: https://doi.org/10.1145/3167084.
  6. Vitalik Buterin and Martin Swende. EIP-2930: Optional access lists. https://eips.ethereum.org/EIPS/eip-2930, 2020. Accessed: 2025‑11‑06.
  7. Franck Cassez. ByteSpector: A Verifying Disassembler for EVM Bytecode. In Diego Marmsoler and Meng Xu, editors, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025), volume 129 of Open Access Series in Informatics (OASIcs), pages 4:1-4:15, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/OASIcs.FMBC.2025.4.
  8. Franck Cassez, Joanne Fuller, Milad K. Ghale, David J. Pearce, and Horacio M. A. Quiles. Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings, pages 571-583, Berlin, Heidelberg, 2023. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-27481-7_32.
  9. Franck Cassez, Joanne Fuller, and Horacio Mijail Antón Quiles. Deductive Verification of Smart Contracts with Dafny. In Formal Methods for Industrial Critical Systems: 27th International Conference, FMICS 2022, Warsaw, Poland, September 14–15, 2022, Proceedings, pages 50-66, Berlin, Heidelberg, 2022. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-15008-1_5.
  10. CertiK. Vyper Incident Analysis, 2023. Accessed 2025-12-01. URL: https://www.certik.com/resources/blog/vyper-incident-anaylsis.
  11. Certora. Certora Prover White Paper. https://www.certora.com/blog/white-paper, 2025.
  12. Ethereum Foundation. ethereum/tests: Common tests for all Ethereum implementations. https://github.com/ethereum/tests. Accessed: 2025‑11‑06.
  13. Emilio Frangella and Lasse Herskind. Aave V3 Technical Paper, January 2022. Accessed: 2025-12-04. URL: https://raw.githubusercontent.com/aave-dao/aave-v3-origin/main/docs/Aave_V3_Technical_Paper.pdf.
  14. Tomer Ganor, Lior Oppenheim, Gad Elbaz, Pamina Georgiou, and Alex Van Der Lelie. Breaking Down the Balancer Hack, November 2025. Accessed 2025-12-04. URL: https://www.certora.com/blog/breaking-down-the-balancer-hack.
  15. Florian Haftmann and Lukas Bulwahn. Code generation from Isabelle/HOL theories. https://isabelle.in.tum.de/doc/codegen.pdf, 2026. Google Scholar
  16. Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pages 204-217, 2018. URL: https://doi.org/10.1109/CSF.2018.00022.
  17. Yoichi Hirai. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In WTSC'17: 1st Workshop on Trusted Smart Contracts, International Conference on Financial Cryptography and Data Security. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-70278-0_33.
  18. Diego Marmsoler, Asad Ahmed, and Achim D. Brucker. Secure smart contracts with Isabelle/Solidity. In Alexandre Madeira and Alexander Knapp, editors, Software Engineering and Formal Methods - 22nd International Conference, SEFM 2024, Aveiro, Portugal, November 6-8, 2024, Proceedings, volume 15280 of Lecture Notes in Computer Science, pages 162-181. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-77382-2_10.
  19. Diego Marmsoler and Achim D. Brucker. Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL. Formal Aspects Computing, October 2024. URL: https://doi.org/10.1145/3700601.
  20. Nethermind. EVMYulLean: Executable formal model of the EVM and Yul in Lean 4, 2025. Accessed: 2025-12-04. URL: https://github.com/NethermindEth/EVMYulLean.
  21. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  22. Grigore Rosu. K: A semantic framework for programming languages and formal analysis tools, pages 186-206. IOS Press, Netherlands, 2017. Publisher Copyright: © 2017 The authors and IOS Press. All rights reserved. URL: https://doi.org/10.3233/978-1-61499-810-5-186.
  23. Gavin Wood. Ethereum: A Secure Decentralised Generalised Transaction Ledger. Technical report, Ethereum Foundation, 2014. Version 1.0. URL: https://ethereum.github.io/yellowpaper/paper.pdf.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact