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 morpho-verity PR #379 commit (merged July 2, 2026), the same 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. Token transfers in the full artifact use Verity's standard legacyStringSafeTransfer / legacyStringSafeTransferFrom modules through a typed IERC20 interface.

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 7ccc1dbeec0e9bba02da506ba4ffcca316422f04
lake build Midnight.Proofs

git clone https://github.com/Th0rgal/morpho-verity
cd morpho-verity
git checkout 7ccc1dbeec0e9bba02da506ba4ffcca316422f04
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

Hypotheses

The main boundaries are named as proof-domain conditions, extraction obligations, or explicit low-level assumption surfaces.

• recovery formula denominator is positive

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

  The recovery theorem assumes lif * lltv < WAD^2, so the denominator WAD^2 - lif * lltv of the Solidity maxRepaid formula is positive. The model still records the Solidity branch that returns uint256 max when the lltv branch is inactive.

• collateral loop values come from the liquidate path

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

  The proof takes the selected collateral index, price, lif, bitmap trace, and capacity as extracted witnesses. The RCF result depends on the same collateral loop that computes maxDebt and the liquidated collateral price. Supplying these concrete witnesses from the full Solidity-shaped liquidate path is remaining generated-body work.

• market total units cover the debt list

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

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

• lender credits are synced to the loss factor

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

  Stored lender credits are synchronized at the modeled loss factor. Lender-credit cover after slashing and updating requires these stored-lender cover and snapshot facts from the accounting projection. They bridge storage to the two-lender modeled cover theorem.

• low-level mechanisms stay named assumptions

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

  The complete artifact keeps 17 distinct named assumption strings explicit, a larger set than Blue's. They cover dynamic ABI callbacks, the inner SSTORE2/CREATE2 market-initcode hash (the deployment and preimage paths go through shared Verity modules), transient liquidation locks, tick-to-price math, multicall delegatecall, Solidity panic payloads, and post-callback health checks, plus several specialized callbacks that the pinned Verity typed-interface and intrinsic surface does not yet express directly. Token transfers use Verity's standard legacyStringSafeTransfer modules through typed IERC20 parameters. The two focused claims rely on their stated proof-domain assumptions; full end-to-end paths carry additional extraction obligations. Source faithfulness is also lower than the Blue model: some calldata is handled manually, some representations are simplified for proof tractability, and immutables are modeled as storage slots.