Formal verification in Solidity and Move: insights from a comparative analysis

• DOI: 10.48550/arxiv.2502.13929
• Publication Date: 2025-02-19
• Authors: Massimo Bartoletti; Silvia Crafà; E. Lipparini
• Keywords: Solidity

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