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

TL;DR

This paper compares formal verification approaches in Solidity and Move, analyzing how language design influences verification effectiveness and reviewing current tools through practical use cases.

Contribution

It provides a comparative analysis of verification challenges and tools for Solidity and Move, highlighting design impacts and evaluating state-of-the-art solutions.

Findings

Move's design facilitates easier verification due to its security focus.

Verification tools for Solidity face challenges from language semantics.

Move Prover demonstrates effective verification on key use cases.

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.