Fast and Reliable Formal Verification of Smart Contracts with the Move Prover

TL;DR

The paper introduces the Move Prover, a fast and reliable formal verification tool for Move smart contracts, enabling routine verification during development and integration testing with high efficiency.

Contribution

It presents the Move Prover with an expressive specification language and three key transformations that make formal verification practical for real-world blockchain code.

Findings

Verified entire Diem blockchain Move code in minutes

MVP can be run routinely by developers for smart contract verification

Successful verification of Diem framework changes before integration

Abstract

The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. MVP has an expressive specification language, and is fast and reliable enough that it can be run routinely by developers and in integration testing in a few minutes. Besides the simplicity of smart contracts and the Move language, three transformations are responsible for the practicality of MVP: (1) an alias-free memory model, (2) fine-grained invariant checking, and (3) monomorphization. The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by MVP in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub.