Isabelle/Solidity – A Shallow Embedding of Solidity in Isabelle/HOL

@Article{ brucker.ea:afp-isabelle-solidity-shallow:2026,
  author   = {Diego Marmsoler and Asad Ahmed and Achim D. Brucker},
  title    = {{Isabelle/Solidity} -- A Shallow Embedding of Solidity in
              {Isabelle/HOL}},
  journal  = {Archive of Formal Proofs},
  areas    = {security, software},
  month    = {March},
  year     = {2026},
  note     = {\url{https://isa-afp.org/entries/Isabelle-Solidity.html},
              Formal proof development},
  issn     = {2150-914x},
  abstract = {Smart contracts, typically written in high-level languages
              such as Solidity, are programs deployed on the blockchain to
              automate financial transactions. Due to the high-stakes nature
              of these applications, bugs can result in severe financial
              consequences. In this paper, we present a verification
              framework for Solidity smart contracts built within the
              Isabelle/HOL proof assistant. Our approach introduces a novel
              formalization of Soliditys storage model, a shallow
              embedding of its expressions and statements, and custom
              Isabelle commands to facilitate contract specification and
              verification. To aid in the verification process, we also
              provide a verification condition generator. We validate the
              semantics through a suite of unit tests and evaluate the
              framework using four case studies. The results demonstrate
              that our framework enables the verification of complex
              contracts with manageable effort. Furthermore, the use of
              shallow embedding significantly reduces verification
              complexity compared to a deep embedding approach.},
}