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.
Formal verification for Move smart contracts - mathematically prove your code is correct.
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;
}
requiresConditions that must be true BEFORE function runs:
spec withdraw {
requires exists<Balance>(addr);
requires global<Balance>(addr).coins >= amount;
}
ensuresConditions 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;
}
aborts_ifWhen function should abort:
spec withdraw {
aborts_if !exists<Balance>(addr) with ERROR_NOT_FOUND;
aborts_if global<Balance>(addr).coins < amount with ERROR_INSUFFICIENT;
}
modifiesWhich global resources change:
spec transfer {
modifies global<Balance>(from);
modifies global<Balance>(to);
}
old() OperatorAccess pre-execution values:
spec increment {
ensures counter.value == old(counter.value) + 1;
}
Properties that always hold for a struct:
struct Balance has key {
coins: u64,
locked: u64,
}
spec Balance {
invariant coins >= locked;
}
Properties that hold across the module:
spec module {
invariant [global]
forall addr: address:
exists<Balance>(addr) ==> global<Balance>(addr).coins >= 0;
}
Properties about state transitions:
spec module {
invariant update [global]
forall addr: address:
old(exists<Frozen>(addr)) ==> exists<Frozen>(addr);
// Once frozen, always frozen
}
forallProperty 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);
}
existsProperty holds for AT LEAST ONE value:
spec module {
invariant exists addr: address: exists<AdminCap>(addr);
// At least one admin exists
}
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;
}
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
}
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;
}
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);
}
spec deposit {
requires global<Balance>(addr).coins + amount <= MAX_U64;
ensures global<Balance>(addr).coins == old(global<Balance>(addr).coins) + amount;
}
# Verify all modules
aptos move prove
# Verify specific module
aptos move prove --filter MyModule
# Verbose output
aptos move prove --verbose
[prover]
enabled = true
timeout = 60
solver = "z3"