📚 Series Overview

This series is designed for Move developers who want to go beyond testing to mathematically prove their contracts are secure. Whether you're building on Sui or Aptos, these techniques will help you catch bugs that testing can never find.

• Part 1: Why Formal Verification Matters for Move

• Part 2: Your First Verification Rule

• Part 3: Invariants and Inductive Proofs

• Part 4: Advanced Techniques: Parametric Rules & Ghost State

Prerequisites:

1. Move Basics: Structs, functions, abilities.

2. DeFi Primitives: Vaults, LP tokens, AMMs.

3. Certora: Sign up and read the docs.

---

Part 1: Why Formal Verification Matters

"Testing tells you what's wrong. Formal verification proves what's right."

Testing can only explore the paths you think of. Formal verification explores every possible path.

This isn't theoretical. It's the difference between "we tested 1000 scenarios" and "we mathematically proved this holds for all $2^{256}$ possible inputs."

🔍 What is Formal Verification?

Formal verification (FV) uses mathematical proofs to verify that code behaves correctly under all possible conditions. Instead of running your code with specific inputs, FV reasons about it symbolically.

---

⚡ Why Move + Certora?

Move was explicitly designed for smart contracts, with formal verification built into the language DNA. Unlike other languages where FV is an afterthought, Move's bytecode verifier and formal semantics make it uniquely suited for proofs.

The Move Advantage

• Native FV Support: Write specifications in Move itself, not a separate language like CVL.

• Simplicity: No dynamic dispatch or reentrancy to complicate proofs.

• Resource Safety: Linear types ensure assets can't be copied or dropped.

Certora SUI Prover takes your Move implementation and specs, translates them into mathematical constraints, and uses SMT solvers to prove they match.

---

🧪 A Taste of What's Possible

Here's a property you might want to prove for a DeFi vault:

Property: "If a user deposits X tokens, the vault balance always increases by exactly X."

In formal verification, we express this as a rule:

public fun deposit_integrity(vault: &mut Vault, amount: u64) {
    // 1. Capture state BEFORE
    let balance_before = vault.get_balance();

    // 2. Execute the function
    deposit_harness(vault, amount);

    // 3. Capture state AFTER
    let balance_after = vault.get_balance();

    // 4. PROVE this holds for ALL possible amounts
    cvlm_assert(balance_after == balance_before + amount);
}

When you run this through , it proves this holds for every valid amount—from 0 to u64::MAX. If it finds even one value where this fails, you get the exact input that breaks it.

---

🏛️ The Three Pillars of Secure DeFi

Through my work verifying DeFi protocols, I've identified three properties that every project must prove:

1. Integrity (Correctness)

"Does this function do exactly what it claims?" For a deposit, this means the right number of shares are minted. For a swap, the correct output is calculated.

2. Solvency (Safety)

"Can users always withdraw their funds?" This is the "last man standing" check. If everyone redeems simultaneously, does the contract have enough assets? Catches inflation attacks and accounting bugs.

3. Monotonicity (Fairness)

"Does this action harm existing users?" A deposit should never decrease the share price for existing LPs. A swap should never decrease the AMM's k value.

---

🔄 The Verification Workflow

Here's how I approach a new protocol:

┌─────────────────┐
│  Read the Code  │
└────────┬────────┘
         │
         ▼
┌─────────────────┐      ┌────────────────────┐
│ Identify State  │ ───► │ What vars matter?  │
└────────┬────────┘      └────────────────────┘
         │
         ▼
┌─────────────────┐      ┌────────────────────┐
│ Define Invariants│ ───► │ What is ALWAYS true?│
└────────┬────────┘      └────────────────────┘
         │
         ▼
┌─────────────────┐
│  Write Rules    │
└────────┬────────┘
         │
         ▼
┌─────────────────┐
│   Run Prover    │
└────────┬────────┘
         │
         ▼
┌─────────────────┐
│ Analyze Results │
└─────────────────┘

---

🚀 What You'll Learn

By the end of this series, you'll be able to:

• ✅ Write integrity rules that catch accounting bugs

• ✅ Prove solvency invariants using induction

• ✅ Use parametric rules to verify entire contracts

• ✅ Track hidden state with ghost variables

---

Next Up: Part 2 - Your First Verification Rule →