A deep embedding of Solidity in Isabelle/HOL

By Diego Marmsoler and Achim D. Brucker.

Keywords:
Solidity, Denotational Semantics, Isabelle/HOL

Please cite this work as follows:
D. Marmsoler and A. D. Brucker, “A deep embedding of Solidity in Isabelle/HOL,” Formal Aspects of Computing (FAC), 2025, doi: 10.1145/3700601. Author copy: https://logicalhacking.com/publications/marmsoler.ea-isabelle-solidity-2025/

BibTeX
@Article{ marmsoler.ea:isabelle-solidity:2025,
  author    = {Diego Marmsoler and Achim D. Brucker},
  journal   = {Formal Aspects of Computing (FAC)},
  language  = {USenglish},
  title     = {A deep embedding of {Solidity} in {Isabelle/HOL}},
  year      = {2025},
  issn      = {0934-5043},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  pages     = {},
  volume    = {},
  number    = {},
  areas     = {formal methods, software},
  doi       = {10.1145/3700601},
  keywords  = {Solidity, Denotational Semantics, Isabelle/HOL},
  abstract  = {Smart contracts are computer programs designed to automate
               legal agreements. They are usually developed in a high-level
               programming language, the most popular of which is Solidity.
               Every day, hundreds of thousands of new contracts are deployed
               managing millions of dollars worth of transactions. As for
               every computer program, smart contracts may contain bugs which
               can be exploited. However, since smart contracts are often
               used to automate financial transactions, such exploits may
               result in huge economic losses. In general, it is estimated
               that since 2019, more than $5B was stolen due to
               vulnerabilities in smart contracts.
               
               This paper addresses the issue of smart contract
               vulnerabilities by introducing an executable denotational
               semantics for Solidity within the Isabelle/HOL interactive
               theorem prover. This formal semantics serves as the basis for
               an interactive program verification environment for Solidity
               smart contracts. To evaluate our semantics, we integrate
               grammar-based fuzzing with symbolic execution to automatically
               test it against the Solidity reference implementation. The
               paper concludes by showcasing the formal verification of
               Solidity programs, exemplified through the verification of a
               basic Solidity token.},
  pdf       = {https://logicalhacking.com/publications/marmsoler.ea-isabelle-solidity-2025/marmsoler.ea-isabelle-solidity-2025.pdf},
  note      = {Author copy: \url{https://logicalhacking.com/publications/marmsoler.ea-isabelle-solidity-2025/}},
}