PV3 ⊧ Move Proverchecks user-specified properties of Move smart contracts

Application domain/field

• Deductive verification
• Auto-active verification
• Blockchain
• Smart contracts

Type of tool

Auto-active verifier/deductive verifier

Expected input

Move source code annotated with specifications (pre-/postconditions).

Format:

• Source code: Move source code
• Specifications: own specification language

Expected output

Whether the specification holds or some kind of source-level diagnosis/error.

Internals

The Move Prover translates annotated Move source code to the Boogie intermediate language. Boogie then generates an SMT formula which can be checked using an SMT solver such as Z3 or CVC4. "Move" is a language for implementing transactions, i.e. smart contracts, on the Libra blockchain. The Move Prover seems to be an auto-active verifier though this is not mentioned in the paper.