DROPS

Document

DOI: 10.4230/OASIcs.FMBC.2025.3

Formal Verification in Solidity and Move: Insights from a Comparative Analysis

Authors: Massimo Bartoletti, Silvia Crafa, and Enrico Lipparini

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

Abstract

Formal verification plays a crucial role in making smart contracts safer, being able to find bugs or to guarantee their absence, as well as checking whether the business logic is correctly implemented. For Solidity, even though there already exist several mature verification tools, the semantical quirks of the language can make verification quite hard in practice. Move, on the other hand, has been designed with security and verification in mind, and it has been accompanied since its early stages by a formal verification tool, the Move Prover. In this paper, we investigate through a comparative analysis: 1) how the different designs of the two contract languages impact verification, and 2) what is the state-of-the-art of verification tools for the two languages, and how do they compare on three paradigmatic use cases. Our investigation is supported by an open dataset of verification tasks performed in Certora and in the Aptos Move Prover.

Cite as

Massimo Bartoletti, Silvia Crafa, and Enrico Lipparini. Formal Verification in Solidity and Move: Insights from a Comparative Analysis. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bartoletti_et_al:OASIcs.FMBC.2025.3,
  author =	{Bartoletti, Massimo and Crafa, Silvia and Lipparini, Enrico},
  title =	{{Formal Verification in Solidity and Move: Insights from a Comparative Analysis}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{3:1--3:18},
  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.3},
  URN =		{urn:nbn:de:0030-drops-230302},
  doi =		{10.4230/OASIcs.FMBC.2025.3},
  annote =	{Keywords: Smart contracts, Solidity, Move, Verification, Blockchain}
}

Search Results

Documents authored by Lipparini, Enrico

Formal Verification in Solidity and Move: Insights from a Comparative Analysis

Abstract

Cite as

Thanks for your feedback!

Could not send message