\Section{Introduction}

The Move Prover (\MVP) is a formal verification tool for smart contracts that
intends to be used routinely during code development.  The verification finishes
fast and predictably, making the experience of running \MVP similar to the
experience of running compilers, linters, type checkers, and other development
tools.  Building a fast verifier is non-trivial, and in this paper, we would
like to share the most important engineering and architectural decisions that
have made this possible.

One factor that makes verification easier is applying it to smart contracts.
Smart contracts are easier to verify than conventional software for at least
three reasons: 1) they are small in code size, 2) they execute in a
well-defined, isolated environment, and 3) their computations are typically
sequential, deterministic, and have minimal interactions with the environment
(e.g., no explicit I/O operations).  At the same time, formal verification is
more appealing to the advocates for smart contracts because of the large
financial and regulatory risks that smart contracts may entail if misbehaved, as
evidenced by large losses that have occurred
already~\cite{CONTRACT_VERIFICATION,hacks-on-smart-contracts,hacks-on-compound}.

The other crucial factor to the success of \MVP is a tight coupling with the
\emph{Move} programming language~\cite{MOVE_LANG}.  Move is developed as part of
the Diem blockchain~\cite{DIEM} and is designed to be used with formal
verification from day one.  Move is currently co-evolving with \MVP.  The
language supports specifying pre-, post-, and aborts conditions of functions, as
well as invariants over data structures and over the content of the global
persistent memory (i.e., the state of the blockchain).  One feature that makes
verification harder is that quantification can be used
freely in specifications.

Despite this specification richness, \MVP is capable of verifying the full Move
implementation of the Diem blockchain (called the Diem
framework~\cite{DIEM_FRAMEWORK}) in a few minutes.  The framework provides
functionality for managing accounts and their interactions, including multiple
currencies, account roles, and rules for transactions.  It consists of about
8,800 lines of Move code and 6,500 lines of specifications (including comments
for both), which shows that the framework is extensively specified.  More
importantly, \emph{verification is fully automated and runs continuously with
  unit and integration tests}, which we consider a testament to the practicality
of the approach.  Running the prover in integration tests requires more than
speed: it requires reliability, because tests that work sometimes and fail or
time out other times are unacceptable in that context.

\MVP is a substantial and evolving piece of software that has been tuned and
optimized in many ways.  As a result, it is not easy to define exactly what
implementation decisions lead to fast and reliable performance.  However, we can
at least identify three major ideas that resulted in dramatic improvements in
speed and reliability since the description of an early prototype of
\MVP~\cite{MOVE_PROVER}:
\begin{itemize}
\item an \emph{alias-free memory model} based on Move's semantics, which are
  similar to the Rust programming language;
\item \emph{fine-grained invariant checking}, which ensures that invariants hold
  at every state, except when developer explicitly suspends them; and
\item monomorphization, which instantiates type parameters in Move's generic
  structures, functions, and specification properties.
\end{itemize}
The combined effect of all these improvements transformed a tool that worked,
but often exhibited frustrating, sometimes random~\cite{BUTTERFLY}, timeouts on
complex and especially on erroneous specifications, to a tool that almost always
completes in less than 30 seconds.  In addition, there have been many other
improvements, including a more expressive specification language, reducing false
positives, and error reporting.

The remainder of the paper first introduces the Move language and how \MVP is
used with it, then discusses the design of \MVP and the three main optimizations
above.  There is also an appendix that describes injection of function
specifications.

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