[Certora] liquidation liveness by lilCertora · Pull Request #834 · morpho-org/midnight

lilCertora · 2026-05-11T09:29:25Z

No description provided.

Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com> Signed-off-by: lilCertora <lilian@certora.com>

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: cd6315e477

ℹ️ About Codex in GitHub

Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: bc11ba8549

ℹ️ About Codex in GitHub

Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 729f46d510

ℹ️ About Codex in GitHub

Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b926c65cce

ℹ️ About Codex in GitHub

Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

chatgpt-codex-connector · 2026-06-22T12:10:22Z

+    mathint recovery0 = ghostMulDivUp(ghostMulDivUp(collateral(id, borrower, 0), ghostPrice(market.collateralParams[0].oracle), ORACLE_PRICE_SCALE()), WAD(), market.collateralParams[0].maxLif);
+    mathint recovery1 = ghostMulDivUp(ghostMulDivUp(collateral(id, borrower, 1), ghostPrice(market.collateralParams[1].oracle), ORACLE_PRICE_SCALE()), WAD(), market.collateralParams[1].maxLif);
+    mathint recovery2 = ghostMulDivUp(ghostMulDivUp(collateral(id, borrower, 2), ghostPrice(market.collateralParams[2].oracle), ORACLE_PRICE_SCALE()), WAD(), market.collateralParams[2].maxLif);


Tighten recovery mulDivUp before computing debtAfter

When a collateral price is below ORACLE_PRICE_SCALE, the current ghostMulDivUp axioms can model mulDivUp(collateral, price, ORACLE_PRICE_SCALE) as any value up to the full collateral amount, far above the real ceil result. Separate from the earlier RCF over-approximation thread, this value feeds the bad-debt recovery here, so debtAfterBadDebt can equal _debt even when the real liquidate would realize bad debt; then the badDebtCanBeLiquidated implication is skipped instead of checking the promised debt drop. Add the mulDivUpTightBound/upper-bound axiom before using this recovery reconstruction.

Useful? React with 👍 / 👎.

jhoenicke · 2026-06-23T17:00:25Z

I replace some require by assert here: #1017. There are still two requires left, which should in principle also be provable.

Otherwise, that looks good. I think all cases are covered except one minor special case: You can liquidate more than maxRepaid if only dust ist left. I don't think that is important enough.

…veness

QGarchery · 2026-07-16T11:48:10Z

