Email Gateway (Mar 17 2026 at 17:56): Email Gateway (Mar 17 2026 at 17:56):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce a quite large and interesting development:
Isabelle/Solidity - A shallow Embedding of Solidity in Isabelle/HOL
Diego Marmsoler , Asad Ahmed and Achim D. Brucker
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 Solidity’s 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.
https://www.isa-afp.org/entries/Isabelle-Solidity.html
(There is also a paper: https://dl.acm.org/doi/10.1145/3700601)
Last updated: Mar 21 2026 at 20:30 UTC