Proving an Aptos Vault Correct with the Move Prover

Testing finds bugs. It does not prove their absence. While unit tests validate specific scenarios, formal verification goes further by proving correctness across all possible inputs and execution paths. The Move Prover gives you this guarantee on Aptos. In this guide, we go from installation to writing formal specifications that verify the core safety properties of a vault: proper initialization, valid deposits, safe withdrawals, and state consistency.

Why Formal Verification?

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

Formal verification proves properties for all possible inputs:

• Traditional Testing: "I tested 100 cases" → 100/∞ confidence
• Formal Verification: "The prover checked all (bounded) paths" → Mathematical certainty

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

Installation & Setup

Installing the Aptos CLI

Option 1: Homebrew (Mac - Recommended)

brew update
brew install aptos
aptos help

Option 2: Install Script (Mac/Linux)

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

Installing Move Prover Dependencies

aptos update prover-dependencies

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

Initialize Your Aptos Project

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

The Vault Architecture

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

Writing Formal Specifications

The Move Prover uses a specification language built into Move to define what "correct" means for each function.

Initializing the Vault

The key invariants for initialization are:

1. The vault cannot be initialized twice
2. Initial balances must be zero
3. The admin must be the signer

A specification for these invariants verifies that no matter how many times someone calls initialize, the second call always aborts if the vault already exists.

Deposit Specifications

For deposits, the key post-conditions are:

• Total assets must increase by exactly the deposited amount
• The user must receive the correct number of shares
• The share ratio must be preserved

Withdrawal Specifications

For withdrawals:

• Total assets must decrease by the withdrawn amount
• User shares must be burned
• The contract must not allow withdrawals that would leave it insolvent

Running the Prover

aptos move prove

If all specifications are satisfied, the prover will output a success message. Any violations will be reported with the specific invariant that was broken.

Common Pitfalls

Integer overflow: Aptos Move uses u64, which can overflow. Specifications should verify that arithmetic operations don't overflow.

Ghost variables: The prover uses ghost variables to track state across function calls. These are not real contract state - they exist only in the specification layer.

Aborts: Every function that can abort should have an aborts_if specification. Missing abort conditions will cause the prover to produce false positives.

Conclusion

Formal verification with the Move Prover is a powerful tool for ensuring correctness in DeFi protocols. By specifying invariants mathematically, you can prove that your vault behaves correctly across all possible inputs - not just the ones you thought to test.

The investment in formal specs pays off during security audits: instead of asking "does this look correct?", reviewers can verify mathematical proofs of correctness.