Formal Verification

Formal verification in Move uses the Move Prover tool to mathematically verify that smart contracts behave correctly under all possible conditions. Unlike traditional testing which checks specific scenarios, formal verification provides mathematical proofs that your code satisfies specified properties for all possible inputs and states.

Overview

The Move Prover is a sophisticated verification tool that analyzes Move modules and proves that they satisfy formal specifications written in the Move Specification Language (MSL). It uses automated theorem proving techniques to verify safety properties, invariants, and functional correctness of your smart contracts before deployment.

Technical Implementation

Formal verification works by translating Move code and specifications into logical formulas that can be processed by SMT (Satisfiability Modulo Theories) solvers. The prover checks whether your code can violate any specified invariants or preconditions under any execution path.

Specification Syntax

module 0x1::verified_coin {
    use std::signer;

    struct Balance has key {
        value: u64
    }

    spec Balance {
        invariant value <= MAX_U64;
    }

    public fun transfer(from: &signer, to: address, amount: u64) acquires Balance {
        let from_addr = signer::address_of(from);
        let from_balance = &mut borrow_global_mut<Balance>(from_addr).value;
        let to_balance = &mut borrow_global_mut<Balance>(to).value;

        *from_balance = *from_balance - amount;
        *to_balance = *to_balance + amount;
    }

    spec transfer {
        requires exists<Balance>(signer::address_of(from));
        requires exists<Balance>(to);
        requires borrow_global<Balance>(signer::address_of(from)).value >= amount;
        ensures borrow_global<Balance>(to).value == old(borrow_global<Balance>(to).value) + amount;
        ensures borrow_global<Balance>(signer::address_of(from)).value ==
                old(borrow_global<Balance>(signer::address_of(from)).value) - amount;
    }
}

Real-World Use Cases

1. DeFi Protocol Security: Verify that token supply invariants hold across all transfer, mint, and burn operations, ensuring no tokens can be created or destroyed unexpectedly.

2. Access Control Validation: Prove that administrative functions can only be called by authorized accounts and that privilege escalation is impossible.

3. Asset Conservation: Verify that total value in lending protocols, DEXes, or vaults remains constant during operations, preventing loss of funds.

4. Upgrade Safety: Prove that module upgrades maintain backward compatibility and preserve critical invariants about stored data.

5. Overflow Protection: Mathematically verify that arithmetic operations cannot overflow or underflow, eliminating a major class of vulnerabilities.

6. State Machine Correctness: Verify that state transitions in governance systems, auctions, or multi-step processes follow valid sequences.

Best Practices

Focus on Critical Properties: Start by verifying the most important safety properties such as asset conservation, access control, and state invariants. Don't try to verify everything at once.

Use Modular Specifications: Break down complex specifications into smaller, reusable components using schema and helper functions in MSL.

Test Specifications: Specifications can have bugs too. Use the prover's counterexample feature to validate that your specifications catch actual bugs.

Iterative Refinement: Begin with simple invariants and progressively add more detailed specifications as you gain confidence in the prover's behavior.

Performance Optimization: Use timeouts, specify verification scope, and leverage modular verification to keep proof times manageable for large codebases.

Documentation: Specifications serve as precise documentation of your contract's behavior. Keep them readable and well-commented.

Running the Move Prover

# Verify all modules in a package
aptos move prove --package-dir .

# Verify specific module
aptos move prove --package-dir . --filter "0x1::verified_coin"

# Generate detailed error traces
aptos move prove --package-dir . --verbose

# Set timeout for proofs
aptos move prove --package-dir . --timeout 120

The prover will report any specification violations with counterexamples showing how the property can be violated, or confirm that all specifications hold.

Related Concepts

• Testing - Complement formal verification with comprehensive unit tests
• Module Structure - Organize code to facilitate verification
• Resource Management - Understand resource semantics for writing correct specifications