Move Prover Expert

Purpose

Provide deep expertise on the Move Prover - a formal verification tool that mathematically proves correctness properties of Move smart contracts. The Prover uses the Move Specification Language (MSL) to express properties and verifies them using SMT solvers (Z3, CVC5).

When to Use

Auto-invoke when users mention:

• Move Prover - formal verification, prove, verification
• Specifications - spec blocks, spec module, spec fun
• Properties - invariants, preconditions, postconditions
• MSL Keywords - ensures, requires, aborts_if, modifies, emits
• Advanced - quantifiers, schema, global invariants, pragma
• Verification - soundness, completeness, verification errors
• Debugging - proof failures, counterexamples, timeout

Move Prover Overview

What is the Move Prover?

The Move Prover is a formal verification tool that:

• Mathematically proves contract properties hold for ALL possible inputs
• Uses SMT (Satisfiability Modulo Theories) solvers
• Finds bugs that testing might miss
• Provides mathematical guarantees of correctness
• Generates counterexamples for failed proofs

Why Use the Move Prover?

Testing vs Verification:

// Testing: Checks specific inputs
#[test]
fun test_transfer() {
    transfer(alice, bob, 100);  // Only tests this one case
}

// Verification: Proves for ALL inputs
spec transfer {
    ensures sender_balance == old(sender_balance) - amount;
    ensures recipient_balance == old(recipient_balance) + amount;
    // Proven for ALL possible values of amount, sender, recipient!
}

Benefits:

• ✅ Catches edge cases testing misses
• ✅ Proves absence of integer overflow/underflow
• ✅ Guarantees invariants always hold
• ✅ Verifies access control is sound
• ✅ Documents intended behavior formally

Specification Language (MSL) Basics

Spec Blocks

module 0x1::counter {
    struct Counter has key {
        value: u64
    }

    public fun increment(addr: address) acquires Counter {
        let counter = borrow_global_mut<Counter>(addr);
        counter.value = counter.value + 1;
    }

    spec increment {
        // Specification for increment function
        requires exists<Counter>(addr);
        ensures global<Counter>(addr).value == old(global<Counter>(addr).value) + 1;
    }
}

Spec Module

spec module {
    // Module-level specifications
    pragma verify = true;  // Enable verification for this module
    pragma aborts_if_is_strict;  // Require complete abort specifications
}

Core Specification Constructs

1. Preconditions -

requires

Conditions that must be true when function is called:

public fun withdraw(account: &signer, amount: u64) acquires Balance {
    let addr = signer::address_of(account);
    let balance = borrow_global_mut<Balance>(addr);
    balance.coins = balance.coins - amount;
}

spec withdraw {
    requires exists<Balance>(signer::address_of(account));
    requires global<Balance>(signer::address_of(account)).coins >= amount;
    // Function only called when these conditions are true
}

Multiple requires:

spec withdraw {
    requires exists<Balance>(addr);
    requires global<Balance>(addr).coins >= amount;
    requires amount > 0;
    requires amount <= MAX_WITHDRAW;
}

2. Postconditions -

ensures

Conditions that must be true after function executes:

public fun transfer(from: address, to: address, amount: u64) acquires Balance {
    let from_balance = borrow_global_mut<Balance>(from);
    from_balance.coins = from_balance.coins - amount;

    let to_balance = borrow_global_mut<Balance>(to);
    to_balance.coins = to_balance.coins + amount;
}

spec transfer {
    // Postconditions
    ensures global<Balance>(from).coins == old(global<Balance>(from).coins) - amount;
    ensures global<Balance>(to).coins == old(global<Balance>(to).coins) + amount;

    // Conservation of funds
    ensures global<Balance>(from).coins + global<Balance>(to).coins ==
            old(global<Balance>(from).coins + global<Balance>(to).coins);
}

3. Abort Conditions -

aborts_if

Specify when function should abort:

const ERROR_INSUFFICIENT_BALANCE: u64 = 1;
const ERROR_NOT_INITIALIZED: u64 = 2;

public fun withdraw(addr: address, amount: u64) acquires Balance {
    assert!(exists<Balance>(addr), ERROR_NOT_INITIALIZED);
    let balance = borrow_global_mut<Balance>(addr);
    assert!(balance.coins >= amount, ERROR_INSUFFICIENT_BALANCE);
    balance.coins = balance.coins - amount;
}

spec withdraw {
    aborts_if !exists<Balance>(addr) with ERROR_NOT_INITIALIZED;
    aborts_if global<Balance>(addr).coins < amount with ERROR_INSUFFICIENT_BALANCE;

    // These are the ONLY ways this function can abort
}

Conditional aborts:

spec withdraw {
    // Only aborts if these conditions are met
    aborts_if !exists<Balance>(addr);
    aborts_if exists<Balance>(addr) && global<Balance>(addr).coins < amount;
}

4. Abort Specification Completeness

spec module {
    pragma aborts_if_is_strict;
    // Now MUST specify all abort conditions
}

public fun transfer(from: address, to: address, amount: u64) acquires Balance {
    assert!(exists<Balance>(from), 1);
    assert!(exists<Balance>(to), 2);
    assert!(global<Balance>(from).coins >= amount, 3);

    // ... transfer logic
}

spec transfer {
    // Must list ALL abort conditions
    aborts_if !exists<Balance>(from);
    aborts_if !exists<Balance>(to);
    aborts_if global<Balance>(from).coins < amount;
    // Missing any condition = verification error
}

5. Modified Resources -

modifies

Specify which global resources are modified:

spec withdraw {
    modifies global<Balance>(addr);
    // Only Balance at addr is modified, nothing else
}

spec transfer {
    modifies global<Balance>(from);
    modifies global<Balance>(to);
    // Only these two resources are modified
}

6. Event Emission -

emits

Specify events that should be emitted:

#[event]
struct TransferEvent has drop, store {
    from: address,
    to: address,
    amount: u64,
}

public fun transfer(from: address, to: address, amount: u64) {
    // ... transfer logic
    event::emit(TransferEvent { from, to, amount });
}

spec transfer {
    emits TransferEvent {
        from: from,
        to: to,
        amount: amount
    } to @my_module;
}

Advanced Features

The

old()

Operator

Access values from before function execution:

spec increment {
    ensures global<Counter>(addr).value == old(global<Counter>(addr).value) + 1;
    //                                      ^^^ value before function ran
}

spec swap {
    ensures a == old(b);
    ensures b == old(a);
}

Global State Access

spec withdraw {
    // Access global state
    let balance = global<Balance>(addr);
    let initial_coins = old(global<Balance>(addr).coins);

    ensures balance.coins == initial_coins - amount;
}

Let Bindings in Specs

spec transfer {
    let from_balance = global<Balance>(from);
    let to_balance = global<Balance>(to);
    let from_initial = old(from_balance.coins);
    let to_initial = old(to_balance.coins);

    ensures from_balance.coins == from_initial - amount;
    ensures to_balance.coins == to_initial + amount;
}

Conditional Ensures

spec withdraw {
    ensures result == true ==> global<Balance>(addr).coins == old(global<Balance>(addr).coins) - amount;
    ensures result == false ==> global<Balance>(addr).coins == old(global<Balance>(addr).coins);
}

Quantifiers

Universal Quantification -

forall

Prove property holds for ALL values:

spec module {
    // For all addresses, if Balance exists, coins >= 0
    invariant forall addr: address:
        exists<Balance>(addr) ==> global<Balance>(addr).coins >= 0;
}

spec transfer {
    // Conservation: total supply unchanged
    ensures forall addr: address where addr != from && addr != to:
        global<Balance>(addr).coins == old(global<Balance>(addr).coins);
}

Existential Quantification -

exists

Prove property holds for AT LEAST ONE value:

spec module {
    // There exists at least one admin
    invariant exists addr: address:
        exists<AdminCap>(addr);
}

Range Quantifiers

spec module {
    // For all indices in vector, value is positive
    invariant forall i in 0..len(balances):
        balances[i] > 0;
}

spec sum_vector {
    ensures result == sum(0..len(v), |i| v[i]);
}

Global Invariants

Module Invariants

Properties that hold for entire module:

spec module {
    // Global supply never exceeds max
    invariant [global]
        forall addr: address:
            exists<Supply>(addr) ==>
            global<Supply>(addr).total <= MAX_SUPPLY;

    // Conservation of total supply
    invariant [global]
        sum_of_balances() == global<TotalSupply>(@admin).value;
}

Struct Invariants

Properties that always hold for a struct:

struct Balance has key {
    coins: u64,
    locked: u64,
}

spec Balance {
    // Available coins >= locked coins
    invariant coins >= locked;

    // Locked amount is multiple of lock unit
    invariant locked % LOCK_UNIT == 0;
}

Update Invariants

Properties about state changes:

spec module {
    // Balance can only increase or decrease, never become negative
    invariant update [global]
        forall addr: address:
            old(exists<Balance>(addr)) ==>
            exists<Balance>(addr) &&
            global<Balance>(addr).coins <= old(global<Balance>(addr).coins) + MAX_DEPOSIT;
}

Schema - Reusable Specifications

Defining Schema

spec schema BalanceExists {
    addr: address;
    requires exists<Balance>(addr);
}

spec schema SufficientBalance {
    addr: address;
    amount: u64;
    requires global<Balance>(addr).coins >= amount;
}

spec schema BalanceNotChanged {
    addr: address;
    ensures global<Balance>(addr).coins == old(global<Balance>(addr).coins);
}

Using Schema

spec withdraw {
    include BalanceExists;
    include SufficientBalance;
}

spec deposit {
    include BalanceExists { addr: recipient };
}

// Apply to multiple functions
spec withdraw, transfer, burn {
    include BalanceExists;
}

Schema with Variables

spec schema TransferEnsures {
    from: address;
    to: address;
    amount: u64;

    ensures global<Balance>(from).coins == old(global<Balance>(from).coins) - amount;
    ensures global<Balance>(to).coins == old(global<Balance>(to).coins) + amount;
}

spec transfer {
    include TransferEnsures;
}

Schema Composition

spec schema ValidTransfer {
    from: address;
    to: address;
    amount: u64;

    include BalanceExists { addr: from };
    include BalanceExists { addr: to };
    include SufficientBalance { addr: from };
}

spec transfer {
    include ValidTransfer;
    include TransferEnsures;
}

Helper Functions

Spec Functions

Define helper functions for specifications:

spec module {
    // Sum of all balances
    fun sum_of_balances(): u64 {
        sum(all_addresses(), |addr| {
            if (exists<Balance>(addr)) {
                global<Balance>(addr).coins
            } else {
                0
            }
        })
    }

    // Check if address is admin
    fun is_admin(addr: address): bool {
        exists<AdminCap>(addr)
    }

    // Get total supply
    fun total_supply(): u64 {
        global<Supply>(@admin).total
    }
}

spec transfer {
    // Conservation using helper function
    ensures sum_of_balances() == old(sum_of_balances());
}

Spec-Only Functions

Functions only used in specifications:

spec module {
    fun balance_of(addr: address): u64 {
        if (exists<Balance>(addr)) {
            global<Balance>(addr).coins
        } else {
            0
        }
    }
}

spec transfer {
    ensures balance_of(from) == old(balance_of(from)) - amount;
    ensures balance_of(to) == old(balance_of(to)) + amount;
}

Pragma Directives

Verification Control

spec module {
    // Enable/disable verification for module
    pragma verify = true;

    // Timeout for each function (seconds)
    pragma timeout = 60;

    // Random seed for solver
    pragma random_seed = 123;

    // Require strict abort specs
    pragma aborts_if_is_strict;

    // Require partial abort specs (default)
    pragma aborts_if_is_partial;
}

Function-Specific Pragmas

spec complex_function {
    pragma verify = false;  // Skip verification of this function
}

spec timeout_function {
    pragma timeout = 120;  // Increase timeout to 2 minutes
}

spec opaque_function {
    pragma opaque;  // Don't inline this function in proofs
}

Solver Configuration

spec module {
    // Use specific SMT solver
    pragma solver = "z3";  // or "cvc5"

    // Increase memory limit
    pragma memory_limit = 16384;  // MB

    // Verification condition generation
    pragma verify_duration_estimate = 300;
}

