I take formal verification seriously, especially when dealing with high-stakes protocols like lending. In this response, I’ll walk you through how I structure Sui Move modules for formal verification of invariant properties in a lending protocol. I’ll also share complete code snippets using spec blocks, assert! checks, and modular design patterns that I personally use to keep lending logic safe and verifiable.

---

✅ 1. I Start With Invariant Modeling

Before writing any code, I define my key invariants — properties that must always hold true. For a lending protocol, some of the most critical are:

• A user cannot borrow more than their allowed LTV (loan-to-value).
• A pool must remain solvent.
• All balances and amounts must remain non-negative.

I write these down and keep them central in how I design the code and specs.

---

🧱 2. I Split the Protocol Into Core Modules

I structure the lending system into smaller modules. Here’s my go-to layout:

- LendingProtocol.move         // High-level flows
- CollateralManager.move       // Handles deposits/withdrawals
- LoanManager.move             // Manages loans
- InterestManager.move         // Interest logic
- SafetySpec.move              // Only for formal specs & invariants

This modularity helps isolate logic and makes it easier to verify individual components.

---

🧩 3. I Use Capabilities and Phantom Types

To control access, I use capabilities and phantom types. For example, I define a LoanAdminCap object that allows only the protocol admin to mint or modify loans.

module LoanManager {

    use sui::object::{Self, UID};
    use sui::tx_context::TxContext;

    struct Loan has key {
        id: UID,
        borrower: address,
        collateral: u64,
        debt: u64,
    }

    struct LoanAdminCap has key {
        id: UID
    }

    public fun init_admin(ctx: &mut TxContext): LoanAdminCap {
        LoanAdminCap { id: object::new(ctx) }
    }

    public fun create_loan(
        admin: &LoanAdminCap,
        borrower: address,
        collateral: u64,
        debt: u64,
        ctx: &mut TxContext
    ): Loan {
        assert!(collateral >= debt * 2, 0x1); // Enforcing LTV (50%)
        Loan {
            id: object::new(ctx),
            borrower,
            collateral,
            debt
        }
    }
}

---

🔍 4. I Annotate With spec Blocks

To enable formal verification, I write spec blocks for functions and modules. Here's how I ensure that the loan's LTV is always safe:

spec module LoanManager {
    const MIN_LTV: u64 = 50;

    spec struct Loan {
        borrower: address,
        collateral: u64,
        debt: u64
    }

    invariant forall loan: Loan {
        loan.collateral >= loan.debt * MIN_LTV / 100
    }

    spec fun create_loan {
        ensures collateral >= debt * MIN_LTV / 100;
    }
}

This allows me to formally prove, using move prover, that no loan violates the collateral ratio.

---

⚠️ 5. I Use assert!() In All Critical Paths

Even before formal verification, I defensively write runtime checks:

public fun repay(
    loan: &mut Loan,
    amount: u64
) {
    assert!(loan.debt >= amount, 0x2); // Can't repay more than owed
    loan.debt = loan.debt - amount;
}

These are essential for catching issues during fuzzing and testing, and serve as hints for formal specs too.

---

🧪 6. I Write Formal Specs With Aborts and Postconditions

I make sure my public functions are spec’d with abort conditions, postconditions, and assertions:

public fun liquidate(loan: &mut Loan, ctx: &mut TxContext) {
    assert!(loan.debt > 0, 0x3);
    assert!(loan.collateral < loan.debt * 50 / 100, 0x4); // Underwater

    loan.debt = 0;
    loan.collateral = 0; // Liquidated
}

spec fun liquidate {
    aborts_if loan.debt == 0;
    aborts_if loan.collateral >= loan.debt * 50 / 100;

    ensures loan.debt == 0;
    ensures loan.collateral == 0;
}

---

🔒 7. I Use Immutable and Minimal Global State

I try not to depend on global mutable state. Instead, I represent each user's loan as an on-chain object:

public fun get_user_loan(borrower: address): Option<Loan> {
    // Look up loan by address
}

This makes it easier to verify and reason about system state.

---

🧯 8. I Build in Emergency and Admin Controls

I always define a pause() or emergency_withdraw() method with a verified capability:

public fun emergency_withdraw(
    admin: &LoanAdminCap,
    loan: &mut Loan
): (u64, u64) {
    let c = loan.collateral;
    let d = loan.debt;
    loan.collateral = 0;
    loan.debt = 0;
    (c, d)
}

spec fun emergency_withdraw {
    ensures result_1 == old(loan.collateral);
    ensures result_2 == old(loan.debt);
    ensures loan.collateral == 0;
    ensures loan.debt == 0;
}

---

🛠️ 9. I Automate Move Prover in CI

Once my code is ready, I run move prove regularly and break builds if specs fail. My CI scripts look like:

#!/bin/bash
move prove --target ./sources --verbose

---

🧰 10. I Use Property-Based Tests Too

I complement my formal specs with fuzz and unit tests. Here's a simple unit test in Sui Move:

#[test]
public fun test_borrow_above_collateral_should_fail() {
    let loan = Loan {
        id: object::new_for_testing(),
        borrower: @0x123,
        collateral: 100,
        debt: 300
    };

    assert!(loan.collateral >= loan.debt * 2, 0x1); // should fail
}

---

✅ Final Thoughts

By combining modular design, assertions, capabilities, and formal spec blocks, I can write lending protocols on Sui that are not only secure but provably safe.

If you're building something serious — especially in DeFi — start formal verification as early as possible. It’s way easier to maintain than to retrofit later.

When I design lending protocols I structure Move modules so the desired invariants are obvious, local, and provable with the Move/Sui verification toolchain (Move Prover / Sui Prover). Below I give the principles I follow, why each helps formal verification, and concrete Move + spec snippets you can adapt for a simple reserve / lending primitive. I include commands and references so you can run the prover against the same patterns I use.

---

High-level best practices (what I do and why)

1. Make the global accounting explicit and localize state. I keep the protocol’s global accounting (total supplied, total borrowed, reserves) in a single well-typed resource (e.g., Reserve or Vault) owned by the module’s address. That lets me state a small number of global invariants (e.g., supply == sum of deposits; total_borrows <= collateral_value * LTV) and have the prover check every entry point preserves them. This pattern is the most direct way to express system-level invariants to the Move Prover / Sui Prover. ([nexio.xyz][2])

2. Use resource typing to enforce ownership and aliasing constraints. Move’s resource semantics reduce aliasing problems. I model account positions as resources (e.g., BorrowPosition / DepositPosition) and transfer/modify them only via module entry functions. That matches Move Prover’s alias-free memory model and makes invariant proofs easier. ([cs.uwaterloo.ca][3])

3. Write small, verifiable functions and separate concerns. I split complex transitions into small, pure/total helper functions where possible and keep the mutable update code minimal (single place that mutates the Reserve). Small functions give the prover smaller proof obligations. The Move Prover works best when proofs are localized. ([cs.uwaterloo.ca][3])

4. Add explicit specs: requires / ensures / aborts_if / loop invariant. I annotate every public entry with pre/postconditions and enumerate abort conditions. This prevents “wildcard” aborts and forces precise reasoning. Use explicit loop invariants when loops are needed. ([nexio.xyz][2])

5. Prove invariants via a spec module global invariant block. For system invariants (e.g., conservation of value), I put them in a spec module { invariant ... } block; the prover will check each module entry preserves them. That’s the canonical way to express “whenever the system is at rest” properties. ([nexio.xyz][2])

6. Use ghost/spec-only state and lemmas. When a property isn’t convenient to track at runtime, I introduce spec-only ghost fields (or spec maps) and lemmas (spec functions) to relate them to runtime state. These do not affect execution but massively simplify proofs. ([aptos.dev][4])

7. Minimize cross-module mutable sharing; verify modules independently. I avoid having multiple modules mutate the same resource. If unavoidable, I create narrow capability resources so that only a small, easily-audited set of functions can change it — making verification tractable.

8. Run the prover routinely and create small lemmas. I run the prover after each refactor, and when it fails I extract small lemmas (spec functions) to help the prover reason about arithmetic/ordering facts. The prover errors often tell you which intermediate claim is missing. ([cs.uwaterloo.ca][3])

---

Minimal illustrative example

Below is a simplified Move module with specs illustrating the above practices. It’s intentionally compact — in a real protocol you’ll expand types (oracles, interest accrual, events, permissions). The snippets show:

• a Reserve resource holding global values,
• per-account Deposit and Borrow resources,
• spec module global invariant,
• entry function specs and aborts_if,
• a small lemma/spec function.

NOTE: different Move Prover and Sui Prover releases have slightly different tooling, but the specification language (MSL) concepts — spec module, spec fun, requires, ensures, aborts_if, invariant — are the same. Use mpm package prove or the Sui Prover flow to run proofs for Sui modules. ([The Sui Blog][1])

address 0xA {
  module Lending {

    use std::signer;
    use std::vector;

    /// --- Runtime types ---
    /// Global Reserve: tracks total deposits and total borrows.
    struct Reserve has key {
      total_deposits: u128,
      total_borrows: u128,
      // reserve_factor, interest_index, etc. omitted for brevity
    }

    /// Each account's deposit resource (one per user per asset in real code).
    struct DepositPosition has key {
      owner: address,
      amount: u128,
    }

    /// Each account's borrow resource.
    struct BorrowPosition has key {
      owner: address,
      amount: u128,
    }

    /// --- Initialization ---
    public fun init(owner: &signer) {
      assert!(!exists<Reserve>(@0xA), 1);
      move_to(owner, Reserve { total_deposits: 0u128, total_borrows: 0u128 });
    }

    /// --- Specification (Move Spec Language) ---
    spec module {
      /// Global invariant: total_deposits >= total_borrows
      /// (example: protocol should never have negative liquidity; adapt for actual invariants).
      invariant exists<Reserve>(@0xA) ==> 
        (borrow_expr());

      /// helper spec function used in invariant
      spec fun borrow_expr(): bool {
        // In MSL you would write the actual expression relating global fields:
        // Reserve::total_deposits(@0xA) >= Reserve::total_borrows(@0xA)
        // Written here in pseudocode for clarity; replace with real expressions in your code.
        true
      }
    }

    /// --- Public entry: deposit ---
    public entry fun deposit(user: &signer, amt: u128) {
      // runtime checks
      assert!(amt > 0, 2);

      // concrete update: add deposit
      deposit_internal(signer::address_of(user), amt);
      // no explicit spec here? below we add the spec block for this function
    }

    spec deposit {
      /// precondition: amt must be > 0
      requires amt > 0;
      /// postcondition: total_deposits increased by amt
      ensures exists<Reserve>(@0xA) ==>
        Reserve::total_deposits(@0xA) == old(Reserve::total_deposits(@0xA)) + amt;
      /// ensure allowance: invariant preserved
      ensures borrow_expr();
    }

    fun deposit_internal(user_addr: address, amt: u128) {
      // create or update user's deposit
      if (!exists<DepositPosition>(user_addr)) {
        move_to(&signer::new(user_addr), DepositPosition { owner: user_addr, amount: amt });
      } else {
        let mut pos = borrow_global_mut<DepositPosition>(user_addr);
        pos.amount = pos.amount + amt;
      }
      let reserve_ref = borrow_global_mut<Reserve>(@0xA);
      reserve_ref.total_deposits = reserve_ref.total_deposits + amt;
    }

    /// --- Public entry: borrow ---
    public entry fun borrow(user: &signer, amt: u128) acquires Reserve, DepositPosition {
      // Preconditions and abort reasons must be enumerated
      assert!(amt > 0, 3);
      // e.g., check LTV, collateral sufficiency (omitted calculation details)
      // Then update
      borrow_internal(signer::address_of(user), amt);
    }

    spec borrow {
      requires amt > 0;
      /// abort if insufficient collateral or if borrow would break invariant
      aborts_if !can_borrow(amt);
      ensures exists<Reserve>(@0xA) ==>
        Reserve::total_borrows(@0xA) == old(Reserve::total_borrows(@0xA)) + amt;
      ensures borrow_expr(); // preserve the module invariant
    }

    spec fun can_borrow(amt: u128): bool {
      // We specify the condition the program checks at runtime.
      // In full code this will reference collateral valuations and LTV ratios
      true
    }

    fun borrow_internal(user_addr: address, amt: u128) acquires Reserve {
      // update borrow position
      if (!exists<BorrowPosition>(user_addr)) {
        move_to(&signer::new(user_addr), BorrowPosition { owner: user_addr, amount: amt });
      } else {
        let mut bpos = borrow_global_mut<BorrowPosition>(user_addr);
        bpos.amount = bpos.amount + amt;
      }
      let reserve_ref = borrow_global_mut<Reserve>(@0xA);
      reserve_ref.total_borrows = reserve_ref.total_borrows + amt;
      // in production you'd also transfer coin, update indexes, emit events...
    }

    /// --- Example of a spec-only lemma used to help the prover ---
    spec fun lemma_deposits_nonneg() {
      // no runtime effect — used to prove arithmetic facts if needed
    }
  }
}

Notes on the snippet

• The spec module area is where I declare module-level invariants the prover will check on every entry. In a real lending protocol the invariant might be total_deposits >= total_borrows + protocol_reserve or a more complex invariant relating collateral valuations and borrow limits. Use precise numeric relations and oracle valuations. ([nexio.xyz][2])
• For all public entry functions I include spec blocks with requires, ensures, and aborts_if where applicable — this avoids unspecified failure modes and helps the prover produce actionable errors. ([cookbook.starcoin.org][5])
• Ghost/spec fun helpers (like can_borrow and lemmas) are essential: they let me express and reuse intermediate proof facts without polluting runtime state. ([aptos.dev][4])

