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 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.
From the client's requirements:
Invariant: Users cannot switch eMode once obligations are created. This must hold under all operations — including flash loans with re-entrant deposit/borrow in a single Programmable Transaction Block (PTB).
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.
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.
The setup requires Python 3.9+, Java 21+, the Sui CLI, and a Certora account. Installation is straightforward:
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:
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:
Tip: The Certora CLI binary installs to your Python user bin directory (e.g., ~/Library/Python/3.9/bin/certoraSuiProver). Add it to your PATH or use the full path. Note: the binary name is certoraSuiProver without the .py extension, despite what the docs say.
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 Certora spec uses three powerful features from the CVLM library:
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.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.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.Let me break down what happens when the prover runs this:
Getting to a passing result wasn't a straight line. Here are the issues I hit and how I resolved them:
certoraSuiProver.py not foundThe Certora docs reference certoraSuiProver.py, but the actual installed binary is certoraSuiProver (no .py extension). It installs to your Python user scripts directory:
When filtering rules with --rule, you can't use spec::module::rule_name. Certora expects the on-chain address:
This was the most subtle error. The prover returned:
ERROR: Field accessor function 0x0::emode_immutability::get_emode_group must return a reference type.
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:
With certora-cli v8.6.3, jobs were failing silently in ~2 seconds. Upgrading to v8.8.1 resolved prover compatibility issues:
After fixing all the issues, I submitted the final run:
The results came back all green:
| Target Function | Assertion | Sanity | Result |
|---|---|---|---|
accrue_interest |
PASSED | PASSED | VERIFIED |
deposit_ctoken |
PASSED | PASSED | VERIFIED |
withdraw_ctokens |
PASSED | PASSED | VERIFIED |
try_borrow_asset |
PASSED | PASSED | VERIFIED |
repay_debt |
PASSED | PASSED | VERIFIED |
unsafe_repay_debt_only |
PASSED | PASSED | VERIFIED |
emode_sanity |
— | SAT | VERIFIED |
What "VERIFIED" means: The Certora prover mathematically proved that no possible sequence of calls to any obligation-mutating function — with any possible arguments, in any possible state — can change the emode_group field. This isn't test coverage. It's exhaustive formal verification across the entire state space.
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.
This verification mathematically guarantees that:
What it doesn't prove: This verification covers the obligation-level functions. It does not cover potential bugs in the eMode assignment at creation time (e.g., could a user create an obligation with an invalid eMode group?). That's a separate invariant to verify.
field_access returns references. This tripped me up. All field_access native functions must return &T, not T. Dereference with * in your rules.0x0::module::rule, not spec::module::rule.target() line.pip3 install certora-cli --upgrade.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.