Formal Verification of a Sui Move Lending Protocol Using Certora Prover

How I mathematically proved that an eMode group assignment is immutable after obligation creation in a Sui DeFi lending protocol — using Certora's Sui Prover, parametric rules, and field accessors.

The Protocol: A Lending Market on Sui

The target was a Compound-style lending protocol built in Move on Sui. Users deposit collateral, borrow assets, earn interest — the usual DeFi primitives. But this protocol had an additional layer of sophistication: eMode groups (efficiency mode), similar to Aave V3's e-mode.

Each eMode group defines a curated set of correlated assets (e.g., stablecoins, or LST variants) with optimized risk parameters — higher collateral factors, tighter liquidation thresholds, and dedicated borrow caps. When a user enters the market, their Obligation is assigned an eMode group, and all their subsequent borrows and deposits are restricted to assets within that group.

The protocol's security depends on a critical invariant: once an Obligation is created with an eMode group, that assignment must be permanent. If a user could switch eMode groups mid-lifecycle, they could borrow assets from one risk tier using collateral parameters from another — effectively bypassing the protocol's risk engine.

The Invariant

From the client's requirements:

This isn't something you can test with unit tests or fuzzing. A unit test checks specific scenarios. A fuzzer explores random paths. But neither can guarantee that no possible sequence of operations across all possible inputs will ever violate the property. For that, you need formal verification.

Background: My Formal Verification Journey

This wasn't my first formal verification engagement. I previously did a formal verification audit with Pashov Audit Group for the SpiceNet Delegate contracts. That project was in Solidity, so we used Certora's EVM prover — a mature, well-documented tool with years of battle-testing on Ethereum protocols.

Move on Sui was a different story. The ecosystem for formal verification tooling was much thinner. After digging around, I found two options:

I went with Certora's Sui Prover. The parametric rule support was the deciding factor — I could write a single rule that automatically verifies the invariant against every obligation-mutating function, rather than manually writing a separate check for each one. The cloud-based execution and web dashboard for inspecting counterexamples were bonuses.

Part 1 — Setting Up Certora for Sui Move

Prerequisites

The setup requires Python 3.9+, Java 21+, the Sui CLI, and a Certora account. Installation is straightforward:

Creating the Spec Package

Certora specs live in a separate Move package that imports both the contract under verification and the cvlm specification library. I created a spec/ directory alongside the protocol:

The Move.toml wires together the protocol, Certora's CVLM library, and Sui platform summaries:

Smoke Test

Before writing any real invariants, I created a minimal smoke test to verify the toolchain works end-to-end:

Build locally with sui move build, then submit to the Certora cloud prover:

Part 2 — Writing the eMode Immutability Invariant

Understanding the Attack Surface

Before writing any spec, I needed to identify every function that takes a mutable reference to Obligation. These are the only functions that could potentially mutate emode_group:

These six functions are the complete attack surface. If none of them modify emode_group, then no operation — including any composition of operations within a PTB or flash loan callback — can change it.

The Spec: Three Key Concepts

The Certora spec uses three powerful features from the CVLM library:

1. field_access — Reading private fields. The emode_group field has no public setter, and its getter is public(package) (not callable from our spec module). Certora's field_access manifest function lets us declare a native accessor that the prover wires directly to the struct field.
2. invoker + target — Parametric rules. Instead of writing 6 separate rules (one per function), we register all 6 functions as targets and declare an invoker. The prover then generates sub-rules for every (rule × target) combination automatically.
3. target_sanity — Vacuity checks. A rule that passes because its preconditions are unsatisfiable is vacuously true — it proves nothing. target_sanity() auto-generates sanity checks that confirm each target is actually reachable.

The Full Spec

Let me break down what happens when the prover runs this:

Part 3 — Debugging the Prover

Getting to a passing result wasn't a straight line. Here are the issues I hit and how I resolved them:

Issue 1: certoraSuiProver.py not found

The Certora docs reference certoraSuiProver.py, but the actual installed binary is certoraSuiProver (no .py extension). It installs to your Python user scripts directory:

Issue 2: Rule names must be fully qualified with address

When filtering rules with --rule, you can't use spec::module::rule_name. Certora expects the on-chain address:

Issue 3: field_access must return a reference type

This was the most subtle error. The prover returned:

The fix: field_access native functions must return &T, not T. I changed the return type from u8 to &u8 and added dereference operators (*) in the rules:

Issue 4: CLI version mismatch

With certora-cli v8.6.3, jobs were failing silently in ~2 seconds. Upgrading to v8.8.1 resolved prover compatibility issues:

Part 4 — The Results

After fixing all the issues, I submitted the final run:

The results came back all green:

The rule_not_vacuous_tac (sanity) checks passing for every target confirms these aren't vacuous proofs — the prover actually explored meaningful, reachable states. And emode_sanity passing as SAT confirms that obligations with non-zero eMode groups exist, so we're not verifying dead code.

What This Proves (and What It Doesn't)

This verification mathematically guarantees that:

1. No single operation changes emode_group. Deposit, withdraw, borrow, repay, interest accrual — none of them touch the field.
2. No composition of operations changes it either. Since each individual operation preserves the invariant, any sequence of operations in a PTB (including flash loan callbacks) also preserves it. Compositionality is free.
3. The proof is not vacuous. The sanity checks confirm the prover explored reachable states with non-trivial eMode assignments.

Key Takeaways for Move Security Researchers

1. Certora now supports Sui Move. The tooling is new but functional. If you've used Certora for Solidity, the mental model transfers — rules, targets, parametric verification — with Move-specific syntax differences.
2. field_access returns references. This tripped me up. All field_access native functions must return &T, not T. Dereference with * in your rules.
3. Rule names use the address, not the module name. The CLI expects 0x0::module::rule, not spec::module::rule.
4. Parametric rules are the killer feature. One rule verifying an invariant across ALL functions is more valuable than six individual rules. It's future-proof — if someone adds a 7th obligation-mutating function, just add one target() line.
5. Keep your CLI version current. Older CLI versions can fail silently with non-descriptive errors. Always upgrade to the latest: pip3 install certora-cli --upgrade.
6. Formal verification complements manual auditing. It doesn't replace reading the code. I found the protocol's architecture, identified the invariant, and understood the attack surface through manual review. Formal verification then proved what manual review suspected.

Formal verification on Sui Move is no longer theoretical — it's practical, accessible, and powerful. If you're auditing lending protocols, the exchange rate, cToken supply, and eMode invariants are the first properties worth proving.

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. The Certora Sui Prover is relatively new tooling; verify its current capabilities and limitations before relying on it for production audits. If any information here is outdated or incorrect, please reach out on X so I can update this article accordingly.