Advanced Patterns

Pattern 1: Access Control Verification

struct AdminCap has key {}

public fun admin_only_function(admin: &signer) acquires AdminCap {
    let admin_addr = signer::address_of(admin);
    assert!(exists<AdminCap>(admin_addr), ERROR_NOT_ADMIN);
    // ... admin operations
}

spec admin_only_function {
    // Precondition: caller must have AdminCap
    requires exists<AdminCap>(signer::address_of(admin));

    // Abort condition
    aborts_if !exists<AdminCap>(signer::address_of(admin));
}

spec module {
    // Global invariant: only one admin exists
    invariant [global]
        forall addr1: address, addr2: address:
            exists<AdminCap>(addr1) && exists<AdminCap>(addr2) ==> addr1 == addr2;
}

Pattern 2: Supply Conservation

spec module {
    // Helper: sum of all balances
    fun total_balance(): u64 {
        sum(all_addresses(), |addr| {
            if (exists<Balance>(addr)) {
                global<Balance>(addr).coins
            } else {
                0
            }
        })
    }

    // Invariant: total balance equals total supply
    invariant [global]
        total_balance() == global<TotalSupply>(@deployer).value;
}

spec mint {
    // Minting increases total supply
    ensures global<TotalSupply>(@deployer).value ==
            old(global<TotalSupply>(@deployer).value) + amount;
}

spec burn {
    // Burning decreases total supply
    ensures global<TotalSupply>(@deployer).value ==
            old(global<TotalSupply>(@deployer).value) - amount;
}

spec transfer {
    // Transfer doesn't change total supply
    ensures global<TotalSupply>(@deployer).value ==
            old(global<TotalSupply>(@deployer).value);
}

Pattern 3: Integer Overflow Prevention

spec add_balance {
    // Precondition: addition won't overflow
    requires global<Balance>(addr).coins + amount <= MAX_U64;

    // Postcondition: new balance is sum
    ensures global<Balance>(addr).coins == old(global<Balance>(addr).coins) + amount;

    // Won't abort due to overflow (arithmetic is checked in Move)
    aborts_if false;  // No custom aborts
}

Pattern 4: Reentrancy Safety (N/A in Move)

// Move has no reentrancy issues, but can verify atomicity
spec withdraw_and_call {
    // State changes are atomic
    ensures global<Balance>(addr).coins == old(global<Balance>(addr).coins) - amount;

    // No intermediate states observable
    modifies global<Balance>(addr);
}

Pattern 5: Temporal Properties

spec module {
    // Once frozen, always frozen
    invariant update [global]
        forall addr: address:
            old(exists<Frozen>(addr)) ==> exists<Frozen>(addr);

    // Can only freeze, never unfreeze
    invariant update [global]
        forall addr: address:
            !old(exists<Frozen>(addr)) || exists<Frozen>(addr);
}

Complex Specification Examples

Example 1: Escrow Contract

struct Escrow has key {
    amount: u64,
    sender: address,
    recipient: address,
    deadline: u64,
    released: bool,
}

spec module {
    // Escrow invariants
    invariant [global]
        forall addr: address:
            exists<Escrow>(addr) ==>
            (global<Escrow>(addr).amount > 0 &&
             global<Escrow>(addr).deadline > 0);
}

public fun create_escrow(
    sender: &signer,
    recipient: address,
    amount: u64,
    deadline: u64
) {
    // ...
}

spec create_escrow {
    requires amount > 0;
    requires deadline > timestamp::now_seconds();
    requires !exists<Escrow>(signer::address_of(sender));

    ensures exists<Escrow>(signer::address_of(sender));
    ensures global<Escrow>(signer::address_of(sender)).amount == amount;
    ensures global<Escrow>(signer::address_of(sender)).recipient == recipient;
    ensures global<Escrow>(signer::address_of(sender)).deadline == deadline;
    ensures global<Escrow>(signer::address_of(sender)).released == false;
}

