Proving an Aptos Vault Correct with the Move Prover

Why Formal Verification?

Traditional testing is example-based. You might test depositing 100 APT (the Aptos native token) and withdrawing 50 APT, but what about edge cases like u64::MAX, single-octa balances, or 1,000 simultaneous withdrawals?

Formal verification tries to prove properties for all possible inputs:

Traditional Testing: "I tested 100 cases" → 100/∞ confidence

Formal Verification: "The prover checked all (bounded) paths" → Mathematical certainty

With that distinction in mind, let’s look at the concrete system we’re going to verify.

What We're Building

We'll build and verify a simple APT vault on Aptos. The vault allows users to:

• Deposit APT - send assets and receive proportional shares
• Withdraw APT - burn shares and receive proportional assets

We'll use formal verification to prove the following properties:

• The vault can only be initialized once
• Deposits require positive amounts and valid vault state
• Withdrawals require positive shares and valid vault state
• Assets increase on deposits and decrease on withdrawals
• Vault state remains consistent after all operations

Formal Specifications:
- initialize(): No double initialization, zero initial balance
- deposit(): Valid preconditions, assets increase
- withdraw(): Valid preconditions, assets decrease
- View functions: Always return non-negative values

‍

Installation & Setup

Installing the Aptos CLI

The Aptos CLI is required to use the Move Prover. Choose one of the following installation methods:

Option 1: Homebrew (Mac - Recommended)

brew update
brew install aptos
aptos help

Option 2: Install Script (Mac/Linux)‍

Using curl:

curl -fsSL "https://aptos.dev/scripts/install_cli.sh" | sh
aptos help

Or using wget:

wget -qO- "https://aptos.dev/scripts/install_cli.sh" | sh
aptos help

‍

Installing Move Prover Dependencies

After installing the Aptos CLI, install the prover dependencies with a single command:

aptos update prover-dependencies

This automatically installs Boogie, Z3, and all other required dependencies.

Verify Everything Works

aptos move prove --help

You should see the prover options and usage information.

Initialize Your Aptos Project

mkdir aptos-vault-prover
cd aptos-vault-prover
aptos move init --name vault_project

This creates:

aptos-vault-prover/
├── Move.toml
├── sources/
│   └── (your .move files)
└── tests/
    └── (your test files)

‍

The Vault Architecture

Before diving into formal specifications, it’s worth grounding ourselves in the vault’s design and accounting model.

High-Level Design

How Share Calculation Works

On Deposit:

IF first_deposit:
    shares_minted = amount (1:1 ratio)
ELSE:
    shares_minted = (amount * total_shares) / total_assets

On Withdrawal:

amount_withdrawn = (shares * total_assets) / total_shares

This ensures the ratio stays constant:

shares/assets before = shares/assets after

This proportional calculation ensures fair distribution of vault assets among shareholders.

‍

The Vault Implementation

Let's build the vault step by step. Create sources/vault.move:

module vault_project::vault {
    use std::signer;
    use std::option;
    use std::string;
    use aptos_framework::fungible_asset::{Self, Metadata, MintRef, TransferRef, BurnRef};
    use aptos_framework::object::{Self, Object};
    use aptos_framework::primary_fungible_store;
    use aptos_framework::coin::{Self, Coin};
    use aptos_framework::aptos_coin::AptosCoin;

    /// Error codes
    const E_NOT_INITIALIZED: u64 = 1;
    const E_ALREADY_INITIALIZED: u64 = 2;
    const E_INVALID_AMOUNT: u64 = 3;
    const E_INSUFFICIENT_SHARES: u64 = 4;
    const E_INSUFFICIENT_BALANCE: u64 = 5;

    /// Vault configuration - stores share token metadata and references
    struct VaultConfig has key {
        mint_ref: MintRef,
        burn_ref: BurnRef,
        transfer_ref: TransferRef,
        metadata: Object<Metadata>,
    }

