Formal Verification with the Move Prover

The Move Prover translates Move code plus specifications into a verification language (Boogie) and uses SMT solvers (Z3, optionally CVC5) to prove that the code satisfies its specs for all possible inputs and states — not just test cases.

40.1 What the Prover does

The Move Prover translates Move code plus specifications into a verification language (Boogie) and uses SMT solvers (Z3, optionally CVC5) to prove that the code satisfies its specs for all possible inputs and states — not just test cases.

Run it with aptos move prove (Aptos/Movement) or the Sui Prover for Sui packages.

40.2 Spec blocks

module my_addr::math {
    public fun add(a: u64, b: u64): u64 { a + b }

    spec add {
        aborts_if a + b > MAX_U64;
        ensures result == a + b;
    }

    public fun safe_div(a: u64, b: u64): u64 {
        if (b == 0) 0 else a / b
    }

    spec safe_div {
        aborts_if false;                      // never aborts
        ensures b == 0 ==> result == 0;
        ensures b > 0 ==> result == a / b;
    }
}

40.3 Spec language essentials

Precondition assumed on entry Postcondition that must hold on normal return

Function aborts if (and, with strict mode, only if) P aborts_with CODE Function aborts with the given code modifies global<T>(addr)

Frame condition: only these resources change result, result_1 Return value(s) Value of e at function entry global<T>(addr), exists<T>(addr) Global storage in specs invariant P (in struct spec)

Data invariant for all values of the struct invariant P (in spec module) Global invariant over storage forall x: T: P, exists x: T: P Helper functions usable only in specs spec schema / include Reusable groups of conditions pragma verify = false; Skip verification for an item pragma aborts_if_is_partial; Allow incomplete aborts_if lists

40.4 Verifying resource invariants (Aptos)

If you delete the assert!, the Prover reports that the struct invariant value <= MAX can be violated and shows a counterexample.

module my_addr::capped_counter {
    use std::signer;

    const MAX: u64 = 100;
    const E_CAP: u64 = 1;

    struct Counter has key { value: u64 }

    spec Counter {
        invariant value <= MAX;
    }

    public entry fun increment(account: &signer) acquires Counter {
        let c = borrow_global_mut<Counter>(signer::address_of(account));
        assert!(c.value < MAX, E_CAP);
        c.value = c.value + 1;
    }

    spec increment {
        let addr = signer::address_of(account);
        aborts_if !exists<Counter>(addr);
        aborts_if global<Counter>(addr).value >= MAX;
        ensures global<Counter>(addr).value == old(global<Counter>(addr).value) + 1;
        modifies global<Counter>(addr);
    }
}

40.5 Practical advice

Start with aborts_if and simple ensures for core arithmetic and access control.

Specify conservation properties for assets (total supply equals sum of balances; pool reserves only change through swaps).

Keep loops simple or annotate with loop invariants (spec { invariant ... } inside loops).

The Aptos Framework itself is extensively specified — read its .spec.move files as examples.

🧪 Part III Exercises

(Aptos) Build a TodoList resource with add/complete/remove entry functions, a #[view] for counts, and tests covering missing-resource aborts.

(Aptos) Rewrite the TodoList so each todo list is an object created with create_object, transferable to another account.

(Sui) Create a Hero object that can equip a wrapped Sword and attach a Shield via a dynamic object field. Inspect both in an explorer and explain why only the shield is visible as its own object.

(Sui) Implement a soulbound Certificate (key only) and a transferable Medal (key + store); show that public_transfer fails to compile for the certificate.

Implement a flash-loan pool with a hot-potato receipt; write a test proving the transaction fails if the loan is not repaid.

Create your own coin (Sui create_currency or Aptos FA), mint to two addresses, and add a burn function protected by the treasury capability / burn ref.

Mint an NFT collection with Display (Sui) or the Digital Asset standard (Aptos), including a royalty, and view it in a wallet.

Write a dice game using on-chain randomness, and explain in comments how your design prevents test-and-abort and undergasing attacks.

Publish a package, then upgrade it with a new function and a version check on a shared object; demonstrate that the old entry point rejects calls after migration.

Write Move Prover specs for a transfer(from, to, amount) function in a simple ledger, proving that the sum of the two balances is unchanged.