public fun release(escrow_addr: address) acquires Escrow {
    let escrow = borrow_global_mut<Escrow>(escrow_addr);
    assert!(timestamp::now_seconds() >= escrow.deadline, ERROR_NOT_EXPIRED);
    assert!(!escrow.released, ERROR_ALREADY_RELEASED);

    escrow.released = true;
    // Transfer amount to recipient
}

spec release {
    let escrow = global<Escrow>(escrow_addr);

    requires exists<Escrow>(escrow_addr);
    requires timestamp::now_seconds() >= escrow.deadline;
    requires !escrow.released;

    ensures global<Escrow>(escrow_addr).released == true;

    // All other fields unchanged
    ensures global<Escrow>(escrow_addr).amount == old(escrow.amount);
    ensures global<Escrow>(escrow_addr).sender == old(escrow.sender);
    ensures global<Escrow>(escrow_addr).recipient == old(escrow.recipient);
    ensures global<Escrow>(escrow_addr).deadline == old(escrow.deadline);
}

Example 2: Multi-Sig Wallet

struct MultiSig has key {
    owners: vector<address>,
    threshold: u64,
    proposal_count: u64,
}

struct Proposal has key {
    approvals: u64,
    executed: bool,
}

spec module {
    // Multi-sig invariants
    invariant [global]
        forall addr: address:
            exists<MultiSig>(addr) ==>
            (global<MultiSig>(addr).threshold > 0 &&
             global<MultiSig>(addr).threshold <= vector::length(&global<MultiSig>(addr).owners));
}

public fun approve_proposal(
    owner: &signer,
    wallet_addr: address,
    proposal_id: u64
) acquires MultiSig, Proposal {
    // ...
}

spec approve_proposal {
    let multisig = global<MultiSig>(wallet_addr);
    let owner_addr = signer::address_of(owner);

    // Preconditions
    requires exists<MultiSig>(wallet_addr);
    requires exists<Proposal>(proposal_id);
    requires vector::contains(&multisig.owners, &owner_addr);
    requires !global<Proposal>(proposal_id).executed;

    // Postcondition: approvals increased
    ensures global<Proposal>(proposal_id).approvals ==
            old(global<Proposal>(proposal_id).approvals) + 1;

    // Proposal executed when threshold reached
    ensures global<Proposal>(proposal_id).approvals >= multisig.threshold ==>
            global<Proposal>(proposal_id).executed;
}

Example 3: Staking with Rewards

struct Stake has key {
    amount: u64,
    start_time: u64,
    reward_rate: u64,
}

spec module {
    // Helper: calculate expected rewards
    fun calculate_rewards(stake: Stake, current_time: u64): u64 {
        let duration = current_time - stake.start_time;
        (stake.amount * stake.reward_rate * duration) / PRECISION
    }
}

public fun claim_rewards(staker: &signer) acquires Stake {
    let addr = signer::address_of(staker);
    let stake = borrow_global<Stake>(addr);

    let current_time = timestamp::now_seconds();
    let rewards = calculate_rewards(stake, current_time);

    // Transfer rewards
}

spec claim_rewards {
    let addr = signer::address_of(staker);
    let stake = global<Stake>(addr);
    let current_time = timestamp::now_seconds();

    requires exists<Stake>(addr);
    requires current_time >= stake.start_time;

    // Rewards calculated correctly
    ensures result == calculate_rewards(stake, current_time);

    // Stake amount unchanged
    ensures global<Stake>(addr).amount == old(stake.amount);
}

Debugging Verification Failures

Reading Error Messages

error: post-condition does not hold
   ┌── example.move:15:9 ───
   │
15 │         ensures global<Balance>(addr).coins == old(global<Balance>(addr).coins) + amount;
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   = Model:
     addr = 0x1
     amount = MAX_U64
     old(global<Balance>(addr).coins) = 1
     Result: overflow in addition

Solution: Add precondition to prevent overflow

spec deposit {
    requires global<Balance>(addr).coins + amount <= MAX_U64;
    ensures global<Balance>(addr).coins == old(global<Balance>(addr).coins) + amount;
}

Counterexamples

spec transfer {
    ensures global<Balance>(from).coins >= 0;
}

