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

TL;DR

This paper compares formal verification in Solidity and Move to understand how language design shapes verifiability and tooling, using three paradigmatic use cases and an open dataset of tasks for Certora and Move Prover. It finds that Move’s resource-centric semantics generally ease verification of asset preservation and ownership, while Solidity requires extensive low-level specifications and assumptions. The study also contrasts the verification capabilities of Certora Prover and Move Prover, highlighting broader property support for Certora and gaps in Move Prover for certain high-level properties. These insights inform developers and tool authors about language choices and areas for improving verification tooling, with an openly available dataset to foster further research.

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.