---
name: move-prover
description: Move Prover formal verification expert for Aptos smart contracts. Write specifications (MSL), preconditions (requires), postconditions (ensures), invariants, abort conditions (aborts_if), quantifiers, schemas, and pragmas. Debug verification failures. Triggers on Move Prover, formal verification, spec, invariant, ensures, requires, aborts_if, precondition, postcondition.
allowed-tools: Read, Write, Edit, Grep, Glob, Bash
model: sonnet
license: MIT
metadata:
  author: raintree
  version: "1.0"
---

# 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.**

```move
// 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:

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

### Postconditions - `ensures`

Conditions that must be true AFTER function runs:

```move
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:

```move
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:

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

### The `old()` Operator

Access pre-execution values:

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

## Invariants

### Struct Invariants

Properties that always hold for a struct:

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

spec Balance {
    invariant coins >= locked;
}
```

### Module Invariants

Properties that hold across the module:

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

### Update Invariants

Properties about state transitions:

```move
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:

```move
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:

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

## Schemas (Reusable Specs)

```move
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

```move
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

```move
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

```move
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

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

## Running the Prover

```bash
# Verify all modules
aptos move prove

# Verify specific module
aptos move prove --filter MyModule

# Verbose output
aptos move prove --verbose
```

### Move.toml Configuration

```toml
[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:
```move
spec deposit {
    requires global<Balance>(addr).coins + amount <= MAX_U64;
}
```

### Common Issues

**Missing precondition:**
```move
// 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:**
```move
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:**
```move
spec complex_function {
    pragma timeout = 300;  // Increase timeout
    // Or simplify the specification
}
```

## Complete Example

```move
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