+}
+
+function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
+    if (d == 0) {


An assumption we are making here is that there is no overflow, I think it's worth mentioning

QGarchery · 2026-07-16T11:53:03Z

+    uint256 lltv = market.collateralParams[i].lltv;
+    uint256 maxLif = market.collateralParams[i].maxLif;
+
+    require lltv > 0 && lltv <= WAD(), "lltv in (0, WAD] for a created market (in CreatedMarkets.spec)";


it does not prove that lltv > 0 right ?
What breaks if we don't have this assumption ?

QGarchery · 2026-07-16T14:29:31Z

+
+    require lltv > 0 && lltv <= WAD(), "lltv in (0, WAD] for a created market (in CreatedMarkets.spec)";
+    require maxLif >= WAD(), "maxLif >= WAD (maxLifIsAtLeastWad)";
+    require lltv < WAD() => lltv * maxLif <= WAD() * (WAD() - 1), "lltv < WAD => lltv*maxLif <= WAD*(WAD-1) (lifTimesLltvStrictBound)";


we don't have the lifTimesLltvStrictBound rule in main anymore, we should add it back (feasible because we kept the invariant liquidationCursor < WAD)

QGarchery · 2026-07-16T14:32:54Z

+    threeCollatSetup(e, market, id, borrower);
+    require collateralIndex == 0 || collateralIndex == 1 || collateralIndex == 2, "seized index in {0,1,2} (<= loop_iter)";
+    require summaryGetBit(collateralBitmap(id, borrower), collateralIndex), "the seized collateral is active";
+    require getPrice(collateralIndex, market.collateralParams) > 0, "the seized collateral is priced (LIVENESS)";


this should be added to the list of assumptions at the top

QGarchery · 2026-07-16T14:40:11Z

+    uint256 maxLifJ = getMaxLif(collateralIndex, market.collateralParams);
+    uint256 priceJ = getPrice(collateralIndex, market.collateralParams);
+    uint128 collatJ = collateral(id, borrower, collateralIndex);
+    assert maxLifJ * lltvJ <= WAD() * (WAD() - 1), "maxLif*lltv <= WAD*(WAD-1) (lifTimesLltvStrictBound) => WAD*WAD - maxLif*lltv >= WAD >= 1";


same, lifTimesLltvStrictBound doesn't exist anymore, although here it's an assert. This is a bit suspicious because you need to know that the liquidation cursor is < WAD

…veness

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 8215ae631e

ℹ️ About Codex in GitHub

Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

chatgpt-codex-connector · 2026-08-18T13:12:15Z

+    uint256 lltv = market.collateralParams[i].lltv;
+    uint256 maxLif = Utils.maxLif(lltv, market.collateralParams[i].liquidationCursor);
+
+    require lltv > 0 && lltv <= WAD(), "lltv in (0, WAD] for a created market (in CreatedMarkets.spec)";


Include zero-LLTV markets in the proof

Remove the lltv > 0 assumption: enableLltv accepts zero and touchMarket permits an enabled zero-LLTV tier, so this require silently excludes valid created markets from every liveness rule despite the message claiming the bound comes from CreatedMarkets.spec. This leaves liquidation liveness unverified for zero-LLTV collateral.

AGENTS.md reference: AGENTS.md:L10-L11

Useful? React with 👍 / 👎.

chatgpt-codex-connector · 2026-08-18T13:12:15Z

+/// Deterministic ghost for UtilsLib.mulDivDown. Each axiom is proven in MulDiv.spec (rule named per axiom).
+persistent ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256 {
+    // Proved in Muldiv.spec : mulDivDownRoundsDown
+    axiom forall uint256 a. forall uint256 b. forall uint256 d. d > 0 => ghostMulDivDown(a, b, d) * d <= a * b;


Guard the mulDiv axioms against overflowing inputs

Add the real non-overflow precondition to these rounding axioms. For example, with a = b = max_uint256 and d = 1, this axiom requires a uint256 ghost result multiplied by one to be at least max_uint256², which is impossible because CVL evaluates the arithmetic as unbounded integers; the analogous mulDivUp axiom has the same problem. Since these are global axioms, the contradiction makes every rule vacuously pass rather than proving liquidation liveness.

AGENTS.md reference: AGENTS.md:L40-L40

Useful? React with 👍 / 👎.

chatgpt-codex-connector · 2026-08-18T13:12:16Z

+    bytes data;
+    liquidate@withrevert(e, market, 0, 0, 0, borrower, postMaturityMode, receiver, 0, data);
+    assert !lastReverted;
+    assert debtAfter < _debt => debt(id, borrower) < _debt;


Prove that one liquidation path exists for each borrower

Add a coverage rule linking the branches promised in the header. When debtAfter == _debt, this implication checks no debt progress, while every positive-input rule independently assumes seizablePreamble and a nonempty safe amount through its requires; nothing proves that the same no-bad-debt borrower admits any positive repayment or seizure. Consequently all current rules can pass without establishing the stated claim that together they cover every liquidatable borrower.

AGENTS.md reference: AGENTS.md:L10-L12

Useful? React with 👍 / 👎.

QGarchery · 2026-08-26T17:19:05Z

see https://morpholabs.slack.com/archives/C0ACSA8TNMA/p1784213415700999?thread_ts=1784122134.033749&cid=C0ACSA8TNMA

lilCertora and others added 28 commits May 5, 2026 15:16

modifs to prove countBits <= 10

da4ce07

linter

33e2dd7

Merge branch 'main' into certora/improveCollateralBitmap

f8a2851

Merge branch 'main' into certora/improveCollateralBitmap

e7f9f0f

Merge branch 'main' into certora/improveCollateralBitmap

d603ce5

update

de7d87f

Merge branch 'main' into certora/improveCollateralBitmap

bd46e1d

addition

9e68d3a

Update certora/specs/BitmapSummaries.spec

551fee7

Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com> Signed-off-by: lilCertora <lilian@certora.com>

Merge branch 'main' into certora/improveCollateralBitmap

47f8898

rule addition in bitmap.spec

c7ed9d2

Merge branch 'main' into certora/improveCollateralBitmap

cbba45a

Merge branch 'main' into certora/improveCollateralBitmap

3413e6c

review modifs

0adfc02

Merge branch 'main' into certora/improveCollateralBitmap

0b5691a

add spec and conf

879852e

Revert unrelated files to main

6e1763a

Merge branch 'main' into certora/liquidationLiveness

e320601

Merge branch 'main' into certora/liquidationLiveness

407d9ae

Merge branch 'main' into certora/liquidationLiveness

9584c45

update

d952ce4

delete old

f3f7de4

delete old conf

26bcbdd

linter + modifs

315c3a2

linter spec

1abd971

simplification

7f68b3a

split confs

ebc1bd7

split confs

8d36ffb

lilCertora self-assigned this May 17, 2026

modif conf

231771b

lilCertora added 5 commits June 5, 2026 16:38

linter

6175f9d

Merge branch 'main' into certora/liquidationLiveness

531d05f

Merge branch 'main' into certora/liquidationLiveness

df2f5c5

cleaning, remove axioms and formatting

f7562b5

cleaning

cd6315e

lilCertora marked this pull request as ready for review June 7, 2026 17:52

chatgpt-codex-connector Bot reviewed Jun 7, 2026

View reviewed changes

Comment thread certora/specs/LiquidateLiveness.spec Outdated

Comment thread certora/confs/LiquidateLiveness.conf

lilCertora added 3 commits June 7, 2026 20:21

codex suggestion

d691711

review

3303269

Merge branch 'main' into certora/liquidationLiveness

bc11ba8

chatgpt-codex-connector Bot reviewed Jun 9, 2026

View reviewed changes

Comment thread certora/specs/LiquidateLiveness.spec

lilCertora requested a review from jhoenicke June 9, 2026 11:40

Merge branch 'main' into certora/liquidationLiveness

729f46d

chatgpt-codex-connector Bot reviewed Jun 15, 2026

View reviewed changes

Comment thread certora/specs/LiquidateLiveness.spec

lilCertora requested review from QGarchery and bhargavbh June 15, 2026 16:51

Merge branch 'main' into certora/liquidationLiveness

b926c65

chatgpt-codex-connector Bot reviewed Jun 22, 2026

View reviewed changes

jhoenicke and others added 4 commits July 15, 2026 17:34

[Certora] liquidation liveness refactor (#1017)

374fa65

Merge remote-tracking branch 'origin/main' into certora/liquidationLi…

e452351

…veness

Updated spec to current main

0bbe529

Use Utils.maxLif()

ccbc262

QGarchery reviewed Jul 16, 2026

View reviewed changes

MathisGD assigned jhoenicke and unassigned lilCertora Aug 3, 2026

Merge remote-tracking branch 'origin/main' into certora/liquidationLi…

8215ae6

…veness

chatgpt-codex-connector Bot reviewed Aug 18, 2026

View reviewed changes

QGarchery closed this Aug 26, 2026

Uh oh!

Conversation

lilCertora commented May 11, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Jun 22, 2026

Choose a reason for hiding this comment

Uh oh!

jhoenicke commented Jun 23, 2026

Uh oh!

QGarchery Jul 16, 2026

Choose a reason for hiding this comment

Uh oh!

QGarchery Jul 16, 2026

Choose a reason for hiding this comment

Uh oh!

QGarchery Jul 16, 2026

Choose a reason for hiding this comment

Uh oh!

QGarchery Jul 16, 2026

Choose a reason for hiding this comment

Uh oh!

QGarchery Jul 16, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Aug 18, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Aug 18, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Aug 18, 2026

Choose a reason for hiding this comment

Uh oh!

QGarchery commented Aug 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants