Deep dive into the Move Prover

May 10, 2025

1. Introduction & Importance of Formal Verification

Smart contracts often handle valuable assets with no safety nets – once deployed, their code executes autonomously and irreversibly. This high-stakes environment makes correctness paramount. Formal verification offers a mathematical approach to prove program correctness for all possible inputs and states, unlike traditional testing which can only catch some bugs but never prove their absence. In formal verification, we model a system (hardware or software) as a finite state machine (FSM) with state variables and transitions. Each unique combination of state variable values represents a state, and each operation (or function call) is a state transition. For even moderately complex systems, the number of possible states grows exponentially with the number of state variables a phenomenon known as the state-space explosion problem . This exponential blow-up makes exhaustive testing infeasible, whereas formal methods use symbolic reasoning to explore all states simultaneously.

State-Space vs. Testing: Consider a simple token contract with state variables tracking each account’s balance and the total supply. Even if each balance is just a 64-bit integer, the space of possible states is astronomically large. A few example transitions are illustrated below:

As more accounts and operations are introduced, the state graph branches out explosively. Traditional simulation/testing would cover only a tiny fraction of possible transitions (following specific paths like the one above), potentially missing corner case bugs. By contrast, formal verification explores all paths symbolically to ensure no violation occurs in any reachable state. Formal verification overcomes this limitation by proving properties hold in all cases, not just observed ones. This exhaustive guarantee is invaluable for critical systems.

In practice, formal verification tools often combine mathematical logic and solvers to tackle the state explosion implicitly. They translate the program and desired properties into logical formulas and use satisfiability modulo theories (SMT) solvers to check those formulas. If the solver finds no counterexample, the property is proven to hold for all states; if it finds a satisfying assignment violating the property, that provides a counterexample trace

Why is Move Secure?

Securing smart contracts is vital in the blockchain sector, as even a small vulnerability can result in disastrous consequences due to the significant value of the assets at stake. As such, selecting an appropriate programming language is essential in ensuring the reliability and security of smart contracts.

The primary goal of safety in smart contract languages is to understand the contract's inner workings and prevent potential problems arising from bugs or security flaws, such as the reentrancy issue, a common problem in smart contracts where multiple self-calls are executed, causing a drain of funds.

The Move language equips developers with valuable tools like the Move prover, which aids in verifying the correct operation of their contracts.

Move Prover is a formal verification tool. Formal verification is the process of using mathematical and logical methods to prove that a program meets its specifications

Other security features of Move:

Linear Type System: Move features a robust linear type system that guarantees specific access and modification patterns for data structures within a Move program. This aids in avoiding unforeseen behaviours.
Visibility System: Move incorporates a solid visibility system, enabling developers to precisely manage data access, modification, and storage within a blockchain. This assists in preventing unauthorised access to sensitive information or code.
Modularity: Move is highly modular, enabling resource ownership by modules, which means that only the module responsible for defining a resource can modify it. This establishes a secure data structure, as only authorized modules can access and modify the information within.

Formal vs. Simulation Workflow: The difference between simulation and formal methods can be visualized as follows:

In summary, simulation (even with fuzzing) explores specific paths in the state space, whereas formal verification proves properties over the entire state space of the contract. This makes formal verification particularly powerful for smart contracts, where security is critical and failures can lead to “massive amounts of funds being stolen or made inaccessible”theory.stanford.edu. Formal methods can catch logical and security issues that might only occur in rare conditions which tests could easily miss.

Token Contract Basics

To ground the discussion, let’s consider a fungible token contract (similar to an ERC-20 in Ethereum, but implemented in Move). Such a contract typically manages a resource representing balances of a coin for each user, and provides functions to mint, transfer, and burn tokens. We will outline the basic behavior of each function and the key properties that a formal specification (using Move Prover) should verify:

Mint: Creates new tokens and adds them to a specified account’s balance (increasing the total supply).
- Authorization: Only certain privileged entities should be able to mint. In Move, this can be enforced by requiring a capability or witness resource held only by authorized accounts (e.g. the module itself or a designated MintCapability).
- Post-condition: The target account’s balance increases by the minted amount, and the global token supply increases by exactly that amount. No other account balances change.
- Supply Invariant: Mint is one of the only operations that can increase total supply (the other being resource creation via module initialization). We expect an invariant that total supply after mint = total supply before + minted amount.
- Preconditions/Abort conditions: The contract might require that the target account already has a balance resource published (or handle creation of one). If such a precondition isn’t met, the function should abort (and the spec should specify this abort condition). For example, attempting to mint to an address that hasn’t been initialized with a balance resource should trigger an abort condition in the spec.
Transfer: Moves tokens from one account to another.
- Precondition: The sender must have at least the amount to transfer (no overdrafts). This can be specified with a requires clause or as an aborts_if sender_balance < amount in the spec.
- Post-condition: On successful transfer, the sender’s balance decreases by amount and the recipient’s balance increases by amount. The sum of the two balances remains constant, and importantly the total supply remains unchanged (tokens are neither created nor destroyed, just relocated).
- Conservation: A key property is balance conservation – the sum of all balances in the system should remain the same before and after a transfer. In other words, transfers do not affect the global coin supply, they only redistribute existing tokens.
- Edge cases: If the contract allows transferring to a new account that has no balance resource, it might automatically publish a new balance resource for the recipient (or abort if it cannot). The specification should account for self-transfers as well (transferring from an account to itself should be either a no-op or disallowed). The Move Prover can verify that even in these edge cases, no tokens are lost or gained unexpectedly.
Burn: Destroys tokens from an account’s balance, reducing the total supply.
- Authorization: Depending on the design, burning might be restricted (perhaps only the token holder can burn their own tokens, or only an admin can trigger burns). The spec should enforce that only allowed entities can burn. In Move, this could be done by requiring a witness (similar to mint) or simply by the logic of the function (e.g., a user can burn from their own balance but not someone else’s).
- Post-condition: The account’s balance is decreased by the burn amount and the total supply is decreased by exactly that amount. No other balances change. If an account burns all its tokens, often the balance resource might be deleted – the spec can verify that the resource deletion only happens when the balance hits zero (if relevant).
- Supply Invariant: Burn is the complementary operation to mint. It should be the only operation (besides possibly explicit self-destruct mechanisms) that decreases the total token supply. An invariant can specify that total supply after burn = total supply before – burned amount.
- Preconditions/Abort: The burner must have at least the amount being burned (no burning more than one’s balance). If not, the operation aborts (which the spec should capture with an aborts_if amount > balance condition).

In a well-designed token contract, these functions uphold fundamental correctness properties, such as ensuring no creation or destruction of tokens except through minting or burning, no transfer of more tokens than are available, and proper authorization. Formal specifications can be used to encode these properties. For example, a global invariant might state that "the sum of the value fields of all Coin resources in the system equals the total_supply value stored in the central resource." This invariant holds true when every mint and burn operation correctly updates total_supply, and every transfer operation leaves total_supply unchanged. The Move Prover can automatically verify that all code paths in mint, transfer, and burn functions preserve this invariant. Indeed, the Move language encourages designing supply tracking in this manner (for example, Aptos’s standard Coin module maintains a global TotalSupply resource). By verifying this invariant once, all transactions using these functions are guaranteed to maintain token conservation.

In summary, the Move Prover allows us to prove properties like “tokens cannot be created or destroyed except by authorized calls to mint/burn” and “balances are correctly debited/credited on transfer” for all users and all execution paths. These are exactly the kinds of logic and security issues that have plagued smart contracts in the past (e.g., bugs that accidentally minted extra tokens or allowed stealing funds). By formally verifying a token contract’s functions, we gain high assurance that such bugs are eliminated from the design.

Specification Setup in Move Prover

The Move Prover uses the Move Specification Language (MSL) to let developers write formal specifications alongside Move code. An MSL specification is typically written in special spec blocks (or in separate .move specification files) and consists of preconditions, postconditions, and invariants that describe the intended behavior of the code. These specifications do not execute at runtime, but the prover uses them to verify the code’s correctness. Key elements of writing specifications include:

Preconditions: These describe what must be true before a function is called. In MSL, one can use requires clauses to state assumptions about inputs or state, and aborts_if clauses to describe conditions under which the function is allowed to abort. For example, for a transfer function, one might write: requires amount <= old_balance (ensuring the caller has enough funds), or aborts_if !exists<Balance<CoinType>>(to) (the function will abort if the recipient’s account has no Balance resource published). A subtle difference between requires and aborts_if is that requires specifies a precondition that callers must satisfy (it won’t even consider executions that violate it), whereas aborts_if documents an internal condition that triggers an abort in the callee. In other words, requires shifts the burden to the caller (and the prover will check at each call site that the condition was met), while aborts_if indicates the function itself will terminate if a condition holds (without necessarily forcing the caller to avoid it). In practice, one often uses both: e.g., a requires amount <= balance and an aborts_if amount > balance – the former helps prove correct usage by internal callers, the latter accounts for external calls that violate the precondition by specifying the outcome (an abort).
Postconditions: These describe what must be true after successful execution of a function (when it does not abort). In MSL, ensures clauses specify relationships between the post-state and the pre-state. For example, for the mint function we might write: ensures global<Balance<CoinType>>(mint_addr).value == old(global<Balance<CoinType>>(mint_addr).value) + amount; to state that the target account’s balance is increased by amount The keyword old(...) is used to refer to the value of an expression in the pre-state (before the function executed), allowing us to formally relate pre- and post-state. We can have multiple ensures clauses to capture different aspects of the post-state. For instance, another postcondition could ensure the total supply increased accordingly, and another could ensure no other account’s balance changed. If a function can abort, postconditions typically describe the guarantees when it doesn’t abort (one can use the construct ensures [ok] ... in MSL to explicitly tie postconditions to the successful execution case if needed).
Invariants: Invariants are properties that should hold in every reachable state of the program or whenever certain conditions are met. Move Prover supports several kinds of invariants:
- Module invariants / global invariants: Properties that should hold whenever the blockchain is at rest (e.g., after any transaction). For example, an invariant could assert that the total supply equals the sum of all account balances system-wide, as mentioned earlier. You can declare such invariants in a spec module { ... } block. When verifying, the prover will check that every transaction (or function in the module) preserves these invariants.
- Resource/struct invariants: Properties that relate the fields of a resource. For example, one might enforce that a Vault resource’s locked flag is false whenever balance > 0, etc. These are declared with spec struct S { invariant ... } and apply to every instance of that struct.
- Function invariants: MSL even allows invariants that hold at specific points in a procedure or across loop iterations (loop invariants), but for many smart contracts these are less common unless verifying complex algorithmic logic.

As an example, if we maintain a special global resource Info with a field total_value tracking total supply, we could write:

spec module {

invariant [global] global<Info>().total_value == Sum<Balance<CoinType>>();

}

Where Sum<Balance<CoinType>>() is a conceptual helper that sums all balances (this can be achieved via a spec function or spec variable as described below). The [global] label indicates it’s a global invariant that should hold after any transaction. The Move Prover will then ensure every call to mint, burn, transfer (or any other function in the module) leaves this invariant true – catching any oversight where, say, someone forgets to update total_value during mint/burn.
Specification Variables (Ghost Variables): MSL allows introducing specification variables, also called ghost variables, which do not exist in the actual runtime but are used in specifications to track conceptual state . For example, one might declare a spec variable to represent the “sum of all coins in the system” and then use invariants to update this variable on mints/burns and assert its boundaries. Ghost variables are never compiled into bytecode and carry no runtime cost; they exist purely to aid verification by making certain state relationships explicit. In other smart contract verification tools, ghost state is often used to track data across multiple transactions . In Move Prover, their use is a bit more limited since the prover’s analysis is mostly per-transaction (local), but they can still be helpful for structuring proofs. For instance, instead of writing a complex sum expression in every invariant, one could maintain a ghost variable total_coins that is updated whenever a coin is created or destroyed, and then simply invariant that total_coins == global<Info>().total_value. The Aptos documentation illustrates this by introducing a global sum_of_counters: num ghost variable and specifying pack and unpack invariants to update it whenever a Counter resource is created or modified
Common Specification Patterns: Move specs often follow Hoare logic style patterns (pre/postconditions). Some common patterns include:
- Using the result of a function call in postconditions. If a function returns a value, you can refer to result (or specify a name for the returned value) in the ensures clause to relate it to inputs.
- Framing and modifies clauses: In Move, one can specify which global resources a function is allowed to modify. The prover ensures no other parts of the state are changed. For example, modifies Balance<CoinType>{ account } could assert that only the Balance resource of the given account may be mutated. This helps catch unintended side-effects.
- Aborts codes: aborts_with can specify particular error codes that a function may throw. The prover will then ensure no other abort conditions occur.
- Utilizing schemas to avoid repetition. Schemas group common specification snippets that can be included in multiple spec blocks . For example, you might define a schema Conservation that includes a set of ensures clauses to check total supply before and after an operation, and then include that schema in both the mint and burn spec blocks (with appropriate substitutions). This promotes consistency and reuse in specs for similar functions.

Writing specifications requires a careful consideration of what the code should do in every scenario. It can be an iterative process – one writes an initial spec, runs the prover, and if the prover finds a counterexample or reports an overlooked case, the spec (or code) is refined. Indeed, writing correct specs can be as challenging as writing correct code. However, the benefit is a much higher confidence in the smart contract’s reliability. The Move Prover checks these specifications automatically against the implementation, as we will see next.

Running the Move Prover: A Guide with Commands

To properly verify your Move modules, you’ll use a set of commands and flags that help tailor the prover’s behavior and allow you to focus on specific modules or properties. Here’s how to get started, along with the commands you’ll need at each step:

1. Setting Up the Environment

Before running the prover, ensure you have the Move CLI installed.
Check that the move command is accessible from your terminal. If you’ve just set up your environment, confirm the installation with:
move --version

2. Preparing the Package

Your Move code should be part of a Move package. If you don’t have one yet, create one:
move package init my_project
Once you have a Move.toml file and your modules are organized under sources/, you’re ready to proceed.

3. Adding Specifications

Write specifications in spec blocks directly in your .move files. These blocks use keywords like requires, ensures, and aborts_if. For example:

spec module {

invariant [global] total_supply == sum_of_all_balances();

}

‍

spec fun transfer {

requires sender_balance >= amount;

ensures sender_balance == old(sender_balance) - amount;

ensures recipient_balance == old(recipient_balance) + amount;

}

4. Running the Prover

To verify all modules in your package:
move prove
To verify a specific module, use the --filter or -f flag. For example, to verify only MyToken.move:
move prove --filter MyToken
To target a particular specification block or function:
move prove --filter MyModule::my_function

5. Adjusting Prover Behavior

To increase verbosity and see detailed prover output:
move prove --verbose
To display all failing assertions and proofs:
move prove --show-warnings
If you need a more detailed intermediate representation, you can dump the Boogie code used by the prover:
move prove --dump-bytecode
To specify a different backend SMT solver, you can adjust the configuration in Move.toml.

6. Debugging and Rerunning

When you encounter a failing specification, refine your spec blocks or code logic. For example, if a postcondition fails, check the ensures clause and the function’s state transitions.
After making changes, run the prover again to verify:
move prove

7. Continuous Integration

Include the prover in your CI pipeline by running:
move prove --ci
This ensures every code change is verified before merging.

By following these steps, you’ll have a reliable process for using the Move Prover to maintain the integrity of your smart contracts.

Conclusion & Next Steps

The Move Prover significantly enhances smart contract security and correctness by integrating formal verification directly into the development process. It guarantees critical safety properties, preventing issues such as unauthorized token minting or invariant breaches, and clarifies intended behaviors through explicit specifications, serving as accurate and always current documentation. Furthermore, it provides immediate automated feedback on code correctness, reducing the need for extensive manual audits and accelerating development cycles.

Future improvements for the Move Prover include verifying liveness properties to ensure certain events eventually occur, enhancing compositional and modular verification for scalable system-wide correctness, and deeper integration with developer tools and continuous integration pipelines, including automated test generation and enriched CI reports. Additionally, expanding formal verification to include resource constraints, such as predictable gas consumption and storage usage, is an important next step.

In comparison to hardware-focused tools like JasperGold or Synopsys Formality, Move Prover is more akin to software verification tools like Dafny or Frama-C, providing user-driven formal verification specifically tailored to smart contracts. By incorporating the Move Prover into development workflows and CI pipelines, developers can confidently build secure and reliable blockchain applications, contributing to a future where critical infrastructure is secure by construction.