Sui Prover — A Smart Contract Developer’s Perspective

How formal verification fits into real-world smart contract development

It’s been about two and a half years since I wrote my first Move smart contract — back in November 2022, around the time the first Sui testnet launched. Move was an intriguing language: mysterious yet oddly familiar, which drew me in. There were very few open-source examples of Move code back then, and almost none that could be considered production-ready. The Sui framework was still under heavy development, with breaking changes landing often — including in the balance and coin modules that we now take for granted. To deepen my understanding of the language, I decided to build a production-worthy implementation of a UniswapV2-style AMM.

Choosing an AMM was a good call — not only because I was already familiar with the UniswapV2 math, but also because that AMM model has a certain symmetry and simplicity that makes the implementation elegant if done right. It’s a great playground to put Move to the test. Plus, UniswapV2 is ubiquitous in DeFi, so I figured it would serve well as an example contract for other developers exploring Move. I finished the implementation and was happy with how it turned out (the code is still up on GitHub: https://github.com/kunalabs-io/sui-smart-contracts/tree/8eb311b1189cdc8cc1a79a22c5874c40d210bea5/amm).

But as I was writing the unit tests, something kept bugging me. There were certain properties that were hard — or even impossible — to fully verify with unit tests alone. These properties had too many edge cases to cover exhaustively, even though they were conceptually straightforward to model.

Take this property, for example: swapping should never return more value than was input (i.e., the pool can’t be drained via swaps). This is easy to reason about at a high level, but with unit tests, you can’t be sure you’ve covered every possible corner case. If you mess up the formula slightly, the tests might still pass for your inputs, but fail in other cases you didn’t account for.

A few more examples:

• Zero-input swaps should always output zero.

• Depositing should never change the asset ratio (price) in the pool.

• Pool balances should be zero iff LP supply is zero.

Making sure the implementation satisfies these kinds of properties is crucial — not just to prevent obvious bugs like fund drain, but also to avoid more subtle issues like corrupted state, bricked contracts, rounding errors, unexpected aborts, or broken access control. While unit tests, fuzzing, and audits help a lot, Move also comes with a powerful formal verification tool: the Move Prover. For properties like the ones above, the Prover can be easier to use and give a much higher — sometimes even absolute — degree of confidence.

Back then, the Prover wasn’t available on Sui, so I shelved the idea and scribbled down my notes for some future time. But the questions stayed with me: Could these properties be formally proven? Could that eliminate some types of tests? Would it make correctness easier to ensure? How hard is it to use the Prover in practice?

Working with Asymptotic

Fast forward to May last year. I was deep into implementing the Kai Leverage smart contracts when Sam reached out to me about Andrei and Cosmin — static verification experts exploring a smart contract verification startup. They were interested in my AMM implementation and the “Prover notes” I’d written. We jumped on a call and started discussing them.

Right away, it was clear that proving those properties wouldn’t be too hard for them. “There’s some challenging arithmetic, but it looks doable,” Andrei said. “Do you have any other smart contracts?”

“Well,” I said, “I’m working on this leveraged yield farming contract, but it’s an order of magnitude more complex — ten times larger, more intricate math, Sui-specific features like dynamic fields, advanced patterns, oracles, external conditions… It might not be as suitable for formal verification.”

But they weren’t fazed. In fact, they dove into that one instead. I wasn’t expecting much, but after seeing their initial results, I was convinced: formal verification isn’t just valuable — it’s practical. Not just for auditing finalized contracts, but also during development.

Vaults, Rounding Bugs, and Real-World Value

I was working on a yield-bearing vault implementation, similar to ERC-4626. It’s a common DeFi pattern where users deposit tokens and receive shares representing ownership in the vault’s assets. As the assets grow, the value of those shares increases. You can find the implementation here.

My main concern wasn’t the math itself — it was the rounding errors. Even if you implement the formulas correctly, rounding in the wrong direction can allow the vault to be drained. The language doesn’t help much here. Robert from OtterSec wrote a great post on this exact issue: https://osec.io/blog/2024-01-18-rounding-bugs. The examples he gives are strikingly similar to how things could go wrong in this vault too.

You can (and should) write unit tests and fuzzing tests to catch this. Fuzzing, in particular, is very applicable here — it gives you statistical confidence. But it’s not perfect. As Robert put it: “I think too many people overindex on how useful the fuzzer mutations are. Throwing a large number of fuzz cycles gives you a very finite increase on the explorable attack surface. If you have a 1/2 trillion chance of hitting a bug, your fuzzer still won’t hit it…”

This is where the Prover shines. Here’s an actual spec for one of the vault functions:

#[spec(prove)]
public fun increase_value_and_issue_x64_spec<T>(
    registry: &mut EquityRegistry<T>, value_x64: u128
): EquityShareBalance<T> {
    requires(registry.inv());

    asserts((registry.underlying_value_x64 as u256) + (value_x64 as u256) <= u128::max_value!() as u256);

    let old_registry = old!(registry);

    let result = increase_value_and_issue_x64(registry, value_x64);

    ensures(registry.inv());
    ensures(registry.price_increase(old_registry));
    ensures(result.value_x64 <= value_x64);
    ensures(registry.underlying_value_x64 == old_registry.underlying_value_x64 + value_x64);
    ensures(registry.supply_x64 == old_registry.supply_x64 + result.value_x64);
    ensures(old_registry.supply_x64 <= registry.supply_x64);
    ensures(old_registry.underlying_value_x64 <= registry.underlying_value_x64);

    result
}

These are powerful assertions. And once you’re familiar with the Prover, writing specs like this isn’t harder than writing unit tests. But the results are far stronger: rather than testing specific values or hoping your fuzzer finds issues, the Prover guarantees these properties hold for all possible inputs.

Once you have specs for low-level modules, you can prove higher-level properties too. Take this function from the Kai Leverage supply pool:

/// Repays the maximum possible amount of debt shares given the balance.
/// Returns the amount of debt shares and balance repaid.
public(package) fun repay_max_possible<T, ST>(
    pool: &mut SupplyPool<T, ST>, shares: &mut FacilDebtShare<ST>, balance: &mut Balance<T>, clock: &Clock
): (u128, u64) {
    let facil_id = shares.facil_id;
    let balance_by_shares =  calc_repay_by_shares(pool, facil_id, shares.value_x64(), clock);
    let shares_by_balance = calc_repay_by_amount(pool, facil_id, balance.value(), clock);
    
    let (share_amt, balance_amt) = if (balance.value() >= balance_by_shares) {
        (shares.value_x64(), balance_by_shares)
    } else {
        // `shares_by_balance <= shares` here, this can be proven with an SMT solver
        (shares_by_balance, balance.value())
    };
    repay(
        pool,
        shares.split_x64(share_amt),
        balance.split(balance_amt),
        clock
    );

    (share_amt, balance_amt)
}

Without diving too deep, this function repays the max possible debt using the given balance and debt shares. It’s part of the liquidation path — so a bug here could mean positions can’t be liquidated, which in turn could lead to bad debt.

I suspected an edge case could cause an abort in shares.split_x64(share_amt), but couldn’t be sure. Fuzz testing gave me some confidence, but not a guarantee. I flagged it to Andrei and Cosmin — and the next day, they had a spec proving it was safe.

Why the Prover Matters

These examples show that the Prover is not just useful for final verification — it’s an asset during development. It can simplify design, replace some types of tests, and give stronger guarantees with comparable effort. Plus, specs are composable: once low-level properties are proven, you can build on them to verify high-level behavior.

That said, it’s not a silver bullet. It won’t replace all tests or audits, especially for economic exploits or protocol-level risks. But it’s a powerful addition to the toolbox.

If you’re curious, check out the specs in the equity, debt, and AMM modules.

Looking Ahead

Working with Asymptotic convinced me: the Prover has a real place in smart contract development. If adopted widely, it could change the way we build and interact with smart contracts.

For example, integrating with contracts that have specs is easier. The spec tells you what the function does, and even guarantees it. If it says “this won’t abort,” you don’t need to code defensively. If it does abort, you know when and why.

This also ties into reliability. Say a function has a 1% chance of aborting. That’s tolerable in isolation — but if your “10x app” composes 10 such contracts, your failure rate jumps to 10%. That’s a problem, especially for backend services or composed protocols.

We already feel this pain in today’s apps. For real reliability, we need guarantees — and the Prover helps us get there.

Another opportunity: formal verification during audits. Specs can serve as tangible artifacts of what was actually checked. This could raise the bar for audit quality and transparency. Smart contracts with specs should be considered higher quality — they’re easier to integrate, more predictable, and safer. Imagine a ‘formal verification checkmark’ on explorers and package managers (such as moveregistry.com) indicating which contracts have verified specs and to what extent. That could be a real trust signal.

Conclusion

Audits, while necessary, could become more effective and measurable. Formal specs would serve as concrete artifacts, clearly showing what properties have been verified. This not only increases trust in the auditing process but also offers a practical way to assess the depth of an audit.

The introduction of formal verification into the CI/CD pipeline could allow us to enforce constraints on dependencies, signaling potential issues before they affect production systems. A ‘formal verification checkmark’ on explorers or package managers could give users a clear indication of a smart contract’s quality and safety. This simple badge would help users trust the contract and contribute to a more secure and reliable ecosystem.

Static verification can help us achieve a level of reliability and security that current practices alone cannot guarantee. By adopting these methods more widely, we can make decentralized applications safer, more reliable, and easier to integrate — making blockchain applications more robust and easier to develop. By embracing these practices, we can move towards a more secure and reliable blockchain ecosystem.

Let’s build toward that future.