Morpho Blue Health and Liquidation Invariants

Morpho Blue is a minimal, immutable lending primitive. Each position is healthy when its collateral, priced by the oracle and scaled by the market loan-to-value, covers its outstanding debt. This case proves two statements about that health predicate: one the Morpho team raised in morpho-blue #684, and one they flagged as hard to state precisely.

Why It Matters

Health is the safety boundary of a lending market. If an account that was healthy can be made unhealthy by an unrelated action, it becomes liquidatable through no fault of its owner, and the market loses the monotonicity that liquidations rely on. The first property rules this out: at a constant price and without interest accrual, no operation can turn a healthy account unhealthy. Read the other way, at a constant price the only thing that can move a position from healthy to unhealthy on its own is interest accrual, the slow growth of the debt that the first property sets aside.

The second property is the mirror image, on the liquidation side. When a borrower is undercollateralized but not by too much, a liquidator should be able to repay the debt, collect the seizure incentive, and leave the position solvent again, without the market absorbing bad debt. The threshold for this is a loan-to-value below 1/LIF, the reciprocal of the liquidation incentive factor. The Morpho team noted that pinning down the rounding on that threshold is delicate, so the property was left unproven.

The proved theorem uses full liquidation: the liquidator repays all remaining borrow shares. A strictly partial version would ask for a smaller repayment that still restores health, but borrow shares are indivisible. If a position owes one share, the only repayments are zero or one share; zero changes nothing, and one share is already the full liquidation.

How This Was Modeled and Proven

The source of truth is a Verity contract, Morpho/Contract.lean, a transcription of Morpho.sol that compiles, through Yul, to EVM bytecode. Several operations (exact Morpho SafeTransferLib with its specific revert strings and code-length guard, length-gated callbacks, market-params keccak, EIP-712 digest, and one IRM read in accrual) are expressed as External Call Modules (ECMs). These are hand-written Yul emitters that the Lean proofs treat as opaque: the model only assumes their declared interface and effects. The produced Yul for the modeled paths is compared to the Solidity IR via an automated identity-gap report and a controlled drift manifest; behavioral parity (145 passing Foundry tests) provides the main cross-check that the compiled artifact behaves like upstream on the tested surface. The same Verity/Lean methodology is used as in the verity-benchmark cases.

The proofs read only the storage the health predicate touches. We isolate that storage in a small projection, HealthModel.lean, holding the position fields borrowShares and collateral, the shared market totals, the loan-to-value, and the oracle price. The health predicate is transcribed verbatim from _isHealthyWithPrice: a position is healthy when it has no debt, or when its rounded-down maximum borrow is at least its rounded-up borrowed amount. The projection is a named, enumerated slice of storage. The correspondence between generated contract bodies and projected shapes is tracked explicitly in Refinement.lean; all generated entrypoint bodies used by the health theorem are proved to refine those projected shapes, including the healthy guards for borrow and withdraw-collateral and the unhealthy guard on liquidation. The liquidation guard is proved at the point where Solidity checks it, after _accrueInterest. The generated extraction now exposes that post-accrual state, and the no-accrual discipline carries the model-level unhealthy classifier back to the original pre-state.

Property one factors every entrypoint, restricted to one watched account, into two shapes. Supply, withdraw, supply-collateral, repay, and every action by another account are monotone for the watched account: collateral does not fall, borrow shares do not rise, and without accrual the shared borrow index does not grow. The arithmetic core, in Arith.lean, shows the rounded maximum borrow cannot fall and the rounded borrowed amount cannot rise, so health survives. Borrow and withdraw-collateral are the other shape: they can lower the account's own health but end in a require(_isHealthy), so a successful call lands healthy by construction.

Property two makes the threshold division-free. We carry the incentive factor as the contract computes it, prove it always lies between one and 1.15, and prove the liquidatable-yet-restorable band is non-empty. The affordability result then chains three flooring steps from the seized collateral back to the quoted collateral; because every rounding falls the favorable way, the seizure never exceeds the posted collateral, so the position keeps a positive collateral balance and the full liquidation triggers no bad-debt socialization. Morpho's liquidate lets the caller specify either the collateral to seize or the debt shares to repay; we model both modes. The two share the same post-state writes, so one transition captures them, and the seized-assets mode adds only the derivation of repaid shares from the named seizure. The post-liquidation state, written liquidate s in the proofs, is s with the repaid shares and the seized collateral subtracted. Driving those shares to zero clears the debt, which is what the health predicate certifies. The companion counterexample exhibits a concrete single-share position where the strictly partial phrasing fails, which is why the sharp statement targets the full liquidation.

The top-level health-preservation theorem names its environmental inputs, constant price and no accrual, as first-class assumptions in Env.lean. The executable refinement layer names the contract-facing inputs it still receives from the environment: ECM market-id and oracle-price alignment, the local oracle-price/collateral-fit arithmetic condition, and the no-accrual discipline for the liquidation path. The liquidate pre-state bridge is now proved from the generated post-accrual guard. The remaining Morpho-side axiom is storage slot injectivity for the keccak-derived layout.

Status reflects the Lean proof of each theorem as stated over the storage projection. The generated Verity bodies for the health theorem are tied to those projected shapes in Refinement.lean.

The property theorems above depend only on the standard logical axioms propext, Quot.sound, and Classical.choice. The generated refinement layer additionally contains the named Morpho storage-layout assumption listed below plus the ECM-interface assumptions for the transfer, callback, market-id, and oracle operations. These ECM assumptions are not Lean axioms in the proof kernel; they are explicit trust boundaries whose Yul implementations are reviewed via the identity report and exercised by the parity suite. None of the files uses a sorry placeholder.

git clone https://github.com/Th0rgal/morpho-verity
cd morpho-verity
git checkout 01781488f393835eecf5f8b52dc3b2e49587ac1e
lake build Morpho.Proofs

Assumptions

The remaining scope conditions and model choices are listed below, with their Lean location and the contract fact they capture.

• ConstPricethe oracle reading is unchanged across the step

  morpho-blue-verity/Morpho/Proofs/Env.lean

  Both properties are stated at a constant price. The price field of the post-state equals that of the pre-state, matching the phrase at constant prices in the original statement.

• NoAccrualthe market borrow index does not grow

  morpho-blue-verity/Morpho/Proofs/Env.lean

  The market borrow index rises only through _accrueInterest. A position's debt is its borrow shares valued at that index, so when the index grows the debt rises while the collateral, price, and loan-to-value stay put, which is the one way a passive position drifts into unhealthy. Excluding accrual is exactly the condition that the index does not grow from pre-state to post-state, which is the crux of the health-preservation proof.

• nat_modelhealth arithmetic modeled over the naturals

  morpho-blue-verity/Morpho/Proofs/HealthFaithful.lean

  The model computes health over the natural numbers. The borrow-side share and asset bounds are proved from packed uint128 reads and the full-precision health conversion. The remaining arithmetic condition says that the oracle price read by the contract keeps the collateral-price product, and then the LLTV product, within uint256. Under that local bound, the contract word arithmetic agrees with the natural-number arithmetic.

• ECM alignmentsymbolic market-id, oracle-price, and transfer/callback outcomes match the projected state

  morpho-blue-verity/Morpho/Proofs/Disciplines.lean

  The generated Verity bodies read market ids and oracle prices through ECM hooks and perform token transfers and optional callbacks through ECMs. Refinement for the guarded entrypoints assumes those symbolic reads and the success/failure of the transfer and callback ECMs are aligned with the market id, price, and state updates used by the storage projection. The custom safeTransfer and safeTransferFrom ECMs exist precisely because Morpho's SafeTransferLib uses specific string reverts and an explicit code-length guard; Verity's built-in helpers use different revert conventions, so the Morpho-specific modules are retained for Yul and parity fidelity.

• slot injectivitydistinct valid storage locations have distinct storage keys

  morpho-blue-verity/Morpho/Proofs/StorageFrame.lean

  The generated-body framing lemmas reason about packed Morpho storage slots through symbolic locations. Their one storage-layout axiom is slot injectivity: two valid projected locations collide only when they are the same location.