    /// Vault treasury - holds deposited APT
    struct VaultTreasury has key {
        coins: Coin<AptosCoin>,
    }

    /// Initialize the vault (one-time operation)
    public entry fun initialize(admin: &signer) {
        let admin_addr = signer::address_of(admin);
        assert!(!exists<VaultConfig>(admin_addr), E_ALREADY_INITIALIZED);

        // Create fungible asset for vault shares
        let constructor_ref = &object::create_named_object(admin, b"VAULT_SHARES");

        primary_fungible_store::create_primary_store_enabled_fungible_asset(
            constructor_ref,
            option::none(),
            string::utf8(b"Vault Shares"),
            string::utf8(b"vAPT"),
            8,
            string::utf8(b"https://aptos.dev/icon.png"),
            string::utf8(b"https://aptos.dev"),
        );

        // Generate references for minting/burning shares
        let mint_ref = fungible_asset::generate_mint_ref(constructor_ref);
        let burn_ref = fungible_asset::generate_burn_ref(constructor_ref);
        let transfer_ref = fungible_asset::generate_transfer_ref(constructor_ref);
        let metadata = object::object_from_constructor_ref<Metadata>(constructor_ref);

        // Store vault config
        move_to(admin, VaultConfig {
            mint_ref,
            burn_ref,
            transfer_ref,
            metadata,
        });

        // Initialize treasury with zero balance
        move_to(admin, VaultTreasury {
            coins: coin::zero<AptosCoin>(),
        });
    }

    /// Deposit APT, receive proportional shares
    public entry fun deposit(user: &signer, amount: u64) 
        acquires VaultConfig, VaultTreasury 
    {
        assert!(amount > 0, E_INVALID_AMOUNT);

        let vault_config = borrow_global_mut<VaultConfig>(@vault_project);
        let vault_treasury = borrow_global_mut<VaultTreasury>(@vault_project);
        let user_addr = signer::address_of(user);

        let total_assets = coin::value(&vault_treasury.coins);

        // Calculate shares to mint
        let shares_to_mint = if (total_assets == 0) {
            amount  // First deposit: 1:1 ratio
        } else {
            let total_shares = fungible_asset::supply(vault_config.metadata);
            let total_shares_value = option::extract(&mut total_shares);
            (((amount as u128) * total_shares_value) / (total_assets as u128) as u64)
        };

        // Transfer APT from user to vault
        let deposited_coins = coin::withdraw<AptosCoin>(user, amount);
        coin::merge(&mut vault_treasury.coins, deposited_coins);

        // Mint shares to user
        let shares = fungible_asset::mint(&vault_config.mint_ref, shares_to_mint);
        primary_fungible_store::deposit(user_addr, shares);
    }

    /// Burn shares, withdraw proportional APT
    public entry fun withdraw(user: &signer, shares: u64) 
        acquires VaultConfig, VaultTreasury 
    {
        assert!(shares > 0, E_INVALID_AMOUNT);

        let vault_config = borrow_global_mut<VaultConfig>(@vault_project);
        let vault_treasury = borrow_global_mut<VaultTreasury>(@vault_project);
        let user_addr = signer::address_of(user);

        // Verify user has enough shares
        let user_shares = primary_fungible_store::balance(user_addr, vault_config.metadata);
        assert!(user_shares >= shares, E_INSUFFICIENT_SHARES);

        // Calculate APT to withdraw
        let total_shares = fungible_asset::supply(vault_config.metadata);
        let total_shares_value = option::extract(&mut total_shares);
        let total_assets = coin::value(&vault_treasury.coins);
        let amount_to_withdraw = (((shares as u128) * (total_assets as u128)) / total_shares_value as u64);

        assert!(total_assets >= amount_to_withdraw, E_INSUFFICIENT_BALANCE);

        // Burn shares from user
        let shares_to_burn = primary_fungible_store::withdraw(user, vault_config.metadata, shares);
        fungible_asset::burn(&vault_config.burn_ref, shares_to_burn);

        // Transfer APT to user
        let withdrawn_coins = coin::extract(&mut vault_treasury.coins, amount_to_withdraw);
        coin::deposit(user_addr, withdrawn_coins);
    }

    // View functions

    #[view]
    public fun total_assets(): u64 acquires VaultTreasury {
        let vault_treasury = borrow_global<VaultTreasury>(@vault_project);
        coin::value(&vault_treasury.coins)
    }

    #[view]
    public fun total_shares(): u128 acquires VaultConfig {
        let vault_config = borrow_global<VaultConfig>(@vault_project);
        let total_shares = fungible_asset::supply(vault_config.metadata);
        option::extract(&mut total_shares)
    }

    #[view]
    public fun balance_of(user: address): u64 acquires VaultConfig {
        let vault_config = borrow_global<VaultConfig>(@vault_project);
        primary_fungible_store::balance(user, vault_config.metadata)
    }

    #[view]
    public fun preview_deposit(amount: u64): u64 acquires VaultConfig, VaultTreasury {
        if (!exists<VaultConfig>(@vault_project)) {
            return amount
        };

        let vault_config = borrow_global<VaultConfig>(@vault_project);
        let vault_treasury = borrow_global<VaultTreasury>(@vault_project);
        let total_assets = coin::value(&vault_treasury.coins);

        if (total_assets == 0) {
            amount
        } else {
            let total_shares = fungible_asset::supply(vault_config.metadata);
            let total_shares_value = option::extract(&mut total_shares);
            (((amount as u128) * total_shares_value) / (total_assets as u128) as u64)
        }
    }

    #[view]
    public fun preview_withdraw(shares: u64): u64 acquires VaultConfig, VaultTreasury {
        if (!exists<VaultConfig>(@vault_project)) {
            return 0
        };

        let vault_config = borrow_global<VaultConfig>(@vault_project);
        let vault_treasury = borrow_global<VaultTreasury>(@vault_project);
        let total_shares = fungible_asset::supply(vault_config.metadata);
        let total_shares_value = option::extract(&mut total_shares);
        let total_assets = coin::value(&vault_treasury.coins);

        if (total_shares_value == 0) {
            0
        } else {
            (((shares as u128) * (total_assets as u128)) / total_shares_value as u64)
        }
    }
}

This is a standard vault implementation. What matters next is not how it looks, but what we can prove about its behaviour.

‍

Writing Formal Specifications

Formal specs in Move use the spec keyword. Think of them as contracts that the prover must verify.

Understanding pragma aborts_if_is_partial

Before we dive into specs, you'll see this pragma everywhere:

spec function_name {
    pragma aborts_if_is_partial;
    // ... specifications
}

What does it mean?

The Aptos framework is complex. Functions like coin::withdraw() or fungible_asset::mint() have dozens of possible abort conditions deep in their call stacks. Specifying every single one would be:

1. Verbose - Hundreds of lines per function
2. Fragile - Break when framework updates
3. Unnecessary - Most relate to framework internals, not your business logic

pragma aborts_if_is_partial tells the prover: "I'm specifying the abort conditions I care about (business logic), trust the framework for the rest."

‍

Module-Level Invariant

Add this at the end of your vault.move file:

spec module {
    pragma aborts_if_is_partial;

    /*
     * This module uses formal specifications to prove:
     * 
     * 1. Initialization safety - Vault can only be initialized once
     * 2. State consistency - VaultConfig and VaultTreasury exist together
     * 3. Operation validity - Deposits and withdrawals require valid state
     * 4. Asset accounting - Assets increase on deposit, decrease on withdraw
     * 5. Input validation - Zero amounts are rejected
     * 
     * The specs verify these properties hold for all possible inputs and states.
     */
}

This comment documents what properties our formal specifications verify.

Function-Level Specifications

Now let's add specs for each function. Add these right after the module-level spec:

1. Initialize Specification

spec initialize {
    pragma aborts_if_is_partial;

    let admin_addr = signer::address_of(admin);

    // Precondition: Vault must NOT already exist
    aborts_if exists<VaultConfig>(admin_addr);
    aborts_if exists<VaultTreasury>(admin_addr);

    // Postconditions: Both resources created with zero balance
    ensures exists<VaultConfig>(admin_addr);
    ensures exists<VaultTreasury>(admin_addr);
    ensures coin::value(global<VaultTreasury>(admin_addr).coins) == 0;
}

What this proves:

• No double initialization (prevents overwriting existing vault)
• Both VaultConfig and VaultTreasury created atomically
• Vault starts with zero assets (important for first deposit logic)

2. Deposit Specification

spec deposit {
    pragma aborts_if_is_partial;

    // Preconditions
    aborts_if !exists<VaultConfig>(@vault_project);
    aborts_if !exists<VaultTreasury>(@vault_project);
    aborts_if amount == 0;

    // Postconditions
    ensures exists<VaultConfig>(@vault_project);
    ensures exists<VaultTreasury>(@vault_project);
    ensures coin::value(global<VaultTreasury>(@vault_project).coins) ==
            old(coin::value(global<VaultTreasury>(@vault_project).coins)) + amount;
}

What this proves:

• Can't deposit to uninitialized vault
• Zero deposits rejected
• Assets increase by exactly amount deposited
• Vault state remains valid

3. Withdraw Specification

spec withdraw {
    pragma aborts_if_is_partial;

    let vault_treasury = global<VaultTreasury>(@vault_project);
    let total_assets_before = coin::value(vault_treasury.coins);

    // Preconditions
    aborts_if !exists<VaultConfig>(@vault_project);
    aborts_if !exists<VaultTreasury>(@vault_project);
    aborts_if shares == 0;

    // Postcondition: Assets decrease
    ensures coin::value(global<VaultTreasury>(@vault_project).coins) <= total_assets_before;
    ensures exists<VaultConfig>(@vault_project);
    ensures exists<VaultTreasury>(@vault_project);
}

What this proves:

• Can't withdraw from uninitialized vault
• Zero share withdrawals rejected
• Total assets decrease (or stay same if rounding)
• Vault integrity maintained

‍‍

4. View Function Specifications

spec balance_of {
    pragma aborts_if_is_partial;
    aborts_if !exists<VaultConfig>(@vault_project);
    ensures result >= 0;
}

spec preview_withdraw {
    pragma aborts_if_is_partial;
    aborts_if exists<VaultConfig>(@vault_project) && !exists<VaultTreasury>(@vault_project);
    ensures result >= 0;
}

spec total_assets {
    pragma aborts_if_is_partial;
    aborts_if !exists<VaultTreasury>(@vault_project);
    ensures result == coin::value(global<VaultTreasury>(@vault_project).coins);
}

spec total_shares {
    pragma aborts_if_is_partial;
    aborts_if !exists<VaultConfig>(@vault_project);
    ensures result >= 0;
}

With the specifications in place, we can now see how the Move Prover actually verifies them.

‍

The Verification Flow

Here's what happens when you run the prover:

vault.move → Move Compiler → Bytecode + Specs → Move Prover
                                                      ↓
                                                  Boogie IL
                                                      ↓
                                                  Z3 Solver
                                                 ↙     ↘            ↘
                                    [✓ SUCCESS]      [✗ FAILURE]    [TIMEOUT]     
                               All paths verified  Counterexample  Undetermined

The prover:

1. Compiles your Move code to bytecode
2. Translates specs to logical formulas
3. Generates verification conditions for all execution paths
4. Invokes Z3 to check if specs hold for all possible inputs
5. Reports success or shows counterexamples

Limitation: In some cases, the search space of possible inputs and execution paths is extremely large. When this happens, the prover might need to run for an impractically long time, potentially days, months, or even longer.

To handle this in practice, we set a timeout parameter that limits how long the prover is allowed to run. This is usually set to a few minutes or hours, depending on complexity. If the timeout is reached before verification completes, the prover stops, and the property is marked as undetermined, meaning it was not proven true or false.

This is a common scenario in real-world codebases.

‍

Running the Prover

Compile First

aptos move compile

This should output:

Compiling, may take a little while to download git dependencies...
...
{
  "Result": "Success"
}

Run Verification

aptos move prove

Expected output:

Proving vault_project::vault ...
[INFO] preparing module 0x123::vault
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 8 verification conditions
[INFO] running solver (Z3)
[INFO] 8 verification conditions proven
SUCCESS

What just happened?

The prover checked 8 verification conditions across all your specs and proved them mathematically. This means for every possible input, your vault maintains the specified properties.

Proofs are only useful if failures are understandable, so let’s look at what happens when a specification is wrong:

If Verification Fails

Let's intentionally break something to see what failure looks like. Change the deposit spec to:

ensures coin::value(global<VaultTreasury>(@vault_project).coins) ==
        old(coin::value(global<VaultTreasury>(@vault_project).coins)) + amount + 1;

Run aptos move prove again:

error: post-condition does not hold
    ┌─ sources/vault.move:257:9
    │  
257 │ ╭         ensures coin::value(global<VaultTreasury>(@vault_project).coins) ==
258 │ │                 old(coin::value(global<VaultTreasury>(@vault_project).coins)) + amount + 1;
    │ ╰───────────────────────────────────────────────────────────────────────────────────────────^
    │  
    =     at sources/vault.move:76: deposit
    =         user = signer{0x10000...}
    =         amount = 2
    =     at sources/vault.move:80: deposit
    =         vault_treasury = &vault::VaultTreasury{coins = coin::Coin{value = 0}}
    ...
    =     Post-condition failed
    =         amount = 2
    =         old(total_assets) = 0
    =         new(total_assets) = 2  (not 3 as spec claims)

The prover found a counterexample proving the spec is wrong - when depositing 2 APT into an empty vault, assets increase by 2, not 3. This demonstrates the power of formal verification: it doesn't just say "test failed," it shows the exact input that breaks your claim.

‍

What Gets Verified vs Trusted

Explicitly Verified (Your Specs)

1. Resource Existence - Functions require initialized vault
2. Zero Rejection - Empty deposits/withdrawals abort
3. State Consistency - Resources exist together after operations
4. Monotonic Changes - Assets increase on deposit, decrease on withdraw
5. Non-Negative Results - View functions return valid values

Implicitly Trusted (Framework)

1. Arithmetic Safety - Move VM prevents overflow/underflow
2. Coin Validity - Framework ensures sufficient balances
3. Share Accounting - Fungible asset framework tracks supply correctly
4. Ownership - Primary store operations respect ownership

‍

The prover assumes the framework is correct. This is reasonable as the Aptos framework is heavily audited and formally verified itself.

‍

Common Spec Patterns

Pattern 1: State Preconditions

spec deposit {
    aborts_if !exists<VaultConfig>(@vault_project);
    aborts_if !exists<VaultTreasury>(@vault_project);
}

Use: Ensure required resources exist before operations.

Pattern 2: Input Validation

spec deposit {
    aborts_if amount == 0;
}

Use: Reject invalid inputs at the spec level.

Pattern 3: State Postconditions

spec initialize {
    ensures exists<VaultConfig>(admin_addr);
    ensures coin::value(global<VaultTreasury>(admin_addr).coins) == 0;
}

Use: Guarantee state after successful execution.

Pattern 4: Monotonic Properties

spec deposit {
    ensures coin::value(global<VaultTreasury>(@vault_project).coins) >=
            old(coin::value(global<VaultTreasury>(@vault_project).coins));
}

‍Use: Prove values only increase/decrease appropriately.

Pattern 5: Exact Changes

