Document Open Access Logo

Isabelle/Solidity: A Tool for the Verification of Solidity Smart Contracts (Tool Paper)

Authors Asad Ahmed , Diego Marmsoler

PDF

File

Thumbnail PDF
PDF
OASIcs.FMBC.2025.12.pdf
  • Filesize: 0.68 MB
  • 9 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
Keywords
  • Program Verification
  • Smart Contracts
  • Isabelle
  • Solidity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Smart contracts are an important innovation in Blockchain which allow to automate financial transactions. Every day, hundreds of thousands of new contracts are deployed managing millions of dollars' worth of transactions. Thus, bugs in smart contracts may lead to high financial losses and it is important to get them right before deploying them to the Blockchain. To address this problem we developed Isabelle/Solidity, a tool for the verification of smart contracts in Isabelle. The tool is implemented as a definitional extension for the Isabelle proof assistant and thus complements existing tools in this area which are mostly based on axiomatic approaches. In this paper we describe Isabelle/Solidity and demonstrate it by verifying a casino contract from the VerifyThis long term verification challenge.

Cite As Get BibTex

Asad Ahmed and Diego Marmsoler. Isabelle/Solidity: A Tool for the Verification of Solidity Smart Contracts (Tool Paper). In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 12:1-12:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/OASIcs.FMBC.2025.12

Author Details

Asad Ahmed
  • University of Exeter, UK
Diego Marmsoler
  • 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. Wolfgang Ahrendt. Welcome to Fabulous Las Contract Blockchain, December 2024. URL: https://web.archive.org/web/20241209135636/https://verifythis.github.io/02casino/.
  2. Wolfgang Ahrendt and Richard Bubel. Functional Verification of Smart Contracts via Strong Data Integrity. In Leveraging Applications of Formal Methods, Verification and Validation: Applications: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III 9, pages 9-24. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-61467-6_2.
  3. Franck Cassez, Joanne Fuller, and Horacio Mijail Anton Quiles. Deductive Verification of Smart Contracts with Dafny. In Jan Friso Groote and Marieke Huisman, editors, Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, Proceedings, volume 13487 of Lecture Notes in Computer Science, pages 50-66. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15008-1_5.
  4. Franck Cassez, Joanne Fuller, and Horacio Mijail Anton Quiles. Deductive Verification of Smart Contracts with Dafny. Int. J. Softw. Tools Technol. Transf., 26(2):131-145, 2024. URL: https://doi.org/10.1007/S10009-024-00738-1.
  5. CipherTrace. Cryptocurrency Crime and Anti-money Laundering Report. Technical report, mastercard, 2021. Google Scholar
  6. David Cock, Gerwin Klein, and Thomas Sewell. Secure Microkernels, State Monads and Scalable Refinement. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, pages 167-182. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_16.
  7. Robert DeLine and K Rustan M Leino. Boogiepl: A Typed Procedural Language for Checking Object-oriented Programs. Technical report, Citeseer, 2005. Google Scholar
  8. Edsger W. Dijkstra. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM, 18(8):453-457, August 1975. URL: https://doi.org/10.1145/360933.360975.
  9. Etherscan. Ethereum Daily Deployed Contracts Chart, February 2025. URL: https://etherscan.io/chart/deployed-contracts.
  10. Ákos Hajdu and Dejan Jovanović. solc-verify: A Modular Verifier for Solidity Smart Contracts. In Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Revised Selected Papers 11, pages 161-179. Springer, 2020. Google Scholar
  11. Alexander Krauss. Recursive Definitions of Monadic Functions. Electronic Proceedings in Theoretical Computer Science, 43:1-13, 2010. URL: https://doi.org/10.4204/eptcs.43.1.
  12. Diego Marmsoler, Asad Ahmed, and Achim D Brucker. Secure Smart Contracts with Isabelle/Solidity. In International Conference on Software Engineering and Formal Methods, pages 162-181. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-77382-2_10.
  13. Diego Marmsoler and Achim D. Brucker. A Denotational Semantics of Solidity in Isabelle/HOL. In Radu Calinescu and Corina S. Păsăreanu, editors, Software Engineering and Formal Methods, pages 403-422, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-92124-8_23.
  14. Diego Marmsoler and Achim D. Brucker. Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL. Form. Asp. Comput., 37(2), March 2025. URL: https://doi.org/10.1145/3700601.
  15. Diego Marmsoler and Billy Thornton. SSCalc: A Calculus for Solidity Smart Contracts. In Carla Ferreira and Tim A. C. Willemse, editors, Software Engineering and Formal Methods, pages 184-204, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-47115-5_11.
  16. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, 2002. Google Scholar
  17. Philip Wadler. Monads for Functional Programming. In Manfred Broy, editor, Program Design Calculi, pages 233-264. Springer, 1993. URL: https://doi.org/10.1007/978-3-662-02880-3_8.
  18. Ycharts. Ethereum Transactions Per Day, February 2025. URL: https://ycharts.com/indicators/ethereum_transactions_per_day.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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