\Section{Conclusion}

We described key aspects of the Move prover (\MVP), a tool for formal
verification of smart contracts written in the Move language. \MVP has been
successfully used to verify large parts of the Diem framework, and is used in
continuous integration in production. The specification language is expressive,
specifically by the powerful concept of global invariants.  We described key
implementation techniques which (as confirmed by our benchmarks) contributed to
the scalability of \MVP. One of the main areas of our future research is to
improve specification productivity and reduce the effort of reading and writing
specs, as well as to continue to improve speed and predictability of
verification.



%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: