Formal Verification of a Sui Move Lending Protocol — Part 2: Proving eMode Borrow Restrictions & Catching a Deposit Limit Bug

How I used Certora's Sui Prover to mathematically prove that only eMode-approved assets can be borrowed — and then turned the prover into a bug-finding weapon that caught a double-subtraction error in the deposit limit check.

✍ 0xTheBlackPanther 📅 Mar 2026 ⏱ 14 min read 🏷 Formal Verification, Sui, Move, Certora, Bug Finding

Previously: eMode Immutability

In Part 1, I proved the first eMode invariant: once an Obligation is created with an eMode group, that assignment can never change. I verified this across all six obligation-mutating functions using Certora's parametric rules, field accessors, and target sanity checks.

But immutability alone isn't enough. An obligation locked to eMode group 1 (stablecoins) is only safe if the protocol actually enforces that restriction — preventing the user from borrowing assets outside their group. That's the second invariant.

The Second Invariant: eMode Borrow Restrictions

From the protocol's requirements:

Invariant: Only assets from the obligation's eMode group can be borrowed. No operation — other than the designated borrow path — should be able to introduce a new debt type into an obligation.

This is a harder property to verify than immutability. We're not checking that a single field stays constant — we're proving that the size of a nested data structure (the debt table inside the obligation) can only grow through one specific, gated code path.

Understanding the Architecture

The borrow flow in this protocol has a layered architecture. Let me trace it from the entry point down:

// The borrow call chain User → entry_point::borrow()
  → market::handle_borrow()
    → emode_registry.borrow_mut_emode(obligation.emode_group(), asset_name)
        // ABORTS if asset not in emode group
    → obligation.try_borrow_asset(amount, borrow_index)
        // Adds new debt type or increases existing debt

The critical gating happens at line 400 of market.move:

// market.move:400 — the eMode gate let emode = self.emode_group_registry.borrow_mut_emode(
    obligation.emode_group(),
    asset_name,
);

And inside borrow_mut_emode in emode.move:

// emode.move:271-278 public(package) fun borrow_mut_emode(
    registry: &mut EModeGroupRegistry,
    group: u8,
    asset: TypeName,
): &mut EMode {
    registry.ensure_group_exists(group);
    let group = registry.groups.borrow_mut(group);
    assert!(group.assets.supports_type(asset), /* abort */);
    group.assets.load_mut_by_type(asset)
}

The assert! on line 275 is the enforcement point. If the asset isn't in the eMode group, the transaction aborts. No new debt is created.

The Verification Strategy

Here's the insight: try_borrow_asset in obligation.move is the only function that can add a new entry to the debt table. It's public(package), meaning only modules within the protocol package can call it. And the only production caller is market::handle_borrow, which gates every borrow through borrow_mut_emode.

So the proof is compositional:

  1. Step 1 (Formal verification): Prove that no obligation-mutating function except try_borrow_asset can increase the debt table size. This covers accrue_interest, deposit_ctoken, withdraw_ctokens, repay_debt, and unsafe_repay_debt_only.
  2. Step 2 (Code-level argument): try_borrow_asset is public(package) and only called from handle_borrow, which enforces eMode group membership via borrow_mut_emode.
  3. Conclusion: New debts can only enter through a path that verifies eMode group membership. The restriction holds.

Part 1 — Writing the eMode Borrow Restriction Spec

The Challenge: Chained Field Accessors

The debt count lives deep inside a nested structure:

// Data path to debt count Obligation
  → .debts : WitTable<ObligationDebts, TypeName, Debt>
    → .table : Table<TypeName, Debt>
      → .size : u64

Three levels of nesting. Each level needs its own field_access.

In the eMode immutability spec, we needed one field_access to read Obligation.emode_group. Here we need three chained accessors to traverse from Obligation down to the table size. This was a new pattern I hadn't used before with the Certora Sui Prover.

The Full Spec

// spec/sources/emode_borrow_restriction.move module spec::emode_borrow_restriction;

use cvlm::manifest::{rule, target, target_sanity, field_access, invoker};
use cvlm::asserts::{cvlm_assert, cvlm_satisfy};
use cvlm::function::Function;

// ---- chained field accessors ----

// Step 1: Obligation → debts (WitTable)
native fun get_debts(
    obligation: &protocol::obligation::Obligation<...>,
): &protocol::wit_table::WitTable<...>;

// Step 2: WitTable → table (Table)
native fun get_debts_table(
    debts: &protocol::wit_table::WitTable<...>,
): &sui::table::Table<TypeName, Debt>;

// Step 3: Table → size (u64)
native fun get_table_size(
    table: &sui::table::Table<TypeName, Debt>,
): &u64;

The invoker and manifest register the same five non-borrow targets (deliberately excluding try_borrow_asset):

// Manifest: targets exclude try_borrow_asset public fun cvlm_manifest() {
    // Wire chained accessors
    field_access(b"get_debts", b"debts");
    field_access(b"get_debts_table", b"table");
    field_access(b"get_table_size", b"size");

    invoker(b"invoke");

    // All obligation-mutating functions EXCEPT try_borrow_asset
    target(@protocol, b"obligation", b"accrue_interest");
    target(@protocol, b"obligation", b"deposit_ctoken");
    target(@protocol, b"obligation", b"withdraw_ctokens");
    target(@protocol, b"obligation", b"repay_debt");
    target(@protocol, b"obligation", b"unsafe_repay_debt_only");

    target_sanity();
    rule(b"no_new_debts_without_borrow");
    rule(b"debt_count_sanity");
}

The core rule is elegant — read the debt table size before and after any non-borrow operation, and assert it doesn't increase:

// The invariant rule public fun no_new_debts_without_borrow(
    obligation: &mut protocol::obligation::Obligation<...>,
    target: Function,
) {
    let size_before = *get_table_size(get_debts_table(get_debts(obligation)));

    // Call any registered target with nondeterministic arguments
    invoke(target, obligation);

    let size_after = *get_table_size(get_debts_table(get_debts(obligation)));

    // Non-borrow operations must never increase the debt count
    cvlm_assert(size_after <= size_before);
}

Notice the chained dereference: get_table_size(get_debts_table(get_debts(obligation))). Each call returns a reference that feeds into the next accessor. The prover resolves this chain at verification time, giving it a precise model of the debt count.

Why exclude try_borrow_asset? Because it should be able to add debts — that's its job. We're proving that nothing else can. The eMode gating of try_borrow_asset is enforced by its sole caller, handle_borrow, which we verify through code-level analysis of the public(package) visibility and the borrow_mut_emode assertion.

Part 2 — The Results

I submitted the spec using a .conf file (a trick I learned to avoid shell quoting issues with the Certora CLI):

// emode_borrow.conf {
    "files": [],
    "rule": [
        "0x0::emode_borrow_restriction::no_new_debts_without_borrow"
    ]
}
// Run from the spec/ directory certoraSuiProver emode_borrow.conf

All green:

Target Function Assertion Sanity Result
accrue_interest PASSED PASSED VERIFIED
deposit_ctoken PASSED PASSED VERIFIED
withdraw_ctokens PASSED PASSED VERIFIED
repay_debt PASSED PASSED VERIFIED
unsafe_repay_debt_only PASSED PASSED VERIFIED
debt_count_sanity — SAT VERIFIED

What this proves: No obligation-mutating function outside of try_borrow_asset can increase the number of debt types on an obligation. Combined with the code-level fact that try_borrow_asset is only callable through handle_borrow (which enforces eMode group membership), this compositionally proves: only assets from the eMode group can be borrowed.

The Compositional Argument

Let me be precise about why this is a complete proof:

The proof structure Formally verified (Certora):
  For all f in {accrue_interest, deposit_ctoken, withdraw_ctokens,
              repay_debt, unsafe_repay_debt_only}:
    debt_count(f(obligation)) ≤ debt_count(obligation)

Code-level (Move visibility + assert):
  try_borrow_asset is public(package)
  → Only callable within the protocol package
  → Only caller: market::handle_borrow
  → handle_borrow calls borrow_mut_emode(obligation.emode_group(), asset)
  → borrow_mut_emode asserts group.assets.supports_type(asset)
  → Aborts if asset not in eMode group

Conclusion: New debts can only be created for eMode-approved assets.

Part 3 — Turning the Prover Into a Bug Finder

After verifying the two eMode invariants, I had a working Certora setup and a growing comfort with the tooling. So I asked a different question: instead of proving that code is correct, could I use the prover to find bugs?

The technique is simple but powerful: write a spec that asserts the code is correct, and if the prover finds a violation, you've found a bug.

The Suspect: deposit_limit_breached

During manual review, I noticed something odd in reserve.move:

// reserve.move:82-90 public(package) fun total_deposit_plus_interest(self: &Reserve): Decimal {
    self.exchange_rate().mul_u64(self.total_supply)
}

public(package) fun deposit_limit_breached(self: &Reserve, increment: u64, limit: u64): bool {
    let total_deposit_plus_interest = self.total_deposit_plus_interest();
    total_deposit_plus_interest.ceil() + increment - self.cash_reserve.ceil() > limit
}

And the exchange rate:

// reserve.move:92-101 public(package) fun exchange_rate(self: &Reserve): Decimal {
    if (self.total_supply == 0) { return float::from_quotient(1, 1) };

    let numerator = self.cash_plus_borrows_minus_reserves();
    let denominator = float::from(self.total_supply);
    numerator.div(denominator)
}

Where cash_plus_borrows_minus_reserves computes debt + cash - cash_reserve.

Do you see it? Let me trace the math:

What exchange_rate returns exchange_rate = (debt + cash - cash_reserve) / total_supply

total_deposit = exchange_rate × total_supply
= debt + cash - cash_reserve

cash_reserve is already subtracted here
What deposit_limit_breached does total_deposit + increment - cash_reserve > limit

= (debt + cash - cash_reserve) + increment - cash_reserve
= debt + cash - 2 × cash_reserve + increment

cash_reserve subtracted TWICE

The Bug: cash_reserve is subtracted once inside exchange_rate() (via cash_plus_borrows_minus_reserves) and then subtracted again explicitly in deposit_limit_breached. The deposit limit is under-enforced by exactly cash_reserve.

The correct check should be:

// CORRECT: total_deposit already excludes cash_reserve
total_deposit_plus_interest.ceil() + increment > limit

// BUGGY: subtracts cash_reserve a second time
total_deposit_plus_interest.ceil() + increment - self.cash_reserve.ceil() > limit

The Impact

When cash_reserve is non-zero (which happens whenever the protocol has accumulated interest from the reserve factor), the deposit limit check is too lenient. Users can deposit up to cash_reserve more than the configured limit allows. The larger the accumulated protocol revenue, the wider the gap.

Part 4 — Proving the Bug Exists with Certora

Manual analysis identified the bug, but I wanted mathematical certainty. So I wrote a spec that asserts the two formulas are equivalent — knowing the prover should produce a counterexample proving they're not.

The Spec

// spec/sources/deposit_limit_double_sub.move module spec::deposit_limit_double_sub;

use cvlm::manifest::{rule, field_access};
use cvlm::asserts::{cvlm_assert, cvlm_satisfy};

// ---- field accessors for Reserve fields ----
native fun get_cash(reserve: &Reserve<...>): &u64;
native fun get_debt(reserve: &Reserve<...>): &Decimal;
native fun get_cash_reserve(reserve: &Reserve<...>): &Decimal;
native fun get_total_supply(reserve: &Reserve<...>): &u64;
native fun get_decimal_raw(decimal: &Decimal): &u256;

The key insight: I needed a get_decimal_raw accessor to read the inner value field from the Decimal struct. This is another chained accessor — first read the Decimal field from Reserve, then read the raw u256 value from the Decimal.

// The bug-detection rule public fun deposit_limit_formulas_equivalent(
    reserve: &Reserve<...>,
) {
    let cash = (*get_cash(reserve) as u256);
    let debt_raw = *get_decimal_raw(get_debt(reserve));
    let cr_raw = *get_decimal_raw(get_cash_reserve(reserve));
    let total_supply = (*get_total_supply(reserve) as u256);

    let wad: u256 = 1_000_000_000_000_000_000;
    let cash_wad = cash * wad;

    // Skip degenerate states
    if (total_supply == 0) return;
    if (cash_wad + debt_raw < cr_raw) return;

    // total_deposit = debt + cash×WAD - cash_reserve
    let total_deposit = debt_raw + cash_wad - cr_raw;

    // CORRECT: use total_deposit directly
    let correct_effective = total_deposit;

    // BUGGY: subtract cash_reserve a second time
    if (total_deposit < cr_raw) return;
    let buggy_effective = total_deposit - cr_raw;

    // This SHOULD FAIL when cash_reserve > 0
    cvlm_assert(correct_effective == buggy_effective);
}

Running the Prover

// deposit_limit.conf {
    "files": [],
    "prover_version": "master",
    "rule": [
        "0x0::deposit_limit_double_sub::deposit_limit_formulas_equivalent",
        "0x0::deposit_limit_double_sub::cash_reserve_positive_reachable"
    ],
    "prover_args": ["-smt_groundQuantifiers true"],
    "server": "production",
    "msg": "deposit_limit_double_sub"
}
certoraSuiProver deposit_limit.conf

The Counterexample

The prover came back in under 2 seconds with a VIOLATED result and a concrete counterexample:

Rule Result Time
deposit_limit_formulas_equivalent VIOLATED 1s
cash_reserve_positive_reachable SAT (VERIFIED) 1s

The prover produced this counterexample:

// Counterexample from Certora reserve = {
    debt.value:         2,
    cash_reserve.value: 1,
    cash:              0,
    total_supply:      1,
}

// Plugging in:
total_deposit = debt + cash×WAD - cash_reserve = 2 + 0 - 1 = 1

correct_effective = 1
buggy_effective   = 1 - 1 = 0

1 ≠ 0 → ASSERTION FAILS

The prover mathematically proved that the two formulas diverge whenever cash_reserve > 0. The smallest counterexample is trivial: cash_reserve = 1 makes the buggy formula evaluate to 0 while the correct formula evaluates to 1. The deposit limit is under-enforced by exactly cash_reserve.

The cash_reserve_positive_reachable sanity check passing as SAT confirms this isn't an academic edge case — any protocol with accumulated interest revenue will have a non-zero cash_reserve, which means the bug is active in production.

What This Proves (and What It Doesn't)

Across this engagement, we verified three distinct properties:

  1. eMode group immutability (Part 1): Proved that emode_group cannot change after obligation creation. Verified across all 6 obligation-mutating functions.
  2. eMode borrow restriction (this post): Proved that only the designated borrow path can add new debt types. Combined with code-level analysis of borrow_mut_emode, this guarantees obligations can only borrow eMode-approved assets.
  3. Deposit limit double-subtraction bug: Used the prover as a bug finder to mathematically confirm that deposit_limit_breached subtracts cash_reserve twice, under-enforcing the limit.

An important pattern: The same tooling that proves correctness can also prove incorrectness. Writing a spec that should pass — and seeing it fail with a concrete counterexample — is one of the most powerful ways to confirm a bug exists. It transforms "I think there's a bug" into "the SMT solver mathematically proved the bug exists."

Key Takeaways

  1. Chained field_access works. You can traverse nested structs (Obligation → WitTable → Table → size) by declaring multiple field accessors. Each one reads one level deep, and you chain them in your rules.
  2. Compositional verification is practical. You don't need to verify everything in one monolithic spec. Prove that only one function can modify a property (formal), then show that function is properly gated (code-level). The combination is rigorous.
  3. Use .conf files for the CLI. The Certora CLI has shell quoting issues with complex --rule arguments. A .conf file (JSON) avoids all of that and is what the prover generates internally anyway.
  4. Formal verification finds real bugs. The deposit limit double-subtraction wasn't hypothetical. The prover found a concrete counterexample in under 2 seconds. Writing specs for "obviously correct" code is how you discover it's not.
  5. prover_args matter. For the deposit limit spec, I needed -smt_groundQuantifiers true to help the SMT solver reason about the arithmetic. Default settings may time out on specs with complex math.
  6. Exclude functions intentionally. In the borrow restriction spec, try_borrow_asset was deliberately excluded from the targets. The spec proves the negative — no other function can do what try_borrow_asset does — and the gating logic is verified separately.

Formal verification isn't just about proving that correct code is correct. It's about finding the code that isn't. The prover doesn't get tired, doesn't skip edge cases, and doesn't make assumptions. If there's a counterexample, it will find it.

Protocol: Compound-style lending market on Sui
Tool: Certora Sui Prover (certora-cli v8.8.1)
Invariant 1: eMode borrow restriction — VERIFIED across 5 target functions
Bug found: deposit_limit_breached double-subtraction — VIOLATED (counterexample produced)
Specs: emode_borrow_restriction.move, deposit_limit_double_sub.move
Part 1: eMode Immutability Verification
Follow: @thepantherplus

Disclaimer: This article is for educational purposes only. The protocol name and specific details have been generalized. The formal verification results shown are from a real engagement, but this article does not constitute security advice. Formal verification proves properties about a mathematical model of the code — it does not guarantee the absence of all bugs. Always combine formal methods with manual review, fuzzing, and testing. If any information here is outdated or incorrect, please reach out on X so I can update this article accordingly.