Lending protocols look simple: deposit, borrow, repay, liquidate. But the properties that keep a lending protocol solvent don't live inside any single function. They emerge from how operations compose. A deposit that's safe on its own can create insolvency when it interacts with a liquidation under certain conditions. The bugs that matter are in those interactions and finding them requires proving things about the system as a whole.

The team here at Certora formally verified Suilend on Sui by writing and proving system-level invariants, properties that must hold across every operation, every reachable state, and every possible sequence of calls. We organized the verification around three categories: solvency, account health, and liquidation.

While none of the vulnerabilities found in Suilend were critical or put funds at immediate risk, their subtlety and intricacy speak to the depth of the formal verification and are a testament to Suilend's existing security.

Proving Solvency

The cToken ratio has to stay >= 1. If it doesn't, depositors can't fully redeem. We proved it holds, that no user action can push it down, and that the reserve's internal bookkeeping never claims more liquidity than actually exists on-chain.

A double-rounding bug came out of the cToken ratio work (M-01). The minting functionality had two truncations stacked so the depositor got slightly more shares than their deposit was worth. Small per transaction, but it compounds. Every deposit was quietly diluting existing holders.

Account Health

A healthy position should stay healthy after any user operation, as long as prices and interest haven't moved. We proved that, along with the expected LTV monotonicity (up with debt, down with collateral), and that borrowing requires collateral backing.

Two findings here. L-01: the protocol updated health aggregates incrementally using rounded arithmetic and the incremental updates could drift from a full recomputation, enough that a position could pass health checks after a borrow, then fail them on the next refresh. L-02: borrow amounts small enough that their USD value truncated to zero bypassed collateral checks entirely.

Liquidation and Profitability

Most formal verification work on lending protocols proves that liquidation moves the right tokens to the right places, which is necessary but doesn't address the actual risk. A liquidation can transfer funds correctly and still leave the position worse off than before.

We went further and proved that liquidations always improve the position's LTV and are always profitable for the liquidator (even at zero bonus). The profitability property matters because if liquidators can't make money, they stop showing up and bad debt accumulates with nobody to clear it.

M-02 was the most interesting finding. When a position's pre-liquidation LTV exceeded 1/(1+bonus), liquidation actually worsened the LTV. Each step ratcheted it higher. Repeated liquidations could push a position into insolvency. The fix was a dynamic cap on the bonus derived from the current LTV, so the operation can only move the position in the right direction.

The Challenge of Verifying Properties That Matter

None of this is straightforward to prove on production code. You need to understand the protocol well enough to identify which properties actually protect users, and then figure out how to express them in a way that is amenable to formal verification. We're proving "is this protocol solvent?" not "does this function return the right number?" and those are very different levels of difficulty.

Choosing what to prove is most of the work. Solvency, account health, and liquidation correctness require reasoning about relationships between storage fields across the whole system rather than verifying individual functions in isolation. These are also where we found the bugs, which is probably not a coincidence.

Check out the full report for details: https://www.certora.com/reports/suilend