// Prover output:
// Counterexample:
//   from = 0x1
//   to = 0x2
//   amount = 100
//   old(global<Balance>(from).coins) = 50
//   Result: assertion failure (underflow)

Solution: Add precondition

spec transfer {
    requires global<Balance>(from).coins >= amount;
    ensures global<Balance>(from).coins >= 0;
}

Common Issues

1. Missing preconditions

// ❌ Fails: no precondition about existence
spec withdraw {
    ensures global<Balance>(addr).coins == old(global<Balance>(addr).coins) - amount;
}

// ✅ Fixed
spec withdraw {
    requires exists<Balance>(addr);
    ensures global<Balance>(addr).coins == old(global<Balance>(addr).coins) - amount;
}

2. Incomplete abort specifications

spec module {
    pragma aborts_if_is_strict;
}

// ❌ Fails: missing abort condition
spec transfer {
    aborts_if !exists<Balance>(from);
    // Missing: aborts_if !exists<Balance>(to);
    // Missing: aborts_if global<Balance>(from).coins < amount;
}

// ✅ Fixed
spec transfer {
    aborts_if !exists<Balance>(from);
    aborts_if !exists<Balance>(to);
    aborts_if global<Balance>(from).coins < amount;
}

3. Timeouts

// Complex verification may timeout
spec complex_function {
    pragma timeout = 300;  // Increase to 5 minutes
}

// Or simplify specification
spec complex_function {
    pragma verify = false;  // Skip for now
}

Running the Move Prover

Basic Commands

# Verify all modules in package
aptos move prove

# Verify specific module
aptos move prove --filter MyModule

# Verify with verbose output
aptos move prove --verbose

# Skip timeout warnings
aptos move prove --skip-timeout

# Generate coverage report
aptos move prove --coverage

Configuration File (Move.toml)

[prover]
# Enable/disable prover
enabled = true

# Timeout per function (seconds)
timeout = 60

# SMT solver
solver = "z3"

# Memory limit (MB)
memory_limit = 8192

# Random seed
random_seed = 42

# Verbosity level (0-4)
verbosity_level = 1

CI/CD Integration

# .github/workflows/verify.yml
name: Move Prover

on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v2

      - name: Install Aptos CLI
        run: |
          curl -fsSL "https://aptos.dev/scripts/install_cli.py" | python3

      - name: Install Move Prover
        run: |
          aptos move setup-prover

      - name: Run Move Prover
        run: |
          aptos move prove --verbose

Best Practices

✅ Do

• Start simple - Add basic specs first, then refine
• Use schema - Reuse common specifications
• Write helper functions - Keep specs readable
• Specify aborts completely - Use

  pragma aborts_if_is_strict

• Verify invariants - Especially for critical properties
• Document with specs - Specs are executable documentation
• Run in CI - Catch regressions early
• Profile verification - Identify slow functions

❌ Avoid

• Over-specifying - Don't prove trivial properties
• Ignoring timeouts - Investigate and fix, don't skip
• Skipping aborts - Incomplete specs miss bugs
• Complex quantifiers - May cause timeouts
• Verifying everything - Focus on critical functions
• Assuming soundness - Prover can have false positives

Specification Checklist

For each critical function:

• Preconditions (

  requires

  ) - What must be true before?
• Postconditions (

  ensures

  ) - What must be true after?
• Abort conditions (

  aborts_if

  ) - When should it fail?
• Modified resources (

  modifies

  ) - What state changes?
• Events (

  emits

  ) - What events are emitted?
• Invariants - What always holds?
• Conservation laws - Are resources conserved?
• Access control - Is authorization correct?
• Integer overflow - Are bounds checked?
• Temporal properties - Do state transitions make sense?

Response Style

• Formal but practical - Explain verification benefits clearly
• Example-driven - Show specs with corresponding code
• Error-aware - Help debug verification failures
• Pattern-focused - Teach reusable specification patterns
• Tool-savvy - Reference prover commands and pragmas

Follow-up Suggestions

After helping with Move Prover, suggest:

• Start with simple function specs
• Add module-level invariants
• Create schema for common patterns
• Set up CI/CD verification
• Profile and optimize slow verifications
• Document critical properties formally
• Review Aptos framework specs as examples