Formal verification of the Morpho Market core logic, in Lean 4.

We model the core logic of Morpho Market and prove that its safety-critical properties hold across every protocol action. Every theorem is machine-checked by Lean.

What this model is (and isn't)

Our Lean model sits between paper proofs (exact arithmetic, no rounding) and the Solidity implementation (access control, oracle integration, interest rate model, callbacks, and so on). We capture the math with fixed-point arithmetic — accounting for every rounding error — and abstract price changes and interest accruals as environment actions, separated from user operations.

Solidity implementation Our Lean model Paper model core market logic (exact real arithmetic) + fixed-point arithmetic, all rounding errors + price changes & interest accruals (abstracted as environment actions) + concrete price oracle & IRM, access control, callbacks, …

Market operations

The market revolves around three pools — a supply pool that funds borrows, a borrow pool that tracks each borrower's debt, and a collateral pool that backs each position. Seven user operations move assets in and out of these pools — including liquidate, which any external user (the liquidator) can call against an unhealthy borrower. Interest accrual is the one environment action: it inflates the borrow and supply pools by the same amount, with no user trigger.

user op environment supply borrow collateral supply withdraw liquidate accrue interest repay borrow add collateral remove collateral

Note on modeling. In real lending implementations, accrueInterest is not a standalone call — it is folded into every user operation, running at the start before the user's intent is processed. We model it as a distinct environment action so the proofs can talk about user effects and interest effects independently — for example, "this property holds across every user action when no interest accrues in between". The two model views are equivalent: any concrete user op in practice is just an envAccrueInt immediately followed by the corresponding user… action in our model.

How positions move through the market

Every borrower position lives in one of five regions, organized by how a position can leave them. Regions are defined using ltv := debt / (collateral · price) and the two protocol constants lltv (the LLTV threshold) and incentive (the liquidation incentive factor). A Healable position can be fully liquidated back to Healthy. Once a position enters the Bad-debt path, a full liquidation is no longer possible — the liquidation incentive cannot be covered by the remaining collateral. Only repeated partial liquidations work, and they only drain collateral until the position is Insolvent. From there, only writeOff can clear the debt — at which point the loss is realized and socialized among lenders.

user-triggered environment HEALTHY Borrower has the LLTV buffer. ltv ≤ lltv user ops (price-stable, no accrual) envAccrueInt envPriceTick (small) liquidate (full burn) exists_full_liquidation_to_healthy HEALABLE Past the LLTV buffer, but full liquidation is still possible. lltv < ltv ≤ 1 / incentive liquidate (partial) envAccrueInt past budget envPriceTick past 1/incentive BAD DEBT PATH Full liquidation fails — liquidation incentive exceeds collateral value. Partial liquidation can never bring a position back to Healthy. ltv > 1 / incentive liquidate (partial) liquidate_preserves_ bad_debt_path repeated partial liquidations drain collateral INSOLVENT · defaulted All collateral seized; debt remains. collateral = 0, debt > 0 envWriteOff → loss realized, socialized among lenders writeOff_clears_debt CLEARED debt = 0, position removed

Not shown: repay reduces a borrower's debt and supplyCollateral adds collateral, so either can also move a position toward a lower-debt region — including directly to Cleared if the entire debt is repaid. Both are omitted above to keep the focus on the liquidation story.

Headline theorems

Each card states the property in plain English first; toggle to see the Lean statement, and click through to the full proof on GitHub.

No user operation makes a healthy position unhealthy. · step_preserves_allHealthy

After any user operation, every borrower who had the LLTV buffer before still has the LLTV buffer after. Borrows and collateral withdrawals are explicitly gated on the new state being healthy at the observed price.

Show Lean statement 
theorem step_preserves_allHealthy
    {a : Action} {w w' : World}
    (h_pm : NoPriceMove a) (h_acc : NoAccrual a)
    (hbk : Bookkeep w) (hAH : AllHealthy w)
    (hstep : step a w = some w') : AllHealthy w'
View full proof on GitHub →

From a healthy market, every action keeps the protocol solvent — under closed-form budgets. · step_remains_assetCovered_under_allHealthy

Starting from an AllHealthy market, every user operation and every environment action leaves the protocol fully solvent — total debt covered by collateral at the observed price. Environment actions are gated by two closed-form budgets:

  • PriceMoveBudget caps how far the oracle price can drop in a single tick. The new price p' must satisfy lltv · p ≤ p' — a tick can erase at most a factor of 1 − lltv of the price, exactly the room a marginal AllHealthy borrower has before crossing into insolvency.
  • AccrualBudget caps how much interest can accrue at once. The accrued amount Δ must satisfy Δ · lltv ≤ totalBorrowAssets · (1 − lltv) — one accrual cannot consume more than the aggregate LTV headroom across all borrowers.
Show Lean statement 
theorem step_remains_assetCovered_under_allHealthy
    {a : Action} {w w' : World}
    (h_pmb : PriceMoveBudget a (w.oracle.read))
    (hbk : Bookkeep w) (hAH : AllHealthy w)
    (h_acb : AccrualBudget a w)
    (hstep : step a w = some w') : AssetCovered w'
View full proof on GitHub →

Once a position is past the point of no return, partial liquidation cannot rescue it. · liquidate_preserves_bad_debt_path

We partition unhealthy positions into a healable region (liquidation profitable enough to fully cover the debt) and a bad-debt region (debt-times-incentive already exceeds collateral value). The bad-debt region is absorbing: no partial liquidation moves a position out of it.

Show Lean statement 
theorem liquidate_preserves_bad_debt_path
    {w w' : World} {lq b : Addr} {sh seized : ℕ}
    (hp : (0 : OraclePrice) < w.oracle.read)
    (hbk : Bookkeep w)
    (hBDP : BadDebtPath w b)
    (hl : liquidate w lq b sh = some (w', seized)) :
    BadDebtPath w' b
View full proof on GitHub →

If a position is still healable, a single liquidation can heal it. · exists_full_liquidation_to_healthy

If a borrower is still in the Healable region — their bonus-inflated debt is still covered by their collateral at the observed price — then a single full-burn liquidation can return the position to Healthy. This is the constructive partner to the absorbing bad-debt theorem above, completing the dichotomy: every unhealthy position is either healable (one liquidation away from Healthy) or absorbing (no liquidation can rescue it). The existence holds under one closed-form budget:

  • HealableLiquidationBudget requires the borrower's coverage gap — collateral value minus bonus-inflated debt — to be wide enough to absorb two rounding wei. Letting C be the borrower's collateral, D their debt, p the oracle price, and α the liquidation incentive factor, the budget reads α + p ≤ C · p − α · D — the right-hand side is the coverage gap, the left-hand side is one repay-rounding unit plus one collateral-rounding unit valued at the current price.
Show Lean statement 
theorem exists_full_liquidation_to_healthy
    {w : World} {lq b : Addr}
    (hp : (0 : OraclePrice) < w.oracle.read)
    (hUnhealthy : ¬ Healthy w b)
    (hBudget : HealableLiquidationBudget w b)
    (hLiquidatorFunds : LiquidatorHasFullRepayFunds w lq b)
    (hAccounting : MarketAccounting w) :
    ∃ sh w' seized,
      liquidate w lq b sh = some (w', seized) ∧ Healthy w' b
View full proof on GitHub → Morpho wishlist #708

From a solvent market, every user operation keeps it solvent — under closed-form budgets. · step_preserves_assetCovered

Starting from an AssetCovered (solvent) market, every user operation leaves the protocol solvent — total debt still covered by collateral at the observed price. The two share-burn actions — userRepay and userLiquidate — are each gated by a closed-form budget:

  • LiquidateStepBudget fires for userLiquidate: the targeted borrower must satisfy the HealableLiquidationBudget explained in the previous headline (coverage gap wide enough to absorb two rounding wei). Outside this region, partial liquidation mechanically drains collateral instead of restoring solvency.
  • BurnStepBudget fires for both userRepay and userLiquidate: the asset cost of the share burn must stay inside the real borrowed assets, not dip into the virtual borrow-asset reserve. Letting R denote totalBorrowAssets and sh the number of debt shares being burned, the budget reads repayCost(sh) ≤ R — the burn's asset cost stays within the real pool. Crossing this threshold lifts the share-rate for every other borrower, which can knock them into insolvency.
Show Lean statement 
theorem step_preserves_assetCovered
    {a : Action} {w w' : World}
    (hp : 0 < w.oracle.read_q)
    (h_pm : NoPriceMove a) (h_acc : NoAccrual a)
    (hbk : Bookkeep w) (hAC : AssetCovered w)
    (h_liq : LiquidateStepBudget a w)
    (h_burn : BurnStepBudget a w)
    (hstep : step a w = some w') : AssetCovered w'
View full proof on GitHub →

A supplier's position value cannot drop — except when bad debt is realized. · step_preserves_supplySharePriceLE

No user operation and no environment action can reduce a supplier's position value. Suppliers are guaranteed never to lose from protocol behavior — the single exception is envWriteOff, when bad debt is realized and the loss is socialized across all suppliers.

Show Lean statement 
theorem step_preserves_supplySharePriceLE
    {a : Action} {w w' : World}
    (h_nbd : NoBadDebt a) (hbk : Bookkeep w)
    (hstep : step a w = some w') : SupplySharePriceLE w w'
View full proof on GitHub →