---

Practical verification workflow I follow

1. Write the code + specs locally. I add spec blocks as I implement features (pre/postconditions, loop invariants, module invariants). Small, incremental specs help catch issues early. ([nexio.xyz][2])

2. Run the prover (Move Prover / Sui Prover). Typical commands depend on your setup. For Move Prover typical flows use the mpm tool (mpm package prove) or the Sui Prover pipeline described in Sui docs/blog. The prover output directs you to missing lemmas or places where it needs additional assertions. ([The Sui Blog][1])

3. Iterate with lemmas and smaller invariants. When a verification obligation fails I extract the missing step into a spec fun lemma and proof it with assert / assume in spec-only context until the prover succeeds. Over time you build a library of useful lending lemmas (monotonicity of totals, bounds after operations, invariants across reentrancy-free calls).

4. Limit complexity in single functions. If a function gets many branches or complex loops, I refactor it into smaller private helpers with their own specs. This makes proof obligations modular and much faster to discharge. ([cs.uwaterloo.ca][3])

---

Specific anti-patterns I avoid (because they break verification)

• Underspecified aborts. Don’t let functions abort without enumerating why — prover will report “possible abort” errors. Always use aborts_if or prove the function cannot abort.
• Implicit global mutation across many modules. If multiple modules can mutate the same resource, proofs become global and brittle.
• Mixing numeric scales / implicit units. Values should use a single unit or carry scaling metadata; mismatched units lead to unprovable lemmas.
• Heavy use of loops without invariants. If you must loop, write precise loop invariants; otherwise the prover won’t be able to build the inductive argument. ([nexio.xyz][2])

---

Example: an invariant you’ll actually want in a lending protocol

A typical provable invariant is value conservation: the protocol’s recorded liquidity equals the sum of account positions (plus reserves). In MSL you’d express it as a spec module invariant that references Reserve::total_deposits and the sum of all DepositPosition resources (or a spec-only aggregator if scanning all accounts is impractical). The Move Prover supports such global invariants and will attempt to verify each public entry preserves them. See examples and explanation in Move Prover docs and Sui Prover announcement. ([nexio.xyz][2])

---

Tooling & references (what I use)

• Sui Prover announcement / guide — Sui’s blog and docs for the Sui-specific prover integration (start here for Sui-specific CLI and integrations). ([The Sui Blog][1])
• Move Prover papers & user guides — describes MSL, spec statements, loop invariants, and verification strategies used across Move ecosystems. Essential reading. ([cs.uwaterloo.ca][3])
• Tutorials / community posts — good quickstarts that show mpm package prove, common spec idioms, and how to handle aborts and loops. ([movebit.xyz][6])

---

Final tips from the trenches (practical heuristics)

• Start with a tiny invariant (e.g., total_deposits >= total_borrows) and get that proving first; then progressively add richer invariants (LTV, liquidation invariants, interest index invariants). Prove incrementally. ([nexio.xyz][2])
• Keep a library of spec-only helpers / lemmas (monotonicity, nonnegativity) and reuse them across modules. They pay back huge verification time. ([cs.uwaterloo.ca][3])
• Automate prover runs in CI so each PR verifies the module invariants — you’ll catch subtle regressions early. ([cs.uwaterloo.ca][3])

To set up your Sui Move modules for formal verification in lending protocols, you should design your code with clear, well-defined invariants and keep your logic modular and simple. Break down complex behaviors into smaller functions with explicit input and output, making it easier to verify each part separately. Use strong type systems and explicit state transitions to prevent invalid states. Document and encode key invariants—like total collateral ratios or debt limits—as assertions or specifications within your Move modules. Avoid side effects or hidden state changes that complicate reasoning about the code. Leveraging formal verification tools that support Move, you can write properties and proofs directly tied to your module’s functions and states. This approach helps ensure your lending protocol maintains safety guarantees like preventing under-collateralized loans or ensuring consistent accounting.

Read more: https://docs.sui.io/build/move#formal-verification-and-safety

To enable formal verification of invariants in your Sui Move modules for lending protocols, you should structure your code clearly and keep logic simple and modular. Design functions with explicit inputs and outputs, making it easier to verify each part independently. Define key invariants—such as collateral ratios or debt limits—as assertions within your code to ensure critical conditions are always met. Use strong types and explicit state transitions to avoid invalid states or hidden side effects that complicate verification. Writing clear specifications and leveraging formal verification tools compatible with Move lets you prove safety properties like preventing under-collateralization and ensuring correct accounting throughout your protocol.

Read more: https://docs.sui.io/build/move#formal-verification-and-safety