Sui Prover Goes Open Source: Why Formal Verification Is the Missing Link in Smart Contract Security
In 2025, DeFi lost $3.3 billion to smart contract exploits—despite the fact that most attacked protocols had been audited, some multiple times. The $1.5 billion Bybit breach in February, the $42 million GMX exploit, and countless reentrancy attacks proved an uncomfortable truth: traditional security audits are necessary but not sufficient. When mathematical precision matters, testing edge cases isn't enough. You need to prove them.
This is why the open-sourcing of Sui Prover matters far more than another GitHub release. Built by Asymptotic and now freely available to the Sui developer community, the Sui Prover brings formal verification—the same mathematical technique that ensures flight control systems and processor designs don't fail—to everyday smart contract development. In a landscape where a single overlooked edge case can drain hundreds of millions, the ability to mathematically prove that code behaves correctly isn't a luxury. It's becoming a necessity.
The Audit Paradox: When "Secure" Isn't Secure Enough
The 2025 blockchain security landscape exposed a troubling pattern. According to Halborn's Top 100 DeFi Hacks Report, protocols that had passed rigorous audits still fell victim to exploits. The reasons varied: supply-chain vulnerabilities, access control flaws, subtle mathematical errors in economic models. But the common thread was that traditional code analysis—whether manual review or automated scanning—couldn't catch every possible failure mode.
Consider the Yearn yETH bug and Balancer rounding error exploits. These weren't amateur mistakes. They were subtle mathematical errors that weaponized rounding precision across thousands of potential execution paths. An auditor might spend weeks reviewing code and still miss the one combination of inputs that triggers catastrophic behavior.
The GMX exploit illustrated another dimension of the problem. The vulnerability didn't exist in the core trading logic—it emerged at the boundaries between components, where oracles met margin calculations and liquidation logic interacted with bridge infrastructure. Testing individual components wasn't enough when the failure emerged from their interaction.
This is where formal verification fundamentally differs from traditional security approaches. Instead of checking specific test cases, formal verification mathematically proves that certain properties hold across all possible inputs and execution paths. If you can prove that a vault cannot be drained under any circumstances, you don't need to worry about the obscure edge case your tests missed.
What Formal Verification Actually Does
Formal verification transforms code into mathematical statements and then proves these statements match a formal specification of intended behavior. The process works like this:
First, developers write specifications describing what their code should do—not in programming language, but in a specialized specification language designed for expressing mathematical properties. For smart contracts, these specifications might include statements like "the total supply of tokens never changes unless mint or burn is called" or "user balances can only decrease with the user's explicit authorization."
Then, a prover tool—in this case, the Sui Prover built on the Boogie verification engine and Z3 SMT solver—exhaustively checks whether the code satisfies these specifications across all possible inputs. Unlike testing, which checks specific values, the prover evaluates against all possible inputs simultaneously through mathematical reasoning.
When verification succeeds, you have mathematical proof that the specified properties hold. When it fails, the prover typically provides a counterexample—a specific input that would violate the specification, which often reveals bugs that testing would have missed.
The Move programming language, used by both Sui and Aptos, was designed with formal verification in mind from the beginning. Its resource-oriented model and strong static typing provide a foundation that makes formal verification more practical than in languages like Solidity. The Move Specification Language (MSL) allows developers to express three categories of properties:
- Struct Invariants: What state a structure should maintain throughout its lifetime
- Function Specifications: Pre-conditions, post-conditions, and behavior guarantees for each function
- Global State Specifications: System-wide properties that must hold across all state transitions
Sui Prover: From Internal Tool to Community Resource
Asymptotic initially developed the Sui Prover to support their audit work across protocols building on Sui. As the only formal verification provider on Sui, they needed tools that could go beyond manual review to mathematically verify high-risk areas of client codebases.
The decision to open-source the tool reflects both the maturity of formal verification technology and the recognition that security is a public good. When more developers can access formal verification, the entire ecosystem becomes more secure—which benefits everyone, including security auditors who can focus on higher-level concerns.
The Sui Prover is available on GitHub and can be installed via Homebrew (brew install asymptotic-code/sui-prover/sui-prover). Active development continues, with recent issues opened in January 2026 addressing ongoing improvements.
What makes the Sui Prover particularly valuable is its integration with Sui Move's existing development workflow. Developers can add specifications to their existing code incrementally, verifying critical functions first while gradually expanding coverage. The specifications serve double duty as both safety checks and documentation—anyone reviewing or integrating the contract can read the specs to understand guaranteed behaviors.
Real-World Properties You Can Prove
The power of formal verification becomes concrete when you consider specific properties that can be proven:
Non-Drainable Vaults: For DeFi protocols holding user funds, proving that no sequence of operations can drain the vault without proper authorization eliminates entire categories of attacks. This isn't "we tested many attack vectors"—it's mathematical certainty that drainage is impossible.
Non-Decreasing Share Prices: Yield vaults and liquidity pools often need to guarantee that share prices never decrease unexpectedly (outside of expected slippage). Formal verification can prove this property holds regardless of market conditions or user actions.
Exact Balance Preservation: Token contracts can prove that total supply remains constant across all operations, that transfers move exactly the specified amount, and that no tokens are created or destroyed except through designated functions.
Access Control Guarantees: Proving that only authorized addresses can call privileged functions, regardless of the contract's state or the sequence of previous operations.
Economic Invariants: Complex DeFi protocols can prove properties about their economic models—that liquidity constraints are respected, that collateralization ratios are maintained, that arbitrage loops cannot extract unbounded value.
These aren't theoretical examples. Developers in the Sui ecosystem have already applied formal specifications to verify DeFi contracts including AMMs and leveraged yield farming systems. When these properties are proven rather than assumed, the security posture fundamentally changes.
The Security Landscape Demands Better Tools
The 2025 statistics make the case for formal verification compelling. According to security researchers, off-chain incidents accounted for 56.5% of attacks and 80.5% of funds lost in 2024, but smart contract vulnerabilities remain devastating when exploited. Access control vulnerabilities alone caused $953.2 million in documented damages throughout 2024.
The OWASP Smart Contract Top 10 for 2025 documented over $1.42 billion in collective losses across decentralized ecosystems. Traditional security tools—Mythril for symbolic execution, Echidna for property-based fuzzing, manual audits from firms like OtterSec, Halborn, and MoveBit—address different aspects of the problem. But as protocols become more complex and handle more value, the gaps between these approaches become more dangerous.
CertiK has deployed formal verification techniques to mathematically verify smart contracts, protecting over $300 billion in assets according to their reports. This scale demonstrates both the demand for mathematical security guarantees and the feasibility of applying formal methods to blockchain systems.
The emerging consensus among security researchers is that audits, bug bounties, monitoring, gradual releases, and formal methods should work together as layers of defense. For high-value systems, formal verification of critical invariants is becoming standard practice rather than exceptional rigor.
Why Move Makes Formal Verification Practical
Not all programming languages are equally amenable to formal verification. Solidity's flexibility and the EVM's complexity make formal verification challenging—possible, but requiring significant tooling overhead and expertise.
Move was designed differently. Its resource-oriented model means assets have linear types that can't be duplicated or discarded implicitly. The type system catches entire categories of bugs at compile time that would require runtime checks in other languages. The Move Prover was developed alongside the language, ensuring tight integration between language features and verification capabilities.
This design heritage means the Move standard libraries themselves were formally verified. When you build on Sui or Aptos, you're building on a foundation that has mathematical proofs of correctness—proofs that compound as you layer your own verified code on top.
The practical implication: formal verification on Move requires less specialized expertise than on other platforms. The Sui Prover's documentation, examples, and integration with standard development workflows make it accessible to developers who aren't formal methods specialists. You can learn to write specifications incrementally, starting with simple function contracts and progressing to complex invariants as your understanding deepens.
What This Means for Sui Developers
For developers building on Sui, the open-source Sui Prover creates new possibilities:
Security Differentiation: In a competitive DeFi landscape, proving security properties isn't just risk mitigation—it's a competitive advantage. Users and auditors can verify claims about protocol safety rather than trusting assertions.
Reduced Audit Costs: When critical functions have formal proofs, auditors can focus on higher-level concerns rather than exhaustively testing edge cases. This can reduce audit scope and cost while actually improving security outcomes.
Documentation Quality: Formal specifications are precise documentation that can't become stale. When the spec says a function preserves a certain invariant, that's either provably true or the prover will flag a violation.
Incremental Adoption: You don't need to formally verify everything. Start with the highest-risk functions—those handling withdrawals, collateral, or privileged operations—and expand coverage over time.
The Sui ecosystem already hosts multiple experienced audit firms including MoveBit (pioneers in Move formal verification), Certora, OtterSec, and Zellic. The Sui Prover adds a tool that developers can use directly, without necessarily engaging external auditors for every verification task.
The Broader Trajectory
The open-sourcing of Sui Prover fits a broader pattern of security tooling maturation across the blockchain industry. Formal verification is moving from academic research to production infrastructure, from specialized consultancies to developer-accessible tools.
This trajectory matters because the scale of value secured by smart contracts continues to grow. DeFi protocols collectively manage hundreds of billions in assets. A single bug in a major protocol can cause losses exceeding what traditional software companies face in their entire existence.
The traditional software industry eventually adopted formal methods for safety-critical systems—avionics, medical devices, financial systems. The blockchain industry, where "code is law" and bugs are often irreversible, has even stronger reasons to embrace mathematical verification.
The Sui Prover represents one step in this direction: making formal verification accessible enough that developers actually use it, rather than relegating it to security theater documentation that nobody reads.
Getting Started
For developers interested in exploring formal verification on Sui:
- Install the Sui Prover:
brew install asymptotic-code/sui-prover/sui-prover - Start Small: Add specifications to a single critical function and verify it passes
- Learn the Spec Language: Move Specification Language has excellent documentation for expressing common properties
- Iterate: Expand coverage to more functions and more complex invariants as you build confidence
The investment in learning formal specification pays compound dividends. Once you've verified that lower-level modules are correct, you can build higher-level logic knowing those foundations are mathematically proven.
For an industry that lost billions to preventable bugs in 2025, the question isn't whether formal verification is worth the effort. The question is how quickly the ecosystem can adopt it. The Sui Prover's open-source release removes one barrier—now the knowledge and practice need to follow.
Building secure applications on Sui requires reliable infrastructure that matches your protocol's security standards. BlockEden.xyz provides enterprise-grade RPC endpoints for Sui, Aptos, and 20+ chains with the uptime and reliability that production applications demand. Explore our API marketplace to power your formally verified smart contracts.