spec deposit {
    ensures coin::value(global<VaultTreasury>(@vault_project).coins) ==
            old(coin::value(global<VaultTreasury>(@vault_project).coins)) + amount;
}

Use: Prove exact state transitions.

‍

Debugging Failed Proofs

When a proof fails, follow this process:

Step 1: Read the Error

ERROR: post-condition does not hold
  ┌─ sources/vault.move:150:9
  │
150 │         ensures total_assets_after == total_assets_before + amount;
  │         ^^^^^^ Post-condition failed

Tells you which spec failed and where.

Step 2: Check the Counterexample

Counterexample:
  amount = 0
  total_assets_before = 100
  total_assets_after = 100

Shows you the exact input that breaks your claim.

‍

Step 3: Fix the Spec or Code

Either:

• Fix the spec if your claim was too strong
• Fix the code if there's an actual bug

In this case, we forgot to specify aborts_if amount == 0, so the prover found a case where the postcondition doesn't hold.

‍

Step 4: Re-verify

aptos move prove

Repeat until all proofs pass.

‍

Performance Tips

1. Use pragma aborts_if_is_partial

Don't try to specify every framework abort condition.

‍

2. Keep Specs Focused

Specify what matters for your business logic:

// Good: Focused on business logic
spec deposit {
    aborts_if amount == 0;
    ensures vault_balance_increases;
}

// Bad: Over-specifying framework details
spec deposit {
    aborts_if !coin::is_account_registered<AptosCoin>(user);
    aborts_if coin::balance<AptosCoin>(user) < amount;
    aborts_if !exists<CoinStore<AptosCoin>>(user);
    // ... 20 more framework conditions
}

‍

3. Separate Complex Logic

If verification is slow, consider extracting complex logic to helper functions with their own specs.

‍

4. Use assume for Framework Trust

spec helper_function {
    // Trust framework guarantee
    assume fungible_asset::supply(metadata) >= 0;
    
    // Prove your logic
    ensures result == compute_shares(amount);
}

Conclusion

Formal verification transforms "I think this works" into "I can prove this works." The Move Prover gives you compile-time mathematical guarantees that your vault:

1. Can only be initialized once
2. Rejects zero deposits/withdrawals
3. Maintains correct asset accounting
4. Preserves vault state consistency
5. Validates all preconditions before operations

This is the difference between:

"We tested 1000 scenarios" → 1000/∞ confidence
"The prover verified all paths" → ∞/∞ confidence

‍

For production DeFi protocols handling millions in TVL, this level of assurance isn't optional, it's essential. Formal verification doesn't replace testing; it complements it by proving properties that tests can only sample.

As with any testing methodology, formal verification has limits, which we briefly touched on above (e.g. timeouts that leave properties undetermined). There’s also another important limitation: formal verification only proves whether the specific list of stated properties holds or not. There could be other important properties that developers or auditors miss, and those aren’t verified. These missed properties are exactly what attackers tend to exploit.

We’ve seen several DeFi protocols across various ecosystems that were "formally verified" and still got hacked. In post-mortem analysis, once the missing property was identified and written down, the formal verifier correctly flagged the vulnerability.

So, be cautious when making strong claims about formal verification. It does not prove the absence of bugs - That would require verifying every possible property about a given program, which isn’t practical for most real-world systems.

If you’re coming from an EVM or Solana background and want to understand how Move-based systems approach safety and correctness at a conceptual level, this related piece may be useful:

Sui Move for EVM and SVM Developers: Part 1 – Mental Models
https://www.adevarlabs.com/blog/sui-move-for-evm-and-svm-developers-part-1-mental-models

We publish practical, high-signal deep dives like this based on real audit work and hands-on protocol analysis. If you’re building close to the metal and care about correctness, follow Adevar Labs on X and LinkedIn for future write-ups on Move, Rust, and smart contract security.

‍

Ship Safely.

‍

References

• Aptos Move Prover Guide
• Move Specification Language
• Boogie Documentation
• Z3 Theorem Prover

‍