  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.
