Morpho Midnight Liquidation and Accounting Proofs

Morpho Midnight is an order-driven lending design with richer liquidation accounting than Morpho Blue. A liquidation may inspect several collateral assets, compute a recovery amount, recognize bad debt, slash the market, and update lender credit. The proof work here is about those numbers: when they are computed as in the model, do they restore the borrower and keep lender accounting covered?

This article is pinned to the audited morpho-verity PR #373 commit used by the Morpho Blue article. At that commit, the repo contains a Verity-compiled Midnight artifact that passes the upstream Foundry suite, plus a focused Lean proof layer for the liquidation and accounting properties described here.

Why It Matters

A Midnight borrower can post many collateral assets. During liquidation, the contract walks the active-collateral bitmap, totals the debt supported by those assets, records bad debt when support is insufficient, then runs the repay-and-seize branch. In normal mode, that branch is constrained by the recovery close factor, or RCF.

The first proved property explains what the RCF buys. When the liquidator repays the Solidity maxRepaid amount, the guard accepts the repayment and the projected post-liquidation borrower is healthy within the stated rounding slack. The proof also tracks affordability: the modeled repayment and seizure fit inside the borrower's debt and selected collateral.

The second proved property follows the bad-debt branch. Bad debt reduces the borrower's debt and the market's totalUnits by the same amount. The loss is then reflected in lender credit through the loss factor and update-position path. The checked result is the cover relation needed after the slash: market total units still cover the modeled lenders' updated credit.

How This Was Modeled and Proven

The source-shaped Verity contract is Midnight/Contract.lean, paired with upstream Midnight.sol. It contains the complete Midnight contract for artifact parity and a focused MidnightRCF surface exposing the arithmetic used by the proofs. The proof entrypoint, Proofs.lean, imports the RCF, collateral-loop, bitmap-schedule, market-ledger, units-accounting, refinement, storage, and generated-body shape files.

The RCF proof uses the Solidity normal-mode formula for maxRepaid: the rounded-up shortfall divided by WAD^2 - lif * lltv. The Lean model keeps the Solidity branch condition: when lltv < WAD, it uses that formula; otherwise it returns type(uint256).max. The recovery theorem works in the positive-denominator domain, where lif * lltv < WAD^2.

BitmapSchedule.lean proves the bitmap order used by the active-collateral loop: repeatedly take the most significant active bit, then clear it. CollateralLoop.lean proves the corresponding accumulators for maximum debt, liquidated collateral price, and bad debt. The refinement layer connects those local facts to the selected collateral index, selected price, and repayment branch.

MarketLedger.lean provides the debt-side cover invariant used when bad debt is charged against totalUnits. UnitsAccounting.lean proves that the loss-factor slash, pending-fee slash, accrued-fee subtraction, and update-position returned-credit formula preserve cover for the modeled lenders. Storage.lean carries those equations back to the touched market and borrower storage fields.

There is also empirical artifact evidence. The mapping manifest states that the complete Verity-compiled Midnight replacement passes the upstream Midnight Foundry suite with 373 passing tests, 0 failures, and 0 skipped. That evidence is separate from the Lean claims: the tests check upstream behavior for the compiled artifact, while Lean checks the named liquidation and accounting projections.

The proof rows are Lean theorems over focused projections and named generated-body extraction obligations. The final row is test-parity evidence for the complete compiled Midnight artifact, run through scripts/run_morpho_midnight_parity.sh.

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

git clone https://github.com/Th0rgal/morpho-verity
cd morpho-verity
git checkout 01781488f393835eecf5f8b52dc3b2e49587ac1e
git submodule update --init --recursive
./scripts/prepare_midnight_artifact.sh
MORPHO_MIDNIGHT_PARITY_MODE=verity ./scripts/run_morpho_midnight_parity.sh
python3 scripts/check_morpho_midnight_mapping.py
python3 scripts/report_yul_identity_gap.py --midnight --enforce-configured-gate

Assumptions

The main boundaries are named as proof-domain conditions, extraction obligations, or explicit runtime ECM surfaces.

• RCF coefficient domainlif * lltv is below WAD^2

  morpho-midnight-verity/Midnight/Proofs/RCF.lean

  The recovery theorem uses the positive-denominator domain for the Solidity maxRepaid formula. The model still records the Solidity branch that returns uint256 max when the lltv branch is inactive.

• collateral-loop witnessesselected index, price, lif, bitmap trace, and capacity are extracted

  morpho-midnight-verity/Midnight/Proofs/Refinement.lean

  The RCF result depends on the same collateral loop that computes maxDebt and liquidated collateral price. The remaining generated-body work is to supply those concrete witnesses from the full Solidity-shaped liquidate path.

• market debt coverthe concrete debt list is covered by totalUnits

  morpho-midnight-verity/Midnight/Proofs/MarketLedger.lean

  The bad-debt branch subtracts the same badDebt amount from the borrower debt and market totalUnits. The proof uses a market debt-list cover invariant to justify that subtraction and carry cover to the post-state.

• lender snapshotsstored lender credits are synchronized at the modeled loss factor

  morpho-midnight-verity/Midnight/Proofs/UnitsAccounting.lean

  Lender-credit cover after slashing and updating requires the stored-lender cover and snapshot facts named by the accounting projection. These facts are the bridge from storage to the two-lender modeled cover theorem.

• runtime ECM surface~19 distinct ECM modules for dynamic ABI callbacks, SSTORE2/CREATE2 market storage, transient liquidation locks, tick-to-price math, multicall delegatecall, market-id helpers, Solidity panic payloads, and post-callback health checks remain explicit

  morpho-midnight-verity/Midnight/Proofs/TRUST_BOUNDARIES.md

  The complete artifact keeps a large set of low-level mechanisms as named ECM surfaces (far more than Blue). They cover the exact dynamic layouts, transient-storage lock depth accounting, CREATE2/SSTORE2 market round-trips, tick math, multicall traversal, and several specialized callbacks that the current Verity typed-interface and intrinsic surface do not yet express directly. The two focused arithmetic/accounting claims rely on their stated proof-domain assumptions; full end-to-end paths carry additional extraction obligations for these ECMs. Source faithfulness is also lower than the Blue model (some manual calldata handling and simplified representations are used for proof tractability; immutables are modeled as storage slots).