DROPS

Document

Tool Paper

DOI: 10.4230/OASIcs.FMBC.2025.12

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

Authors: Asad Ahmed and Diego Marmsoler

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{ahmed_et_al:OASIcs.FMBC.2025.12,
  author =	{Ahmed, Asad and Marmsoler, Diego},
  title =	{{Isabelle/Solidity: A Tool for the Verification of Solidity Smart Contracts}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{12:1--12:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.12},
  URN =		{urn:nbn:de:0030-drops-230393},
  doi =		{10.4230/OASIcs.FMBC.2025.12},
  annote =	{Keywords: Program Verification, Smart Contracts, Isabelle, Solidity}
}

Search Results

Documents authored by Ahmed, Asad

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

Abstract

Cite as

Thanks for your feedback!

Could not send message