eric861129/move-prover

Move Prover Expert

Formal verification for Move smart contracts - mathematically prove your code is correct.

When to Use

• Writing specifications for Move functions
• Proving correctness properties (invariants, access control)
• Debugging verification failures or timeouts
• Understanding MSL (Move Specification Language)

Why Move Prover?

Testing checks specific inputs. Verification proves ALL inputs.

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

// Verification: Proves for ALL possible inputs
spec transfer {
    ensures sender_balance == old(sender_balance) - amount;
    ensures recipient_balance == old(recipient_balance) + amount;
}

Core Constructs

Preconditions - requires

Conditions that must be true BEFORE function runs:

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

Postconditions - ensures

Conditions that must be true AFTER function runs:

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

Abort Conditions - aborts_if

When function should abort:

spec withdraw {
    aborts_if !exists<Balance>(addr) with ERROR_NOT_FOUND;
    aborts_if global<Balance>(addr).coins < amount with ERROR_INSUFFICIENT;
}

Modified Resources - modifies

Which global resources change:

spec transfer {
    modifies global<Balance>(from);
    modifies global<Balance>(to);
}

The old() Operator

Access pre-execution values:

spec increment {
    ensures counter.value == old(counter.value) + 1;
}

Invariants

Struct Invariants

Properties that always hold for a struct:

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

spec Balance {
    invariant coins >= locked;
}

Module Invariants

Properties that hold across the module:

spec module {
    invariant [global]
        forall addr: address:
            exists<Balance>(addr) ==> global<Balance>(addr).coins >= 0;
}

Update Invariants

Properties about state transitions:

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

Quantifiers

Universal - forall

Property holds for ALL values:

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

Existential - exists

Property holds for AT LEAST ONE value:

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

Schemas (Reusable Specs)

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

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

// Reuse in functions
spec withdraw {
    include BalanceExists;
    include SufficientBalance;
}

Pragmas

spec module {
    pragma verify = true;           // Enable verification
    pragma aborts_if_is_strict;     // Require complete abort specs
    pragma timeout = 120;           // Timeout in seconds
}

spec complex_function {
    pragma verify = false;          // Skip this function
    pragma timeout = 300;           // Custom timeout
}

Common Patterns

Access Control

spec admin_only_function {
    requires exists<AdminCap>(signer::address_of(admin));
    aborts_if !exists<AdminCap>(signer::address_of(admin));
}

spec module {
    // Only one admin
    invariant [global]
        forall a1: address, a2: address:
            exists<AdminCap>(a1) && exists<AdminCap>(a2) ==> a1 == a2;
}

Supply Conservation

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

    invariant [global] total_balance() == global<TotalSupply>(@admin).value;
}

spec transfer {
    ensures global<TotalSupply>(@admin).value == old(global<TotalSupply>(@admin).value);
}

Overflow Prevention

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

Running the Prover

# Verify all modules
aptos move prove

# Verify specific module
aptos move prove --filter MyModule

# Verbose output
aptos move prove --verbose

Move.toml Configuration

[prover]
enabled = true
timeout = 60
solver = "z3"

Debugging Failures

Reading Errors

error: post-condition does not hold
   ┌── example.move:15:9 ───
15 │         ensures balance.coins == old(balance.coins) + amount;
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   = Counterexample:
     amount = MAX_U64
     old(balance.coins) = 1
     Result: overflow

Solution: Add overflow precondition:

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

Common Issues

Missing precondition:

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

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

Incomplete abort specs:

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;
}

Timeout:

spec complex_function {
    pragma timeout = 300;  // Increase timeout
    // Or simplify the specification
}

Complete Example

module 0x1::coin {
    struct Coin has key {
        value: u64
    }

    const ERROR_NOT_FOUND: u64 = 1;
    const ERROR_INSUFFICIENT: u64 = 2;

    public fun transfer(from: &signer, to: address, amount: u64) acquires Coin {
        let from_addr = signer::address_of(from);
        assert!(exists<Coin>(from_addr), ERROR_NOT_FOUND);
        assert!(exists<Coin>(to), ERROR_NOT_FOUND);

        let from_coin = borrow_global_mut<Coin>(from_addr);
        assert!(from_coin.value >= amount, ERROR_INSUFFICIENT);
        from_coin.value = from_coin.value - amount;

        let to_coin = borrow_global_mut<Coin>(to);
        to_coin.value = to_coin.value + amount;
    }

    spec transfer {
        let from_addr = signer::address_of(from);

        // Preconditions
        requires exists<Coin>(from_addr);
        requires exists<Coin>(to);
        requires global<Coin>(from_addr).value >= amount;
        requires global<Coin>(to).value + amount <= MAX_U64;

        // Abort conditions
        aborts_if !exists<Coin>(from_addr) with ERROR_NOT_FOUND;
        aborts_if !exists<Coin>(to) with ERROR_NOT_FOUND;
        aborts_if global<Coin>(from_addr).value < amount with ERROR_INSUFFICIENT;

        // Postconditions
        ensures global<Coin>(from_addr).value == old(global<Coin>(from_addr).value) - amount;
        ensures global<Coin>(to).value == old(global<Coin>(to).value) + amount;

        // Modified resources
        modifies global<Coin>(from_addr);
        modifies global<Coin>(to);
    }

    spec module {
        pragma verify = true;
        pragma aborts_if_is_strict;
    }
}

Specification Checklist

For critical functions, verify:

• [ ] Preconditions - What must be true before?
• [ ] Postconditions - What must be true after?
• [ ] Abort conditions - When should it fail?
• [ ] Modified resources - What state changes?
• [ ] Invariants - What always holds?
• [ ] Conservation - Are resources conserved?
• [ ] Access control - Is authorization correct?
• [ ] Overflow - Are bounds checked?

Resources

• Aptos Move Prover Docs: https://aptos.dev/move/prover/
• Move Specification Language: https://github.com/move-language/move/blob/main/language/move-prover/doc/user/spec-lang.md