Sui Prover: Bringing Formal Verification to Sui

Formal verification is no longer out of reach—it’s now accessible to all developers building on Sui. The Sui Prover, built by Asymptotic and now available to the community, brings this powerful capability to everyday development on Sui. 

Designed to bring stronger guarantees to smart contract development, the Sui Prover helps improve the safety, reliability, and clarity of onchain logic by enabling developers to formally prove that their code behaves as intended.

With the Sui Prover, developers can mathematically verify that their smart contracts behave as intended, even in some extreme edge cases. It allows properties like non-drainable vaults, non-decreasing share prices, or exact token balance preservation to be proven rather than assumed, helping prevent bugs that traditional testing might miss.

The importance of formal verification

Formal verification is a method of proving that a program behaves as intended across all possible inputs and states. Unlike testing, which checks behavior in specific scenarios, formal verification evaluates whether a piece of code always satisfies a defined set of conditions. These conditions, called specs, are written alongside the code and describe its expected behavior in precise, logical terms. If the code violates any of these specs under any circumstances, a prover employing formal verification will surface it.

In the context of smart contracts, where edge cases can lead to irreversible loss of funds or broken logic, being able to rule out entire classes of bugs with this level of rigor is especially valuable. It means developers can assert things like: “this function will never cause an overflow,” or “this vault’s share price can never decrease,” and be sure those properties hold in all cases, not just in those covered by tests.

While the benefits are clear, formal verification has traditionally been difficult to apply in practice. In many blockchain environments, verification tools are limited, hard to integrate into normal workflows, or require working around language-level constraints. By contrast, Move was designed from the ground up with safety and verifiability in mind. Its resource-oriented model and strong static typing make it a natural fit for formal methods, enabling developers to express and verify key properties of their smart contracts more directly.

The Sui Prover builds on these foundations to offer a practical, developer-friendly tool for Move on Sui. With it, developers can write specs that capture properties they care about—like correct rounding, non-drainable pools, or guaranteed balance preservation—and prove those properties. Once verified, these specs serve not just as safety checks, but also as readable documentation for anyone integrating or auditing the contract.

Improving the developer experience on Sui

The Sui Prover was initially developed by Asymptotic to support formal verification in their audit work across protocols built on Sui. By open-sourcing the tool, they’ve made this capability widely available, and it’s already having a meaningful impact on how developers write, reason about, and secure smart contracts on Sui.

Among the early adopters of the Sui Prover is Krešimir Klas (a.k.a. kklas), a developer who recently shared a detailed look at how formal specs helped verify critical safety properties in two of his DeFi contracts: an AMM and a leveraged yield farming system. In both cases, traditional testing methods surfaced limitations. With unit tests, there’s always a risk of missing edge cases; with fuzzing, the statistical coverage might still fall short. But by expressing the intended behavior of a function through a formal spec and using the Sui Prover to verify it, kklas was able to gain a level of confidence that would be hard to reach otherwise.

These specs don’t just help during audits or post-launch hardening. They’re useful in active development too. For example, when implementing a vault module that issues shares on deposit, the prover was used to confirm that the share price only increases over time and that rounding behavior couldn’t be exploited to drain value. In more complex modules, such as liquidation logic within a leveraged yield protocol, specs helped ensure edge cases wouldn’t cause critical functions to unexpectedly abort. The result was not only safer code, but clearer logic, because knowing what can’t go wrong makes it easier to reason about what should happen.

Building toward safer, more reliable code

The Prover works by evaluating the specs against all possible inputs, rather than checking specific values. This brings a fundamentally different level of certainty. And once low-level modules are verified, that assurance compounds, developers can then build higher-level logic on top, while leaning on guarantees that have already been proven.

While formal verification can’t replace audits or eliminate the need for strong protocol design, it can make both more effective. Audits can be clearer about what properties have been formally checked. Specs themselves serve as documentation, making smart contracts easier to integrate by clearly stating behavior at the function level, whether a call might abort, whether balances are preserved, and so on. This has implications not just for safety, but also for reliability, especially as more complex apps are built on Sui.

What comes next

The Sui Prover is available today, open source, and integrated into Asymptotic’s audit process. Developers are encouraged to explore the repository and try it out in their own code. For more technical information, explore the Sui Prover’s docs, join the Telegram channel, and reach out to those using it already.

As more contracts adopt formal specs, the entire Sui ecosystem stands to benefit from developers building with clearer guarantees to users interacting with safer, more reliable apps. By making smart contracts easier to trust, the entire ecosystem moves forward.