Secure Smart Contracts with Isabelle/Solidity -

Our paper, titled: Isabelle/Solidity: A Tool for the Verification of
Solidity Smart Contracts, published in 6th International Workshop on Formal Methods for Blockchains (FMBC 2025) held on May 04, 2025, co-located with ETAPS 2025, May 3–8, 2025, Hamilton, Canada, McMaster University

Our paper Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL is published in Formal Aspects of Computing. 

Paper published in the refereed proceedings of the 22nd International Conference on Software Engineering and Formal Methods, SEFM 2024, held in Aveiro, Portugal, during November 6–8, 2024.

Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. The framework consists of a novel formalization of the Solidity storage model, a shallow embedding of Solidity expressions and statements, an implementation of Isabelle commands to support a user in specifying Solidity smart contracts, and a verification condition generator to support a user in the verification. Compliance of the semantics is tested by a set of unit tests and the approach is evaluated by means of three case studies. Our results show that the framework can be used to verify even complex contracts with reasonable effort. Moreover, the proposed shallow embedding significantly reduces the verification effort compared to an alternative approach based on a deep embedding.

• A preprint is available here.

Invited talk at the Royal Academy of Engineering, London on Tuesday, 21st of May 2024 arranged by Research Institute on Verified Trustworthy Software Systems (VeTSS).

Diego Marmsoler, “Secure Smart Contracts with Isabelle/Solidity”, VeTSS Annual Meeting, 2024 – YouTube

---

---

---

---

---