This repository is a practical, opinionated guide to formally verifying Move-based protocols on Sui using the Certora Prover.
It’s built for engineers who want to go from “I’ve heard of formal verification” to “I can prove non-trivial safety properties on real DeFi protocols.”
Just specs, rules, invariants, and battle-tested patterns.
The content evolves from fundamentals to advanced verification patterns, using real DeFi primitives as case studies:
- Vaults
- AMMs (e.g., Uniswap V2–style constant product pools)
- CLAMMs (e.g., Uniswap V3–style concentrated liquidity)
- Lending protocols
🚧 Work in progress: Vault and AMM specs are complete. CLAMM and lending protocol specifications are currently in progress.
Before diving into the spec code, read the write-ups in the Blog/ folder. They explain the reasoning behind the rules and invariants.
Suggested order:
-
Why Formal Verification?
-
Your First Rules
-
Thinking in Invariants
-
Advanced Prover Features
Ghost variables, summaries, abstraction patterns, loop handling.
If you’re new to FV, start there. If you already know what an invariant is, jump into the specs and break things.
To illustrate the depth of this work without exposing proprietary mechanics (the "alpha"), here is a high-level look at how we structure advanced rules for Vaults and AMMs.
Real contracts take concrete objects like Coin<SUI>. Because the Certora Prover explores symbolic values to cover infinite permutations, we utilize harnesses to manipulate symbolic resources safely within the verification environment.
Here is an example proving Deposit Integrity for a Vault. It ensures that the vault balances and shares correctly reflect the deposited amount.
// The Harness bridges symbolic execution with real contract parameters
fun deposit_harness(vault: &mut Vault, amount: u64): u64 {
let mut ctx = tx_context::dummy();
let deposit_coin = coin::from_balance<SUI>(
balance::create_for_testing(amount),
&mut ctx
);
let lp_coin: Coin<VAULT> = vault.deposit(deposit_coin, &mut ctx);
let shares_minted = coin::value(&lp_coin);
balance::destroy_for_testing(coin::into_balance(lp_coin));
shares_minted
}
// The Integrity Rule:
public fun deposit_integrity(vault: &mut Vault, amount: u64) {
// Capture pre-state with offset for precision safety
let assets_before = vault.total_assets() + 1000000000;
let shares_before = vault.total_shares() + 1000000000;
cvlm_assume_msg(amount >= 1000, b"Amount must be >= MIN_LIQUIDITY");
// Execute the symbolic harness
let shares_minted = deposit_harness(vault, amount);
// Capture post-state
let assets_after = vault.total_assets() + 1000000000;
let shares_after = vault.total_shares() + 1000000000;
// Assert actual values matched expected linear additions
cvlm_assert(assets_after == assets_before + amount);
cvlm_assert(shares_after == shares_before + shares_minted);
// Monotonicity check via cross-multiplication to avoid precision loss
if (shares_before > 0) {
cvlm_assert(shares_minted > 0);
cvlm_assert((assets_after * shares_before) >= (assets_before * shares_after));
}
}We pair rules like the one above with cvlm_satisfy equivalents to prevent vacuous truths—proving properties about code that actually always reverts.
Verifying functions in isolation isn't enough to guarantee system safety. Instead, we establish System Invariants that must hold across any state transition, tested using mathematical induction.
For example, checking the core Solvency Invariant of a Vault (accounting for virtual offsets to protect against inflation attacks):
public fun solvency_check(vault: &mut Vault) {
// 1. Snapshot State & Assume Inductive Hypothesis
cvlm_assume_msg(
vault.total_assets() >= vault.total_shares(),
b"Vault must be solvent at start"
);
let total_supply = vault.total_shares();
let total_assets = vault.total_assets();
// 2. Calculate liabilities using the 'redeem' formula with u128 to prevent overflow
let offset = 1_000_000_000u128;
let supply_u128 = total_supply as u128;
let assets_u128 = total_assets as u128;
// Required if everyone redeems
let numerator = supply_u128 * (assets_u128 + offset);
let denominator = supply_u128 + offset;
let required_assets = (numerator / denominator) as u64;
// 3. ASSERT: The vault must ALWAYS have enough cash to pay everyone
cvlm_assert(required_assets <= total_assets);
}As protocols scale out to 20+ operations, writing an integrity invariant rule per function is non-scalable.
To solve this we use Parametric Rules: a single rule that abstracts over the function being called. By using a native invoke hook dynamically bound to a list of function targets in our configuration manifest, the prover tests the property against all registered functions automatically.
If you introduce a new feature that unexpectedly allows dilution or insolvency, the universal Parametric Rule catches it immediately.
// 1. We define standard Wrappers for all features
fun wrapper_deposit(...) { ... }
fun wrapper_redeem(...) { ... }
// 2. We define a Native Invoker
native fun invoke(target: Function, vault: &mut Vault, amount: u64);
// 3. One Parametric Rule to bind them all
public fun parametric_invariant(vault: &mut Vault, amount: u64, target: Function) {
cvlm_assume_msg(amount >= 1000, b"Amount must be >= MIN_LIQUIDITY");
cvlm_assume_msg(vault.total_assets() >= vault.total_shares(), b"Solvent start");
let assets_before = vault.total_assets() as u128 + 1000000000;
let shares_before = vault.total_shares() as u128 + 1000000000;
// EXECUTE arbitrary function Target dynamically
invoke(target, vault, amount);
let assets_after = vault.total_assets() as u128 + 1000000000;
let shares_after = vault.total_shares() as u128 + 1000000000;
// The share-price invariant MUST be respected regardless of what executed
cvlm_assert((assets_after * shares_before) >= (assets_before * shares_after));
}Automated Market Makers absolutely rely on the k invariant (x * y = k). Our specifications mathematically ensure that even under extreme symbolic stress and slippage, pool health is strictly preserved relative to fees.
public fun amm_swap_a_integrity(pool: &mut Pool<T1, T2>, amount_in: u64) {
// Filter extreme micro-dust that could pollute floating-point bounding
cvlm_assume_msg(amount_in > 1000, b"Input > dust");
// Snapshot Pre-State
let (a_before, b_before, _) = uniswapV2::pool_balances(pool);
let k_before = (a_before as u128) * (b_before as u128);
// Execute swap through formalized harness architecture
let (amount_in_ret, amount_out_ret, snap) = swap_a_harness(pool, amount_in);
// Evaluate Post-State
let (a_final, b_final, _) = uniswapV2::pool_balances(pool);
// Core Constant Product Assertion computation
let k_after = (a_final as u128) * (b_final as u128);
// PROOF: The pool's total value equivalent MUST NOT DECREASE
// after the swap fee calculation is resolved.
cvlm_assert(k_after >= k_before);
}Beyond basic deposits and withdrawals, enterprise-grade Vaults must be protected against multi-step manipulation attacks. Here are just a few advanced Vault invariants we prove.
Concept: A common attack vector involves warping Exchange Rates by inflating Vault assets using flash-loans right before a transaction, then deflating them. We mathematically prove that taking zero-duration, zero-cost loans against the vault never artificially scales share redemptions.
[REDACTED] // Spec code leveraging Parametric execution bounds to prove share-prices remain rigid during single-block, zero-cost arbitrage calls.Concept: If a Vault charges performance fees or management fees, we must prove that the fee system is mathematically capped. Even if compounding math bugs out, the protocol can never siphon principal funds from LPs into the treasury—fees are mathematically constrained to be a fractional subset of pure profit.
[REDACTED] // Spec code utilizing Inductive properties to assert that over infinite compounding steps, protocol_shares <= max_fee_rate * total_generated_profit.Concept: We prove that the total Vault supply equals the exact sum of every individual user's balance. This proves that no internal mechanism can mint "ghost shares" or burn shares un-accounted for, ensuring total accounting integrity across all ledgers.
[REDACTED] // Spec code using mathematical aggregations (often aided by Ghost variables) to prove sum(user_shares) == total_shares is strictly preserved.Complex Liquidity pools (especially Concentrated ones) have massive surface areas for bugs relative to Uniswap V2. We prove invariants protecting the core engines from sophisticated slippage and rounding exploits.
Concept: AMMs rely on amountOutMinimum parameters. We mathematically prove that, regardless of how maliciously the pool is manipulated beforehand, if a transaction confirms, the user is mathematically guaranteed to receive at least their minimum out, or the swap reverts. The engine physically cannot execute a bad trade.
[REDACTED] // Spec code asserting that returning amount_out unconditionally >= amount_limit on all successful paths.Concept: In multi-hop swaps or when calculating optimal routes, the math can sometimes overflow or round down aggressively. We prove that single-hop swaps vs multi-hop swaps maintain logical routing integrity, and that rounding errors never compound to steal user funds or break the k invariant across multiple hops.
[REDACTED] // Spec code proving path sequence commutativity and bounded rounding errors.Concept: When massive "whale" trades hit an AMM, they generate significant fees but also shift the price curve drastically. We prove that the fees properly accrue to the Liquidity Providers and that no sequence of massive trades can mathematically dilute the proportionate claim of an existing, passive LP.
[REDACTED] // Spec code using Ghost Variables to track LP proportionate ownership across massive curve manipulations.In production-grade Move protocols, state mutations and mathematical calculations can become too complex or hidden for standard invariant checks. To solve this, we employ Ghost States and Function Summaries.
Concept: Sometimes it is critical to verify properties involving data that isn't stored on-chain. For example, proving that "no hidden mint operations ever occurred" or that "fee revenue exactly matches fee events".
Ghost variables shadow on-chain state but exist purely in the verification layer. By creating a GhostVault that strictly tracks authorized deposits and withdrawals, we can assert at the end of any transaction that the actual, physical total_shares perfectly matches our authorized GhostVault.expected_shares. If any hidden code path or exploit modifies shares without authorization, the Ghost State invariant will catch the discrepancy immediately.
[REDACTED] // Spec code defining native ghost structures and tracking expected state versus actual state post-execution.Concept: Real-world DeFi contracts often involve intense mathematical loops (e.g., compounding interest calculated per-second over years, or iterative tree traversals). These operations can cause the mathematical solver to time out (state explosion). We solve this using Function Summaries: we replace the complex, time-consuming math loop with a mathematically rigorous abstraction. We tell the prover: "Assume this function returns a symbolic value, but constrain that value so it is mathematically logical (e.g., interest must be positive and bounded by the principal)." This allows us to instantly verify the surrounding protocol logic without getting choked by the microscopic permutations of a single math library.
[REDACTED] // Spec code abstracting heavy compounding math into bounded, non-deterministic summaries within the manifest.