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

Assumptions

The main boundaries are named as proof-domain conditions, extraction obligations, or explicit low-level assumption 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.

• low-level assumption surface17 distinct named assumption strings for dynamic ABI callbacks, the inner SSTORE2/CREATE2 market-initcode hash, transient liquidation locks, tick-to-price math, multicall delegatecall, Solidity panic payloads, and post-callback health checks remain explicit

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

  The complete artifact keeps a set of low-level mechanisms as named assumption surfaces, a larger set than Blue's. They cover the exact dynamic layouts, transient-storage lock depth accounting, the inner CREATE2/SSTORE2 market-initcode hash (the deployment and preimage paths go through shared Verity modules), tick math, multicall traversal, and 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 arithmetic/accounting claims rely on their stated proof-domain assumptions; full end-to-end paths carry additional extraction obligations for these boundaries. 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).