From d595508e56a8ba0fc9a4be99504bf0c7f31f90c1 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Thu, 2 Apr 2026 15:35:51 +0200
Subject: [PATCH 01/27] added moer rules for offer.buy=false and
 takeDoesNotAffectThirdParties

---
 certora/confs/ContinuousFeeProtection.conf |  24 +++
 certora/specs/ContinuousFeeProtection.spec | 165 +++++++++++++++++++++
 2 files changed, 189 insertions(+)
 create mode 100644 certora/confs/ContinuousFeeProtection.conf
 create mode 100644 certora/specs/ContinuousFeeProtection.spec

diff --git a/certora/confs/ContinuousFeeProtection.conf b/certora/confs/ContinuousFeeProtection.conf
new file mode 100644
index 000000000..ffbf922d1
--- /dev/null
+++ b/certora/confs/ContinuousFeeProtection.conf
@@ -0,0 +1,24 @@
+{
+  "files": [
+    "src/Midnight.sol"
+  ],
+  "verify": "Midnight:certora/specs/ContinuousFeeProtection.spec",
+  "solc": "solc-0.8.31",
+  "solc_evm_version": "osaka",
+  "optimistic_hashing": true,
+  "hashing_length_bound": 2048,
+  "solc_via_ir": true,
+  "optimistic_loop": true,
+  "loop_iter": 2,
+  "rule_sanity": "basic",
+  "smt_timeout": 7200,
+  "prover_args": [
+    "-depth 5",
+    "-timeout 3600",
+    "-splitParallel",
+    "true",
+    "-dontStopAtFirstSplitTimeout",
+    "true"
+  ],
+  "msg": "Midnight Continuous Fee Protection"
+}
diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
new file mode 100644
index 000000000..67cc0dd1e
--- /dev/null
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -0,0 +1,165 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function multicall(bytes[]) external => HAVOC_ALL DELETE;
+
+    function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation, chainId, midnight);
+    function UtilsLib.mulDivDown(uint256 a, uint256 b, uint256 denominator) internal returns (uint256) => CVL_mulDivDown(a, b, denominator);
+    function UtilsLib.mulDivUp(uint256 a, uint256 b, uint256 denominator) internal returns (uint256) => CVL_mulDivUp(a, b, denominator);
+    function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
+    function TickLib.wExp(int256) internal returns (uint256) => NONDET;
+    function UtilsLib.msb(uint128) internal returns (uint256) => NONDET;
+    function tradingFee(bytes32 id, uint256 timeToMaturity) internal returns (uint256) => NONDET;
+
+    function creditOf(bytes32 id, address user) external returns (uint256) envfree;
+    function pendingFee(bytes32 id, address user) external returns (uint128) envfree;
+    function continuousFee(bytes32 id) external returns (uint32) envfree;
+    function userLossIndex(bytes32 id, address user) external returns (uint128) envfree;
+    function lossIndex(bytes32 id) external returns (uint128) envfree;
+    function lastAccrual(bytes32 id, address user) external returns (uint128) envfree;
+    function updatePositionView(Midnight.Obligation memory obligation, bytes32 id, address user) external returns (uint128, uint128, uint128);
+
+    function _.price() external => NONDET;
+    function signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET;
+    function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET;
+    function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET;
+    function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
+    function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, uint256, bytes) external => NONDET;
+    function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, uint256, bytes) external => NONDET;
+    function isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET;
+    function _.canIncreaseCredit(address) external => NONDET;
+    function _.canIncreaseDebt(address) external => NONDET;
+}
+
+// IdLib summary: remember the last id returned by toId.
+persistent ghost bytes32 lastId;
+
+function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midnight) returns bytes32 {
+    bytes32 id;
+    lastId = id;
+    return id;
+}
+
+// Exact mulDivDown: floor(a * b / d)
+function CVL_mulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 {
+    require d > 0, "see NoDivisionByZero.spec";
+    return require_uint256((to_mathint(a) * to_mathint(b)) / to_mathint(d));
+}
+
+// Exact mulDivUp: ceil(a * b / d)
+function CVL_mulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 {
+    require d > 0, "see NoDivisionByZero.spec";
+    return require_uint256((to_mathint(a) * to_mathint(b) + to_mathint(d) - 1) / to_mathint(d));
+}
+
+function passiveFeeRecipient() returns address {
+    return 0x7e3dce7c19791d65d67ef7ce3c42d2b7fe6fecb1;
+}
+
+definition WAD() returns uint256 = 10 ^ 18;
+
+// The continuous fee is never overcharged: when a lender's credit increases via a buy-offer
+// take, their pendingFee increases by at most floor(creditIncrease * continuousFee * timeToMaturity / WAD).
+// This is a rounding-favors-maker guarantee: mulDivDown means the lender pays the floor, never the ceiling.
+// Pending accrual is not required: time-based fee drainage inside _updatePosition only
+// reduces pendingFeeDelta, never raises it. Pending slash and lossIndex saturation must still
+// be excluded because they wipe credit without proportionally reducing pendingFee, breaking the inequality.
+rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address takerCallback,
+        bytes takerCallbackData, address receiver, Midnight.Offer offer,
+        Midnight.Signature signature, bytes32 root, bytes32[] proof, address lender) {
+    require offer.buy;
+    // PASSIVE_FEE_RECIPIENT receives extra credit from every _updatePosition call on other
+    // positions (line 682 of Midnight.sol), so their credit change is not governed solely
+    // by the continuousFee formula.
+    require lender != passiveFeeRecipient();
+
+    bytes32 id;
+    uint256 creditBefore = creditOf(id, lender);
+    uint256 pendingFeeBefore = pendingFee(id, lender);
+    require pendingFeeBefore <= creditBefore;
+    require userLossIndex(id, lender) == lossIndex(id); // no pending slash: slashing reduces creditDelta without proportionally reducing pendingFeeDelta, which can push pendingFeeDelta above the formula
+    require lossIndex(id) < max_uint128; // excludes lossIndex saturation: same risk as pending slash — credit is wiped unconditionally, shrinking creditDelta without a matching reduction in pendingFeeDelta
+
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
+
+    require id == lastId;
+
+    // Read contFee AFTER take so it matches the value actually used by take: touchObligation
+    // initializes continuousFee = defaultContinuousFee[loanToken] on the first touch, so a
+    // pre-take read would see stale storage if the obligation was just created during this call.
+    uint256 contFee = continuousFee(id);
+    uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity
+        ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
+    // Economic viability constraint: the total continuous fee cannot exceed 100% of credit
+    // (contFee * timeToMaturity / WAD <= 1). Without this, accrual inside _updatePosition
+    // inflates buyerCreditIncrease above creditDelta, pushing pendingFeeDelta above the formula.
+    // In practice MAX_CONTINUOUS_FEE = 317097919 (~1% APR) with realistic maturities keeps r << 1.
+    require to_mathint(contFee) * to_mathint(timeToMaturity) <= WAD();
+
+    uint256 creditAfter     = creditOf(id, lender);
+    uint256 pendingFeeAfter = pendingFee(id, lender);
+
+    mathint creditDelta     = to_mathint(creditAfter)     - to_mathint(creditBefore);
+    mathint pendingFeeDelta = to_mathint(pendingFeeAfter) - to_mathint(pendingFeeBefore);
+
+    require creditDelta >= 0; // scope to buyers gaining credit
+    assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+}
+
+// When a seller's credit decreases via a take, their pendingFee decreases by
+// exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
+// updatePositionView accounts for slash and accrual before the proportional formula runs.
+rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker, address takerCallback,
+        bytes takerCallbackData, address receiver, Midnight.Offer offer,
+        Midnight.Signature signature, bytes32 root, bytes32[] proof, address seller) {
+    require !offer.buy;
+    require seller != passiveFeeRecipient();
+
+    bytes32 id;
+    uint128 postUpdateCredit;
+    uint128 postUpdatePendingFee;
+    uint128 accruedFee;
+    postUpdateCredit, postUpdatePendingFee, accruedFee = updatePositionView(e, offer.obligation, id, seller);
+    // The Solidity mulDivUp is skipped when sellerPos.credit == 0 after _updatePosition,
+    // leaving pendingFee unchanged. Require credit > 0 to stay in the proportional branch.
+    require postUpdateCredit > 0;
+
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
+
+    require id == lastId;
+
+    uint256 creditAfter     = creditOf(id, seller);
+    uint256 pendingFeeAfter = pendingFee(id, seller);
+
+    mathint creditDelta     = to_mathint(creditAfter)     - to_mathint(postUpdateCredit);
+    mathint pendingFeeDelta = to_mathint(pendingFeeAfter) - to_mathint(postUpdatePendingFee);
+
+    require creditDelta <= 0; // scope to sellers losing credit
+    mathint creditDecrease = -creditDelta;
+    assert pendingFeeDelta == -((to_mathint(postUpdatePendingFee) * creditDecrease + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit));
+}
+
+// take() must not modify credit or pendingFee of any address other than the buyer, seller,
+// and PASSIVE_FEE_RECIPIENT. This catches accidental writes to wrong positions (e.g. wrong id,
+// wrong user) and callback side-effects.
+rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback,
+        bytes takerCallbackData, address receiver, Midnight.Offer offer,
+        Midnight.Signature signature, bytes32 root, bytes32[] proof, address user) {
+    address buyer  = offer.buy ? offer.maker : taker;
+    address seller = offer.buy ? taker       : offer.maker;
+
+    require user != buyer;
+    require user != seller;
+    require user != passiveFeeRecipient();
+
+    bytes32 id;
+    uint256 creditBefore     = creditOf(id, user);
+    uint256 pendingFeeBefore = pendingFee(id, user);
+
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
+
+    require id == lastId;
+
+    assert creditOf(id, user)     == creditBefore;
+    assert pendingFee(id, user)   == pendingFeeBefore;
+}

From 584606ecdba826ff6caad6373b2cb14fda54b26d Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Thu, 2 Apr 2026 15:40:04 +0200
Subject: [PATCH 02/27] fmt

---
 certora/specs/ContinuousFeeProtection.spec | 36 ++++++++++------------
 1 file changed, 16 insertions(+), 20 deletions(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index 67cc0dd1e..731d0f82c 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -64,10 +64,9 @@ definition WAD() returns uint256 = 10 ^ 18;
 // Pending accrual is not required: time-based fee drainage inside _updatePosition only
 // reduces pendingFeeDelta, never raises it. Pending slash and lossIndex saturation must still
 // be excluded because they wipe credit without proportionally reducing pendingFee, breaking the inequality.
-rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address takerCallback,
-        bytes takerCallbackData, address receiver, Midnight.Offer offer,
-        Midnight.Signature signature, bytes32 root, bytes32[] proof, address lender) {
+rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address lender) {
     require offer.buy;
+
     // PASSIVE_FEE_RECIPIENT receives extra credit from every _updatePosition call on other
     // positions (line 682 of Midnight.sol), so their credit change is not governed solely
     // by the continuousFee formula.
@@ -88,18 +87,18 @@ rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address ta
     // initializes continuousFee = defaultContinuousFee[loanToken] on the first touch, so a
     // pre-take read would see stale storage if the obligation was just created during this call.
     uint256 contFee = continuousFee(id);
-    uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity
-        ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
+    uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
+
     // Economic viability constraint: the total continuous fee cannot exceed 100% of credit
     // (contFee * timeToMaturity / WAD <= 1). Without this, accrual inside _updatePosition
     // inflates buyerCreditIncrease above creditDelta, pushing pendingFeeDelta above the formula.
     // In practice MAX_CONTINUOUS_FEE = 317097919 (~1% APR) with realistic maturities keeps r << 1.
     require to_mathint(contFee) * to_mathint(timeToMaturity) <= WAD();
 
-    uint256 creditAfter     = creditOf(id, lender);
+    uint256 creditAfter = creditOf(id, lender);
     uint256 pendingFeeAfter = pendingFee(id, lender);
 
-    mathint creditDelta     = to_mathint(creditAfter)     - to_mathint(creditBefore);
+    mathint creditDelta = to_mathint(creditAfter) - to_mathint(creditBefore);
     mathint pendingFeeDelta = to_mathint(pendingFeeAfter) - to_mathint(pendingFeeBefore);
 
     require creditDelta >= 0; // scope to buyers gaining credit
@@ -109,9 +108,7 @@ rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address ta
 // When a seller's credit decreases via a take, their pendingFee decreases by
 // exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
 // updatePositionView accounts for slash and accrual before the proportional formula runs.
-rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker, address takerCallback,
-        bytes takerCallbackData, address receiver, Midnight.Offer offer,
-        Midnight.Signature signature, bytes32 root, bytes32[] proof, address seller) {
+rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address seller) {
     require !offer.buy;
     require seller != passiveFeeRecipient();
 
@@ -120,6 +117,7 @@ rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker
     uint128 postUpdatePendingFee;
     uint128 accruedFee;
     postUpdateCredit, postUpdatePendingFee, accruedFee = updatePositionView(e, offer.obligation, id, seller);
+
     // The Solidity mulDivUp is skipped when sellerPos.credit == 0 after _updatePosition,
     // leaving pendingFee unchanged. Require credit > 0 to stay in the proportional branch.
     require postUpdateCredit > 0;
@@ -128,10 +126,10 @@ rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker
 
     require id == lastId;
 
-    uint256 creditAfter     = creditOf(id, seller);
+    uint256 creditAfter = creditOf(id, seller);
     uint256 pendingFeeAfter = pendingFee(id, seller);
 
-    mathint creditDelta     = to_mathint(creditAfter)     - to_mathint(postUpdateCredit);
+    mathint creditDelta = to_mathint(creditAfter) - to_mathint(postUpdateCredit);
     mathint pendingFeeDelta = to_mathint(pendingFeeAfter) - to_mathint(postUpdatePendingFee);
 
     require creditDelta <= 0; // scope to sellers losing credit
@@ -142,24 +140,22 @@ rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker
 // take() must not modify credit or pendingFee of any address other than the buyer, seller,
 // and PASSIVE_FEE_RECIPIENT. This catches accidental writes to wrong positions (e.g. wrong id,
 // wrong user) and callback side-effects.
-rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback,
-        bytes takerCallbackData, address receiver, Midnight.Offer offer,
-        Midnight.Signature signature, bytes32 root, bytes32[] proof, address user) {
-    address buyer  = offer.buy ? offer.maker : taker;
-    address seller = offer.buy ? taker       : offer.maker;
+rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address user) {
+    address buyer = offer.buy ? offer.maker : taker;
+    address seller = offer.buy ? taker : offer.maker;
 
     require user != buyer;
     require user != seller;
     require user != passiveFeeRecipient();
 
     bytes32 id;
-    uint256 creditBefore     = creditOf(id, user);
+    uint256 creditBefore = creditOf(id, user);
     uint256 pendingFeeBefore = pendingFee(id, user);
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 
     require id == lastId;
 
-    assert creditOf(id, user)     == creditBefore;
-    assert pendingFee(id, user)   == pendingFeeBefore;
+    assert creditOf(id, user) == creditBefore;
+    assert pendingFee(id, user) == pendingFeeBefore;
 }

From 018dfe5c9693246cfd0436eb8708439bb227a113 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Thu, 2 Apr 2026 15:45:18 +0200
Subject: [PATCH 03/27] fmt

---
 certora/specs/ContinuousFeeProtection.spec | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index 731d0f82c..49e960916 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -79,22 +79,27 @@ rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address ta
     require userLossIndex(id, lender) == lossIndex(id); // no pending slash: slashing reduces creditDelta without proportionally reducing pendingFeeDelta, which can push pendingFeeDelta above the formula
     require lossIndex(id) < max_uint128; // excludes lossIndex saturation: same risk as pending slash — credit is wiped unconditionally, shrinking creditDelta without a matching reduction in pendingFeeDelta
 
-    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
-
-    require id == lastId;
-
-    // Read contFee AFTER take so it matches the value actually used by take: touchObligation
-    // initializes continuousFee = defaultContinuousFee[loanToken] on the first touch, so a
-    // pre-take read would see stale storage if the obligation was just created during this call.
+    // Read contFee and timeToMaturity before take so the prover can use these constraints to
+    // prune execution paths inside take(). timeToMaturity is a pure function of the offer fields
+    // (which don't change), so it's consistent before and after. contFee requires an extra
+    // post-take consistency check (see below).
     uint256 contFee = continuousFee(id);
     uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
-
     // Economic viability constraint: the total continuous fee cannot exceed 100% of credit
     // (contFee * timeToMaturity / WAD <= 1). Without this, accrual inside _updatePosition
     // inflates buyerCreditIncrease above creditDelta, pushing pendingFeeDelta above the formula.
     // In practice MAX_CONTINUOUS_FEE = 317097919 (~1% APR) with realistic maturities keeps r << 1.
     require to_mathint(contFee) * to_mathint(timeToMaturity) <= WAD();
 
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
+
+    require id == lastId;
+    // touchObligation sets continuousFee = defaultContinuousFee[loanToken] on first creation, so
+    // the pre-take storage value could differ from the value actually used inside take. Requiring
+    // equality pins the pre-read to the post-take value, ensuring our formula uses the same contFee
+    // that the Solidity code applied. For already-created obligations this is trivially satisfied.
+    require continuousFee(id) == contFee;
+
     uint256 creditAfter = creditOf(id, lender);
     uint256 pendingFeeAfter = pendingFee(id, lender);
 

From d24eedfe20e82953ef7aea4c2a9cc9ed364a4b00 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Thu, 2 Apr 2026 23:34:54 +0200
Subject: [PATCH 04/27] simplified the rules

---
 certora/specs/ContinuousFeeProtection.spec | 61 ++++++----------------
 1 file changed, 16 insertions(+), 45 deletions(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index 49e960916..ed33ad7ff 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -17,7 +17,6 @@ methods {
     function userLossIndex(bytes32 id, address user) external returns (uint128) envfree;
     function lossIndex(bytes32 id) external returns (uint128) envfree;
     function lastAccrual(bytes32 id, address user) external returns (uint128) envfree;
-    function updatePositionView(Midnight.Obligation memory obligation, bytes32 id, address user) external returns (uint128, uint128, uint128);
 
     function _.price() external => NONDET;
     function signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET;
@@ -58,70 +57,42 @@ function passiveFeeRecipient() returns address {
 
 definition WAD() returns uint256 = 10 ^ 18;
 
-// The continuous fee is never overcharged: when a lender's credit increases via a buy-offer
-// take, their pendingFee increases by at most floor(creditIncrease * continuousFee * timeToMaturity / WAD).
-// This is a rounding-favors-maker guarantee: mulDivDown means the lender pays the floor, never the ceiling.
-// Pending accrual is not required: time-based fee drainage inside _updatePosition only
-// reduces pendingFeeDelta, never raises it. Pending slash and lossIndex saturation must still
-// be excluded because they wipe credit without proportionally reducing pendingFee, breaking the inequality.
-rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address lender) {
+rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
     require offer.buy;
-
-    // PASSIVE_FEE_RECIPIENT receives extra credit from every _updatePosition call on other
-    // positions (line 682 of Midnight.sol), so their credit change is not governed solely
-    // by the continuousFee formula.
-    require lender != passiveFeeRecipient();
+    require offer.maker != passiveFeeRecipient();
 
     bytes32 id;
-    uint256 creditBefore = creditOf(id, lender);
-    uint256 pendingFeeBefore = pendingFee(id, lender);
-    require pendingFeeBefore <= creditBefore;
-    require userLossIndex(id, lender) == lossIndex(id); // no pending slash: slashing reduces creditDelta without proportionally reducing pendingFeeDelta, which can push pendingFeeDelta above the formula
-    require lossIndex(id) < max_uint128; // excludes lossIndex saturation: same risk as pending slash — credit is wiped unconditionally, shrinking creditDelta without a matching reduction in pendingFeeDelta
-
-    // Read contFee and timeToMaturity before take so the prover can use these constraints to
-    // prune execution paths inside take(). timeToMaturity is a pure function of the offer fields
-    // (which don't change), so it's consistent before and after. contFee requires an extra
-    // post-take consistency check (see below).
-    uint256 contFee = continuousFee(id);
-    uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
-    // Economic viability constraint: the total continuous fee cannot exceed 100% of credit
-    // (contFee * timeToMaturity / WAD <= 1). Without this, accrual inside _updatePosition
-    // inflates buyerCreditIncrease above creditDelta, pushing pendingFeeDelta above the formula.
-    // In practice MAX_CONTINUOUS_FEE = 317097919 (~1% APR) with realistic maturities keeps r << 1.
-    require to_mathint(contFee) * to_mathint(timeToMaturity) <= WAD();
+    uint128 postUpdateCredit;
+    uint128 postUpdatePendingFee;
+    uint128 accruedFee;
+    postUpdateCredit, postUpdatePendingFee, accruedFee = updatePositionView(e, offer.obligation, id, offer.maker);
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 
     require id == lastId;
-    // touchObligation sets continuousFee = defaultContinuousFee[loanToken] on first creation, so
-    // the pre-take storage value could differ from the value actually used inside take. Requiring
-    // equality pins the pre-read to the post-take value, ensuring our formula uses the same contFee
-    // that the Solidity code applied. For already-created obligations this is trivially satisfied.
-    require continuousFee(id) == contFee;
 
-    uint256 creditAfter = creditOf(id, lender);
-    uint256 pendingFeeAfter = pendingFee(id, lender);
+    uint256 contFee = continuousFee(id);
+    uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
 
-    mathint creditDelta = to_mathint(creditAfter) - to_mathint(creditBefore);
-    mathint pendingFeeDelta = to_mathint(pendingFeeAfter) - to_mathint(pendingFeeBefore);
+    mathint creditDelta = to_mathint(creditOf(id, offer.maker)) - to_mathint(postUpdateCredit);
+    mathint pendingFeeDelta = to_mathint(pendingFee(id, offer.maker)) - to_mathint(postUpdatePendingFee);
 
-    require creditDelta >= 0; // scope to buyers gaining credit
+    require creditDelta >= 0;
     assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
 }
 
 // When a seller's credit decreases via a take, their pendingFee decreases by
 // exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
 // updatePositionView accounts for slash and accrual before the proportional formula runs.
-rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address seller) {
+rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
     require !offer.buy;
-    require seller != passiveFeeRecipient();
+    require offer.maker != passiveFeeRecipient();
 
     bytes32 id;
     uint128 postUpdateCredit;
     uint128 postUpdatePendingFee;
     uint128 accruedFee;
-    postUpdateCredit, postUpdatePendingFee, accruedFee = updatePositionView(e, offer.obligation, id, seller);
+    postUpdateCredit, postUpdatePendingFee, accruedFee = updatePositionView(e, offer.obligation, id, offer.maker);
 
     // The Solidity mulDivUp is skipped when sellerPos.credit == 0 after _updatePosition,
     // leaving pendingFee unchanged. Require credit > 0 to stay in the proportional branch.
@@ -131,8 +102,8 @@ rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker
 
     require id == lastId;
 
-    uint256 creditAfter = creditOf(id, seller);
-    uint256 pendingFeeAfter = pendingFee(id, seller);
+    uint256 creditAfter = creditOf(id, offer.maker);
+    uint256 pendingFeeAfter = pendingFee(id, offer.maker);
 
     mathint creditDelta = to_mathint(creditAfter) - to_mathint(postUpdateCredit);
     mathint pendingFeeDelta = to_mathint(pendingFeeAfter) - to_mathint(postUpdatePendingFee);

From a420942e46335f7fb5b8052e5071c516b966b8e4 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Fri, 3 Apr 2026 00:09:40 +0200
Subject: [PATCH 05/27] added comments

---
 certora/specs/ContinuousFeeProtection.spec | 67 +++++++++-------------
 1 file changed, 28 insertions(+), 39 deletions(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index ed33ad7ff..80391f880 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -4,8 +4,6 @@ methods {
     function multicall(bytes[]) external => HAVOC_ALL DELETE;
 
     function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation, chainId, midnight);
-    function UtilsLib.mulDivDown(uint256 a, uint256 b, uint256 denominator) internal returns (uint256) => CVL_mulDivDown(a, b, denominator);
-    function UtilsLib.mulDivUp(uint256 a, uint256 b, uint256 denominator) internal returns (uint256) => CVL_mulDivUp(a, b, denominator);
     function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
     function TickLib.wExp(int256) internal returns (uint256) => NONDET;
     function UtilsLib.msb(uint128) internal returns (uint256) => NONDET;
@@ -30,46 +28,39 @@ methods {
     function _.canIncreaseDebt(address) external => NONDET;
 }
 
+/// HELPERS ///
+
 // IdLib summary: remember the last id returned by toId.
+
 persistent ghost bytes32 lastId;
 
 function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midnight) returns bytes32 {
+    // non-deterministic id
     bytes32 id;
     lastId = id;
     return id;
 }
 
-// Exact mulDivDown: floor(a * b / d)
-function CVL_mulDivDown(uint256 a, uint256 b, uint256 d) returns uint256 {
-    require d > 0, "see NoDivisionByZero.spec";
-    return require_uint256((to_mathint(a) * to_mathint(b)) / to_mathint(d));
-}
-
-// Exact mulDivUp: ceil(a * b / d)
-function CVL_mulDivUp(uint256 a, uint256 b, uint256 d) returns uint256 {
-    require d > 0, "see NoDivisionByZero.spec";
-    return require_uint256((to_mathint(a) * to_mathint(b) + to_mathint(d) - 1) / to_mathint(d));
-}
-
 function passiveFeeRecipient() returns address {
     return 0x7e3dce7c19791d65d67ef7ce3c42d2b7fe6fecb1;
 }
 
 definition WAD() returns uint256 = 10 ^ 18;
 
-rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
-    require offer.buy;
-    require offer.maker != passiveFeeRecipient();
+// In a buy-offer take, the buyer's pendingFee increases by at most floor(creditIncrease * continuousFee * timeToMaturity / WAD).
+// Measured from the post-update baseline (after slash and accrual) so that only the new-credit fee contribution is bounded.
+rule continuousFeeNotOverchargedInBuyOffer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+    require offer.maker != passiveFeeRecipient(), "Passive Fee Recipient can't call take()";
 
     bytes32 id;
     uint128 postUpdateCredit;
     uint128 postUpdatePendingFee;
-    uint128 accruedFee;
-    postUpdateCredit, postUpdatePendingFee, accruedFee = updatePositionView(e, offer.obligation, id, offer.maker);
+
+    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, offer.maker);
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 
-    require id == lastId;
+    require id == lastId, "id should be derived from obligation";
 
     uint256 contFee = continuousFee(id);
     uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
@@ -77,30 +68,25 @@ rule continuousFeeNotOvercharged(env e, uint256 units, address taker, address ta
     mathint creditDelta = to_mathint(creditOf(id, offer.maker)) - to_mathint(postUpdateCredit);
     mathint pendingFeeDelta = to_mathint(pendingFee(id, offer.maker)) - to_mathint(postUpdatePendingFee);
 
-    require creditDelta >= 0;
-    assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+    require creditDelta >= 0, "take only adds credit to the maker in a buy-offer";
+
+    assert !offer.buy || pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
 }
 
 // When a seller's credit decreases via a take, their pendingFee decreases by
 // exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
-// updatePositionView accounts for slash and accrual before the proportional formula runs.
-rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
-    require !offer.buy;
-    require offer.maker != passiveFeeRecipient();
+rule pendingFeeDecreasesProportionallyInSellOffer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+    require offer.maker != passiveFeeRecipient(), "Passive Fee Recipient can't call take()";
 
     bytes32 id;
     uint128 postUpdateCredit;
     uint128 postUpdatePendingFee;
-    uint128 accruedFee;
-    postUpdateCredit, postUpdatePendingFee, accruedFee = updatePositionView(e, offer.obligation, id, offer.maker);
 
-    // The Solidity mulDivUp is skipped when sellerPos.credit == 0 after _updatePosition,
-    // leaving pendingFee unchanged. Require credit > 0 to stay in the proportional branch.
-    require postUpdateCredit > 0;
+    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, offer.maker);
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 
-    require id == lastId;
+    require id == lastId, "id should be derived from obligation";
 
     uint256 creditAfter = creditOf(id, offer.maker);
     uint256 pendingFeeAfter = pendingFee(id, offer.maker);
@@ -110,19 +96,22 @@ rule sellerPendingFeeDecreasesProportionally(env e, uint256 units, address taker
 
     require creditDelta <= 0; // scope to sellers losing credit
     mathint creditDecrease = -creditDelta;
-    assert pendingFeeDelta == -((to_mathint(postUpdatePendingFee) * creditDecrease + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit));
+    require offer.buy == false, "take only removes credit from the maker in a sell-offer";
+
+    // if postUpdateCredit is zero, then pendingFeeDelta is also zero, else equals ceil(creditDecrease * postUpdatePendingFee / postUpdateCredit).
+    assert postUpdateCredit == 0 || pendingFeeDelta == -((to_mathint(postUpdatePendingFee) * creditDecrease + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit));
+    assert postUpdateCredit != 0 || pendingFeeDelta == 0;
 }
 
 // take() must not modify credit or pendingFee of any address other than the buyer, seller,
-// and PASSIVE_FEE_RECIPIENT. This catches accidental writes to wrong positions (e.g. wrong id,
-// wrong user) and callback side-effects.
+// and PASSIVE_FEE_RECIPIENT.
 rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address user) {
     address buyer = offer.buy ? offer.maker : taker;
     address seller = offer.buy ? taker : offer.maker;
 
-    require user != buyer;
-    require user != seller;
-    require user != passiveFeeRecipient();
+    require user != buyer, "user is a third party, different from buyer";
+    require user != seller, "user is a third party, different from seller";
+    require user != passiveFeeRecipient(), "user is a third party, different from passive fee recipient";
 
     bytes32 id;
     uint256 creditBefore = creditOf(id, user);
@@ -130,7 +119,7 @@ rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 
-    require id == lastId;
+    require id == lastId, "id should be derived from obligation";
 
     assert creditOf(id, user) == creditBefore;
     assert pendingFee(id, user) == pendingFeeBefore;

From 106a234cd8f288f6ce423ba54dfd0c532b5650a5 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Mon, 6 Apr 2026 18:16:43 +0200
Subject: [PATCH 06/27] cleaned up assumptions

---
 certora/confs/ContinuousFeeProtection.conf |  3 +-
 certora/specs/ContinuousFeeProtection.spec | 32 ++++++++++------------
 2 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/certora/confs/ContinuousFeeProtection.conf b/certora/confs/ContinuousFeeProtection.conf
index ffbf922d1..78791341e 100644
--- a/certora/confs/ContinuousFeeProtection.conf
+++ b/certora/confs/ContinuousFeeProtection.conf
@@ -1,6 +1,7 @@
 {
   "files": [
-    "src/Midnight.sol"
+    "src/Midnight.sol",
+    "certora/helpers/Utils.sol"
   ],
   "verify": "Midnight:certora/specs/ContinuousFeeProtection.spec",
   "solc": "solc-0.8.31",
diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index 80391f880..874d5bb6e 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -1,5 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
+using Utils as Utils;
+
 methods {
     function multicall(bytes[]) external => HAVOC_ALL DELETE;
 
@@ -15,6 +17,7 @@ methods {
     function userLossIndex(bytes32 id, address user) external returns (uint128) envfree;
     function lossIndex(bytes32 id) external returns (uint128) envfree;
     function lastAccrual(bytes32 id, address user) external returns (uint128) envfree;
+    function Utils.continuousFeeRecipient() external returns (address) envfree;
 
     function _.price() external => NONDET;
     function signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET;
@@ -41,16 +44,12 @@ function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midni
     return id;
 }
 
-function passiveFeeRecipient() returns address {
-    return 0x7e3dce7c19791d65d67ef7ce3c42d2b7fe6fecb1;
-}
-
 definition WAD() returns uint256 = 10 ^ 18;
 
 // In a buy-offer take, the buyer's pendingFee increases by at most floor(creditIncrease * continuousFee * timeToMaturity / WAD).
 // Measured from the post-update baseline (after slash and accrual) so that only the new-credit fee contribution is bounded.
 rule continuousFeeNotOverchargedInBuyOffer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
-    require offer.maker != passiveFeeRecipient(), "Passive Fee Recipient can't call take()";
+    require offer.maker != Utils.continuousFeeRecipient(), "Continuous Fee Recipient can't call take()";
 
     bytes32 id;
     uint128 postUpdateCredit;
@@ -68,15 +67,16 @@ rule continuousFeeNotOverchargedInBuyOffer(env e, uint256 units, address taker,
     mathint creditDelta = to_mathint(creditOf(id, offer.maker)) - to_mathint(postUpdateCredit);
     mathint pendingFeeDelta = to_mathint(pendingFee(id, offer.maker)) - to_mathint(postUpdatePendingFee);
 
-    require creditDelta >= 0, "take only adds credit to the maker in a buy-offer";
+    require offer.buy, "maker is the buyer only in a buy-offer";
 
-    assert !offer.buy || pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+    assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
 }
 
 // When a seller's credit decreases via a take, their pendingFee decreases by
 // exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
 rule pendingFeeDecreasesProportionallyInSellOffer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
-    require offer.maker != passiveFeeRecipient(), "Passive Fee Recipient can't call take()";
+    require offer.maker != Utils.continuousFeeRecipient(), "Continuous Fee Recipient can't call take()";
+    //require offer.maker != taker, "maker and taker are the same address";
 
     bytes32 id;
     uint128 postUpdateCredit;
@@ -84,6 +84,8 @@ rule pendingFeeDecreasesProportionallyInSellOffer(env e, uint256 units, address
 
     postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, offer.maker);
 
+    require postUpdateCredit > 0 || postUpdatePendingFee == 0, "noRemainingContinuousFeeWithoutCredit: credit == 0 => pendingFee == 0";
+
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 
     require id == lastId, "id should be derived from obligation";
@@ -91,27 +93,23 @@ rule pendingFeeDecreasesProportionallyInSellOffer(env e, uint256 units, address
     uint256 creditAfter = creditOf(id, offer.maker);
     uint256 pendingFeeAfter = pendingFee(id, offer.maker);
 
-    mathint creditDelta = to_mathint(creditAfter) - to_mathint(postUpdateCredit);
-    mathint pendingFeeDelta = to_mathint(pendingFeeAfter) - to_mathint(postUpdatePendingFee);
+    mathint creditDelta = to_mathint(postUpdateCredit) - to_mathint(creditAfter);
+    mathint pendingFeeDelta = to_mathint(postUpdatePendingFee) - to_mathint(pendingFeeAfter);
 
-    require creditDelta <= 0; // scope to sellers losing credit
-    mathint creditDecrease = -creditDelta;
     require offer.buy == false, "take only removes credit from the maker in a sell-offer";
 
     // if postUpdateCredit is zero, then pendingFeeDelta is also zero, else equals ceil(creditDecrease * postUpdatePendingFee / postUpdateCredit).
-    assert postUpdateCredit == 0 || pendingFeeDelta == -((to_mathint(postUpdatePendingFee) * creditDecrease + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit));
-    assert postUpdateCredit != 0 || pendingFeeDelta == 0;
+    assert postUpdateCredit == 0 || pendingFeeDelta == (to_mathint(postUpdatePendingFee) * creditDelta + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit);
 }
 
-// take() must not modify credit or pendingFee of any address other than the buyer, seller,
-// and PASSIVE_FEE_RECIPIENT.
+// take() must not modify credit or pendingFee of any address other than the buyer, seller, and CONTINUOUS_FEE_RECIPIENT.
 rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address user) {
     address buyer = offer.buy ? offer.maker : taker;
     address seller = offer.buy ? taker : offer.maker;
 
     require user != buyer, "user is a third party, different from buyer";
     require user != seller, "user is a third party, different from seller";
-    require user != passiveFeeRecipient(), "user is a third party, different from passive fee recipient";
+    require user != Utils.continuousFeeRecipient(), "user is a third party, different from continuous fee recipient";
 
     bytes32 id;
     uint256 creditBefore = creditOf(id, user);

From 22e51e761fabd3aa2f1ad12cda7465c6b132d1af Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Mon, 6 Apr 2026 21:14:23 +0200
Subject: [PATCH 07/27] addded a rule on fees accrued

---
 certora/confs/ContinuousFeeProtection.conf |  5 +-
 certora/specs/ContinuousFeeProtection.spec | 60 ++++++++++++----------
 2 files changed, 35 insertions(+), 30 deletions(-)

diff --git a/certora/confs/ContinuousFeeProtection.conf b/certora/confs/ContinuousFeeProtection.conf
index 78791341e..4071e3e0a 100644
--- a/certora/confs/ContinuousFeeProtection.conf
+++ b/certora/confs/ContinuousFeeProtection.conf
@@ -1,10 +1,9 @@
 {
   "files": [
-    "src/Midnight.sol",
-    "certora/helpers/Utils.sol"
+    "src/Midnight.sol"
   ],
   "verify": "Midnight:certora/specs/ContinuousFeeProtection.spec",
-  "solc": "solc-0.8.31",
+  "solc": "solc-0.8.34",
   "solc_evm_version": "osaka",
   "optimistic_hashing": true,
   "hashing_length_bound": 2048,
diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index 874d5bb6e..c4dc93387 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -1,34 +1,29 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-using Utils as Utils;
-
 methods {
-    function multicall(bytes[]) external => HAVOC_ALL DELETE;
-
     function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation, chainId, midnight);
-    function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
-    function TickLib.wExp(int256) internal returns (uint256) => NONDET;
-    function UtilsLib.msb(uint128) internal returns (uint256) => NONDET;
-    function tradingFee(bytes32 id, uint256 timeToMaturity) internal returns (uint256) => NONDET;
 
     function creditOf(bytes32 id, address user) external returns (uint256) envfree;
     function pendingFee(bytes32 id, address user) external returns (uint128) envfree;
     function continuousFee(bytes32 id) external returns (uint32) envfree;
+    function continuousFeeCredit(bytes32 id) external returns (uint256) envfree;
     function userLossIndex(bytes32 id, address user) external returns (uint128) envfree;
     function lossIndex(bytes32 id) external returns (uint128) envfree;
     function lastAccrual(bytes32 id, address user) external returns (uint128) envfree;
-    function Utils.continuousFeeRecipient() external returns (address) envfree;
 
     function _.price() external => NONDET;
     function signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET;
     function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET;
+    function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET;
     function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET;
     function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
-    function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, uint256, bytes) external => NONDET;
-    function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, uint256, bytes) external => NONDET;
+    function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
+    function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
     function isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET;
     function _.canIncreaseCredit(address) external => NONDET;
     function _.canIncreaseDebt(address) external => NONDET;
+    function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
+    function tradingFee(bytes32 id, uint256 timeToMaturity) internal returns (uint256) => NONDET;
 }
 
 /// HELPERS ///
@@ -47,10 +42,7 @@ function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midni
 definition WAD() returns uint256 = 10 ^ 18;
 
 // In a buy-offer take, the buyer's pendingFee increases by at most floor(creditIncrease * continuousFee * timeToMaturity / WAD).
-// Measured from the post-update baseline (after slash and accrual) so that only the new-credit fee contribution is bounded.
 rule continuousFeeNotOverchargedInBuyOffer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
-    require offer.maker != Utils.continuousFeeRecipient(), "Continuous Fee Recipient can't call take()";
-
     bytes32 id;
     uint128 postUpdateCredit;
     uint128 postUpdatePendingFee;
@@ -67,24 +59,20 @@ rule continuousFeeNotOverchargedInBuyOffer(env e, uint256 units, address taker,
     mathint creditDelta = to_mathint(creditOf(id, offer.maker)) - to_mathint(postUpdateCredit);
     mathint pendingFeeDelta = to_mathint(pendingFee(id, offer.maker)) - to_mathint(postUpdatePendingFee);
 
-    require offer.buy, "maker is the buyer only in a buy-offer";
+    require offer.buy, "scope to buy offers";
 
     assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
 }
 
-// When a seller's credit decreases via a take, their pendingFee decreases by
-// exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
+// When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
 rule pendingFeeDecreasesProportionallyInSellOffer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
-    require offer.maker != Utils.continuousFeeRecipient(), "Continuous Fee Recipient can't call take()";
-    //require offer.maker != taker, "maker and taker are the same address";
-
     bytes32 id;
     uint128 postUpdateCredit;
     uint128 postUpdatePendingFee;
 
     postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, offer.maker);
 
-    require postUpdateCredit > 0 || postUpdatePendingFee == 0, "noRemainingContinuousFeeWithoutCredit: credit == 0 => pendingFee == 0";
+    require postUpdateCredit > 0 || postUpdatePendingFee == 0, "noRemainingContinuousFeeWithoutCredit";
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 
@@ -96,20 +84,38 @@ rule pendingFeeDecreasesProportionallyInSellOffer(env e, uint256 units, address
     mathint creditDelta = to_mathint(postUpdateCredit) - to_mathint(creditAfter);
     mathint pendingFeeDelta = to_mathint(postUpdatePendingFee) - to_mathint(pendingFeeAfter);
 
-    require offer.buy == false, "take only removes credit from the maker in a sell-offer";
+    require offer.buy == false, "scope to sell offers";
 
-    // if postUpdateCredit is zero, then pendingFeeDelta is also zero, else equals ceil(creditDecrease * postUpdatePendingFee / postUpdateCredit).
     assert postUpdateCredit == 0 || pendingFeeDelta == (to_mathint(postUpdatePendingFee) * creditDelta + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit);
 }
 
-// take() must not modify credit or pendingFee of any address other than the buyer, seller, and CONTINUOUS_FEE_RECIPIENT.
+// take() increases continuousFeeCredit by exactly the accrued fees of the buyer and seller.
+rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+    address buyer = offer.buy ? offer.maker : taker;
+    address seller = offer.buy ? taker : offer.maker;
+
+    bytes32 id;
+    uint128 buyerAccruedFee;
+    uint128 sellerAccruedFee;
+
+    _, _, buyerAccruedFee = updatePositionView(e, offer.obligation, id, buyer);
+    _, _, sellerAccruedFee = updatePositionView(e, offer.obligation, id, seller);
+
+    uint256 continuousFeeCreditBefore = continuousFeeCredit(id);
+
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
+
+    require id == lastId, "id should be derived from obligation";
+
+    assert continuousFeeCredit(id) == continuousFeeCreditBefore + buyerAccruedFee + sellerAccruedFee;
+}
+
+// take() must not modify credit or pendingFee of any address other than the buyer and seller.
 rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address user) {
     address buyer = offer.buy ? offer.maker : taker;
     address seller = offer.buy ? taker : offer.maker;
 
-    require user != buyer, "user is a third party, different from buyer";
-    require user != seller, "user is a third party, different from seller";
-    require user != Utils.continuousFeeRecipient(), "user is a third party, different from continuous fee recipient";
+    require user != buyer && user != seller, "user is different from buyer and seller";
 
     bytes32 id;
     uint256 creditBefore = creditOf(id, user);

From ba11b43ed5bdf92148740caa84473cd12940a6c7 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Mon, 6 Apr 2026 22:00:10 +0200
Subject: [PATCH 08/27] added comment for tExchange summary

---
 certora/specs/ContinuousFeeProtection.spec | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index c4dc93387..1f2677f42 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -14,7 +14,6 @@ methods {
     function _.price() external => NONDET;
     function signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET;
     function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET;
-    function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET;
     function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET;
     function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
     function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
@@ -24,6 +23,9 @@ methods {
     function _.canIncreaseDebt(address) external => NONDET;
     function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
     function tradingFee(bytes32 id, uint256 timeToMaturity) internal returns (uint256) => NONDET;
+
+    // the properties are about pendingFee/ credit accounting, and not liquidation interactions.
+    function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET;
 }
 
 /// HELPERS ///

From 5158e106076f0a061a657e5f3f76a887478928e8 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Tue, 7 Apr 2026 08:49:00 +0200
Subject: [PATCH 09/27] tuned comment

---
 certora/specs/ContinuousFeeProtection.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index 1f2677f42..fe67a0192 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -74,7 +74,7 @@ rule pendingFeeDecreasesProportionallyInSellOffer(env e, uint256 units, address
 
     postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, offer.maker);
 
-    require postUpdateCredit > 0 || postUpdatePendingFee == 0, "noRemainingContinuousFeeWithoutCredit";
+    require postUpdateCredit > 0 || postUpdatePendingFee == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec";
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 

From b93e58b8d48aeb4267ad649378616bfcab6cea08 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Tue, 7 Apr 2026 12:10:48 +0200
Subject: [PATCH 10/27] generalised the rule: states for buyers/sellers and not
 makers/takers; assert updatePositionView are equal before and after take

---
 certora/specs/ContinuousFeeProtection.spec | 44 +++++++++++++---------
 1 file changed, 26 insertions(+), 18 deletions(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index fe67a0192..ae05e0b05 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -43,13 +43,15 @@ function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midni
 
 definition WAD() returns uint256 = 10 ^ 18;
 
-// In a buy-offer take, the buyer's pendingFee increases by at most floor(creditIncrease * continuousFee * timeToMaturity / WAD).
-rule continuousFeeNotOverchargedInBuyOffer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+// The buyer's pendingFee increases by at most floor(creditIncrease * continuousFee * timeToMaturity / WAD).
+rule continuousFeeNotOverchargedBuyer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+    address buyer = offer.buy ? offer.maker : taker;
+
     bytes32 id;
     uint128 postUpdateCredit;
     uint128 postUpdatePendingFee;
 
-    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, offer.maker);
+    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, buyer);
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 
@@ -58,21 +60,21 @@ rule continuousFeeNotOverchargedInBuyOffer(env e, uint256 units, address taker,
     uint256 contFee = continuousFee(id);
     uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
 
-    mathint creditDelta = to_mathint(creditOf(id, offer.maker)) - to_mathint(postUpdateCredit);
-    mathint pendingFeeDelta = to_mathint(pendingFee(id, offer.maker)) - to_mathint(postUpdatePendingFee);
-
-    require offer.buy, "scope to buy offers";
+    mathint creditDelta = to_mathint(creditOf(id, buyer)) - to_mathint(postUpdateCredit);
+    mathint pendingFeeDelta = to_mathint(pendingFee(id, buyer)) - to_mathint(postUpdatePendingFee);
 
     assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
 }
 
 // When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
-rule pendingFeeDecreasesProportionallyInSellOffer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+rule pendingFeeDecreasesProportionallySeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+    address seller = offer.buy ? taker : offer.maker;
+
     bytes32 id;
     uint128 postUpdateCredit;
     uint128 postUpdatePendingFee;
 
-    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, offer.maker);
+    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, seller);
 
     require postUpdateCredit > 0 || postUpdatePendingFee == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec";
 
@@ -80,14 +82,12 @@ rule pendingFeeDecreasesProportionallyInSellOffer(env e, uint256 units, address
 
     require id == lastId, "id should be derived from obligation";
 
-    uint256 creditAfter = creditOf(id, offer.maker);
-    uint256 pendingFeeAfter = pendingFee(id, offer.maker);
+    uint256 creditAfter = creditOf(id, seller);
+    uint256 pendingFeeAfter = pendingFee(id, seller);
 
     mathint creditDelta = to_mathint(postUpdateCredit) - to_mathint(creditAfter);
     mathint pendingFeeDelta = to_mathint(postUpdatePendingFee) - to_mathint(pendingFeeAfter);
 
-    require offer.buy == false, "scope to sell offers";
-
     assert postUpdateCredit == 0 || pendingFeeDelta == (to_mathint(postUpdatePendingFee) * creditDelta + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit);
 }
 
@@ -112,7 +112,7 @@ rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address tak
     assert continuousFeeCredit(id) == continuousFeeCreditBefore + buyerAccruedFee + sellerAccruedFee;
 }
 
-// take() must not modify credit or pendingFee of any address other than the buyer and seller.
+// updatePositionView()
 rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address user) {
     address buyer = offer.buy ? offer.maker : taker;
     address seller = offer.buy ? taker : offer.maker;
@@ -120,13 +120,21 @@ rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address
     require user != buyer && user != seller, "user is different from buyer and seller";
 
     bytes32 id;
-    uint256 creditBefore = creditOf(id, user);
-    uint256 pendingFeeBefore = pendingFee(id, user);
+    uint256 postUpdateCreditBefore;
+    uint256 postUpdatePendingFeeBefore;
+    uint256 userAccruedFeeBefore;
+    postUpdateCreditBefore, postUpdatePendingFeeBefore, userAccruedFeeBefore = updatePositionView(e, offer.obligation, id, user);
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
 
     require id == lastId, "id should be derived from obligation";
 
-    assert creditOf(id, user) == creditBefore;
-    assert pendingFee(id, user) == pendingFeeBefore;
+    uint256 postUpdateCreditAfter;
+    uint256 postUpdatePendingFeeAfter;
+    uint256 userAccruedFeeAfter;
+    postUpdateCreditAfter, postUpdatePendingFeeAfter, userAccruedFeeAfter = updatePositionView(e, offer.obligation, id, user);
+
+    assert postUpdateCreditBefore == postUpdateCreditAfter, "take should not change credit of third party";
+    assert postUpdatePendingFeeBefore == postUpdatePendingFeeAfter, "take should not change pending fee of third party";
+    assert userAccruedFeeBefore == userAccruedFeeAfter, "take should not change accrued fee of third party";
 }

From fcfd984ac919908a0695cabe2e5af1784b11a986 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Tue, 7 Apr 2026 13:17:04 +0200
Subject: [PATCH 11/27] tuned comment

---
 certora/specs/ContinuousFeeProtection.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index ae05e0b05..3983a8be2 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -66,7 +66,7 @@ rule continuousFeeNotOverchargedBuyer(env e, uint256 units, address taker, addre
     assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
 }
 
-// When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
+// When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(PendingFee * creditDelta / postUpdateCredit).
 rule pendingFeeDecreasesProportionallySeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
     address seller = offer.buy ? taker : offer.maker;
 

From 00e6cea53876d82cbd0a68d9e4f0841bc2b5e2f1 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Tue, 7 Apr 2026 13:47:58 +0200
Subject: [PATCH 12/27] adapted to ratifications introduced in 588

---
 certora/specs/ContinuousFeeProtection.spec | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index 3983a8be2..360dbac02 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -12,7 +12,7 @@ methods {
     function lastAccrual(bytes32 id, address user) external returns (uint128) envfree;
 
     function _.price() external => NONDET;
-    function signer(bytes32, Midnight.Signature memory) internal returns (address) => NONDET;
+    function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET;
     function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET;
     function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET;
     function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
@@ -44,7 +44,7 @@ function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midni
 definition WAD() returns uint256 = 10 ^ 18;
 
 // The buyer's pendingFee increases by at most floor(creditIncrease * continuousFee * timeToMaturity / WAD).
-rule continuousFeeNotOverchargedBuyer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+rule continuousFeeNotOverchargedBuyer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
     address buyer = offer.buy ? offer.maker : taker;
 
     bytes32 id;
@@ -53,7 +53,7 @@ rule continuousFeeNotOverchargedBuyer(env e, uint256 units, address taker, addre
 
     postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, buyer);
 
-    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof);
 
     require id == lastId, "id should be derived from obligation";
 
@@ -67,7 +67,7 @@ rule continuousFeeNotOverchargedBuyer(env e, uint256 units, address taker, addre
 }
 
 // When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(PendingFee * creditDelta / postUpdateCredit).
-rule pendingFeeDecreasesProportionallySeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+rule pendingFeeDecreasesProportionallySeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
     address seller = offer.buy ? taker : offer.maker;
 
     bytes32 id;
@@ -78,7 +78,7 @@ rule pendingFeeDecreasesProportionallySeller(env e, uint256 units, address taker
 
     require postUpdateCredit > 0 || postUpdatePendingFee == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec";
 
-    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof);
 
     require id == lastId, "id should be derived from obligation";
 
@@ -92,7 +92,7 @@ rule pendingFeeDecreasesProportionallySeller(env e, uint256 units, address taker
 }
 
 // take() increases continuousFeeCredit by exactly the accrued fees of the buyer and seller.
-rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof) {
+rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
     address buyer = offer.buy ? offer.maker : taker;
     address seller = offer.buy ? taker : offer.maker;
 
@@ -105,7 +105,7 @@ rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address tak
 
     uint256 continuousFeeCreditBefore = continuousFeeCredit(id);
 
-    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof);
 
     require id == lastId, "id should be derived from obligation";
 
@@ -113,7 +113,7 @@ rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address tak
 }
 
 // updatePositionView()
-rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, Midnight.Signature signature, bytes32 root, bytes32[] proof, address user) {
+rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof, address user) {
     address buyer = offer.buy ? offer.maker : taker;
     address seller = offer.buy ? taker : offer.maker;
 
@@ -125,7 +125,7 @@ rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address
     uint256 userAccruedFeeBefore;
     postUpdateCreditBefore, postUpdatePendingFeeBefore, userAccruedFeeBefore = updatePositionView(e, offer.obligation, id, user);
 
-    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, signature, root, proof);
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof);
 
     require id == lastId, "id should be derived from obligation";
 

From d3e93aa2a8a904aed05116791dfd3cc7b92822ee Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Tue, 7 Apr 2026 17:12:07 +0200
Subject: [PATCH 13/27] no more separation of buyer and seller case

---
 certora/specs/ContinuousFeeProtection.spec | 51 ++++++++--------------
 1 file changed, 19 insertions(+), 32 deletions(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index 360dbac02..d4b93242f 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -43,15 +43,23 @@ function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midni
 
 definition WAD() returns uint256 = 10 ^ 18;
 
-// The buyer's pendingFee increases by at most floor(creditIncrease * continuousFee * timeToMaturity / WAD).
-rule continuousFeeNotOverchargedBuyer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
+// take() updates buyer and seller pending fees according to their post-update credit changes:
+// 1. the buyer's pendingFee increases by floor(creditIncrease * continuousFee * timeToMaturity / WAD).
+// 2. the seller's pendingFee decreases by exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
+rule pendingFeeAdjustedForBuyerAndSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
     address buyer = offer.buy ? offer.maker : taker;
+    address seller = offer.buy ? taker : offer.maker;
 
     bytes32 id;
-    uint128 postUpdateCredit;
-    uint128 postUpdatePendingFee;
+    uint128 buyerPostUpdateCredit;
+    uint128 buyerPostUpdatePendingFee;
+    uint128 sellerPostUpdateCredit;
+    uint128 sellerPostUpdatePendingFee;
+
+    buyerPostUpdateCredit, buyerPostUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, buyer);
+    sellerPostUpdateCredit, sellerPostUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, seller);
 
-    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, buyer);
+    require sellerPostUpdateCredit > 0 || sellerPostUpdatePendingFee == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec";
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof);
 
@@ -60,35 +68,14 @@ rule continuousFeeNotOverchargedBuyer(env e, uint256 units, address taker, addre
     uint256 contFee = continuousFee(id);
     uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
 
-    mathint creditDelta = to_mathint(creditOf(id, buyer)) - to_mathint(postUpdateCredit);
-    mathint pendingFeeDelta = to_mathint(pendingFee(id, buyer)) - to_mathint(postUpdatePendingFee);
-
-    assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
-}
-
-// When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(PendingFee * creditDelta / postUpdateCredit).
-rule pendingFeeDecreasesProportionallySeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
-    address seller = offer.buy ? taker : offer.maker;
-
-    bytes32 id;
-    uint128 postUpdateCredit;
-    uint128 postUpdatePendingFee;
-
-    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, seller);
-
-    require postUpdateCredit > 0 || postUpdatePendingFee == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec";
-
-    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof);
-
-    require id == lastId, "id should be derived from obligation";
-
-    uint256 creditAfter = creditOf(id, seller);
-    uint256 pendingFeeAfter = pendingFee(id, seller);
+    mathint buyerCreditIncrease = to_mathint(creditOf(id, buyer)) - to_mathint(buyerPostUpdateCredit);
+    mathint buyerPendingFeeIncrease = to_mathint(pendingFee(id, buyer)) - to_mathint(buyerPostUpdatePendingFee);
 
-    mathint creditDelta = to_mathint(postUpdateCredit) - to_mathint(creditAfter);
-    mathint pendingFeeDelta = to_mathint(postUpdatePendingFee) - to_mathint(pendingFeeAfter);
+    mathint sellerCreditDecrease = to_mathint(sellerPostUpdateCredit) - to_mathint(creditOf(id, seller));
+    mathint sellerPendingFeeDecrease = to_mathint(sellerPostUpdatePendingFee) - to_mathint(pendingFee(id, seller));
 
-    assert postUpdateCredit == 0 || pendingFeeDelta == (to_mathint(postUpdatePendingFee) * creditDelta + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit);
+    assert buyerPendingFeeIncrease == (buyerCreditIncrease * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+    assert sellerPostUpdateCredit == 0 || sellerPendingFeeDecrease == (to_mathint(sellerPostUpdatePendingFee) * sellerCreditDecrease + to_mathint(sellerPostUpdateCredit) - 1) / to_mathint(sellerPostUpdateCredit);
 }
 
 // take() increases continuousFeeCredit by exactly the accrued fees of the buyer and seller.

From a2d1824612b580be0f0100899c9e1eef92491aa4 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Wed, 15 Apr 2026 10:10:36 +0200
Subject: [PATCH 14/27] clean up

---
 certora/confs/ContinuousFeeProtection.conf | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/certora/confs/ContinuousFeeProtection.conf b/certora/confs/ContinuousFeeProtection.conf
index 4071e3e0a..ba38c9ec5 100644
--- a/certora/confs/ContinuousFeeProtection.conf
+++ b/certora/confs/ContinuousFeeProtection.conf
@@ -10,15 +10,12 @@
   "solc_via_ir": true,
   "optimistic_loop": true,
   "loop_iter": 2,
-  "rule_sanity": "basic",
   "smt_timeout": 7200,
   "prover_args": [
     "-depth 5",
     "-timeout 3600",
-    "-splitParallel",
-    "true",
-    "-dontStopAtFirstSplitTimeout",
-    "true"
+    "-splitParallel true",
+    "-dontStopAtFirstSplitTimeout true"
   ],
-  "msg": "Midnight Continuous Fee Protection"
+  "msg": "Midnight Continuous Fee"
 }

From bf295f7e1f174b9f5e5ef331c25b19af4f9a9359 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Wed, 15 Apr 2026 15:45:12 +0200
Subject: [PATCH 15/27] improved pendingFeeDecreasesProportionallyForSeller

---
 certora/confs/ContinuousFeeProtection.conf |  1 -
 certora/specs/ContinuousFeeProtection.spec | 72 ++++++++++++----------
 2 files changed, 40 insertions(+), 33 deletions(-)

diff --git a/certora/confs/ContinuousFeeProtection.conf b/certora/confs/ContinuousFeeProtection.conf
index ba38c9ec5..18393e95d 100644
--- a/certora/confs/ContinuousFeeProtection.conf
+++ b/certora/confs/ContinuousFeeProtection.conf
@@ -10,7 +10,6 @@
   "solc_via_ir": true,
   "optimistic_loop": true,
   "loop_iter": 2,
-  "smt_timeout": 7200,
   "prover_args": [
     "-depth 5",
     "-timeout 3600",
diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index d4b93242f..e18f0e934 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -7,25 +7,17 @@ methods {
     function pendingFee(bytes32 id, address user) external returns (uint128) envfree;
     function continuousFee(bytes32 id) external returns (uint32) envfree;
     function continuousFeeCredit(bytes32 id) external returns (uint256) envfree;
-    function userLossIndex(bytes32 id, address user) external returns (uint128) envfree;
-    function lossIndex(bytes32 id) external returns (uint128) envfree;
-    function lastAccrual(bytes32 id, address user) external returns (uint128) envfree;
 
-    function _.price() external => NONDET;
-    function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET;
+    // Summarize internals irrelevant to continuous fee tracking.
     function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET;
     function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET;
-    function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET;
-    function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
-    function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
     function isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET;
-    function _.canIncreaseCredit(address) external => NONDET;
-    function _.canIncreaseDebt(address) external => NONDET;
     function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
     function tradingFee(bytes32 id, uint256 timeToMaturity) internal returns (uint256) => NONDET;
 
-    // the properties are about pendingFee/ credit accounting, and not liquidation interactions.
+    // summaries over-approximating the behavior of transient storage.
     function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET;
+    function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET;
 }
 
 /// HELPERS ///
@@ -43,23 +35,15 @@ function CVL_toId(Midnight.Obligation obligation, uint256 chainId, address midni
 
 definition WAD() returns uint256 = 10 ^ 18;
 
-// take() updates buyer and seller pending fees according to their post-update credit changes:
-// 1. the buyer's pendingFee increases by floor(creditIncrease * continuousFee * timeToMaturity / WAD).
-// 2. the seller's pendingFee decreases by exactly ceil(postUpdatePendingFee * creditDecrease / postUpdateCredit).
-rule pendingFeeAdjustedForBuyerAndSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
+// The buyer's pendingFee increases by floor(creditIncrease * continuousFee * timeToMaturity / WAD).
+rule continuousFeeNotOverchargedForBuyer(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
     address buyer = offer.buy ? offer.maker : taker;
-    address seller = offer.buy ? taker : offer.maker;
 
     bytes32 id;
-    uint128 buyerPostUpdateCredit;
-    uint128 buyerPostUpdatePendingFee;
-    uint128 sellerPostUpdateCredit;
-    uint128 sellerPostUpdatePendingFee;
-
-    buyerPostUpdateCredit, buyerPostUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, buyer);
-    sellerPostUpdateCredit, sellerPostUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, seller);
+    uint128 postUpdateCredit;
+    uint128 postUpdatePendingFee;
 
-    require sellerPostUpdateCredit > 0 || sellerPostUpdatePendingFee == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec";
+    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, buyer);
 
     take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof);
 
@@ -68,17 +52,42 @@ rule pendingFeeAdjustedForBuyerAndSeller(env e, uint256 units, address taker, ad
     uint256 contFee = continuousFee(id);
     uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
 
-    mathint buyerCreditIncrease = to_mathint(creditOf(id, buyer)) - to_mathint(buyerPostUpdateCredit);
-    mathint buyerPendingFeeIncrease = to_mathint(pendingFee(id, buyer)) - to_mathint(buyerPostUpdatePendingFee);
+    mathint creditDelta = to_mathint(creditOf(id, buyer)) - to_mathint(postUpdateCredit);
+    mathint pendingFeeDelta = to_mathint(pendingFee(id, buyer)) - to_mathint(postUpdatePendingFee);
+
+    assert pendingFeeDelta == (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+}
+
+// When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(PendingFee * creditDelta / postUpdateCredit).
+rule pendingFeeDecreasesProportionallyForSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
+    address seller = offer.buy ? taker : offer.maker;
+
+    bytes32 id;
+    uint128 postUpdateCredit;
+    uint128 postUpdatePendingFee;
+
+    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, offer.obligation, id, seller);
+
+    require postUpdateCredit > 0 || postUpdatePendingFee == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec";
+
+    take(e, units, taker, takerCallback, takerCallbackData, receiver, offer, ratifierData, root, proof);
+
+    require id == lastId, "id should be derived from obligation";
+
+    uint256 creditAfter = creditOf(id, seller);
+    uint256 pendingFeeAfter = pendingFee(id, seller);
+
+    require creditAfter > 0 || pendingFeeAfter == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec";
 
-    mathint sellerCreditDecrease = to_mathint(sellerPostUpdateCredit) - to_mathint(creditOf(id, seller));
-    mathint sellerPendingFeeDecrease = to_mathint(sellerPostUpdatePendingFee) - to_mathint(pendingFee(id, seller));
+    mathint creditDelta = to_mathint(postUpdateCredit) - to_mathint(creditAfter);
+    mathint pendingFeeDelta = to_mathint(postUpdatePendingFee) - to_mathint(pendingFeeAfter);
 
-    assert buyerPendingFeeIncrease == (buyerCreditIncrease * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
-    assert sellerPostUpdateCredit == 0 || sellerPendingFeeDecrease == (to_mathint(sellerPostUpdatePendingFee) * sellerCreditDecrease + to_mathint(sellerPostUpdateCredit) - 1) / to_mathint(sellerPostUpdateCredit);
+    // When postUpdateCredit == 0: noRemainingContinuousFeeWithoutCredit gives postUpdatePendingFee == 0; credit is non-increasing for a seller, therefore creditAfter == 0;
+    // noRemainingContinuousFeeWithoutCredit gives pendingFeeAfter == 0; hence pendingFeeDelta == 0.
+    assert postUpdateCredit == 0 ? pendingFeeDelta == 0 : pendingFeeDelta == (to_mathint(postUpdatePendingFee) * creditDelta + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit);
 }
 
-// take() increases continuousFeeCredit by exactly the accrued fees of the buyer and seller.
+// take() increases continuousFeeCredit by exactly the sum of the accrued fees of the buyer and seller.
 rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
     address buyer = offer.buy ? offer.maker : taker;
     address seller = offer.buy ? taker : offer.maker;
@@ -99,7 +108,6 @@ rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address tak
     assert continuousFeeCredit(id) == continuousFeeCreditBefore + buyerAccruedFee + sellerAccruedFee;
 }
 
-// updatePositionView()
 rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof, address user) {
     address buyer = offer.buy ? offer.maker : taker;
     address seller = offer.buy ? taker : offer.maker;

From f909e1e9b231201799146535854a198915158571 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Wed, 15 Apr 2026 15:55:32 +0200
Subject: [PATCH 16/27] added comment: takeDoesNotAffectThirdParties

---
 certora/specs/ContinuousFeeProtection.spec | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFeeProtection.spec
index e18f0e934..7bd9ab7f1 100644
--- a/certora/specs/ContinuousFeeProtection.spec
+++ b/certora/specs/ContinuousFeeProtection.spec
@@ -108,6 +108,7 @@ rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address tak
     assert continuousFeeCredit(id) == continuousFeeCreditBefore + buyerAccruedFee + sellerAccruedFee;
 }
 
+// take should not change the return values of updatePositionView (i.e., post-update credit, pending fee, and accrued fee) of a third party.
 rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof, address user) {
     address buyer = offer.buy ? offer.maker : taker;
     address seller = offer.buy ? taker : offer.maker;
@@ -129,7 +130,7 @@ rule takeDoesNotAffectThirdParties(env e, uint256 units, address taker, address
     uint256 userAccruedFeeAfter;
     postUpdateCreditAfter, postUpdatePendingFeeAfter, userAccruedFeeAfter = updatePositionView(e, offer.obligation, id, user);
 
-    assert postUpdateCreditBefore == postUpdateCreditAfter, "take should not change credit of third party";
-    assert postUpdatePendingFeeBefore == postUpdatePendingFeeAfter, "take should not change pending fee of third party";
-    assert userAccruedFeeBefore == userAccruedFeeAfter, "take should not change accrued fee of third party";
+    assert postUpdateCreditBefore == postUpdateCreditAfter;
+    assert postUpdatePendingFeeBefore == postUpdatePendingFeeAfter;
+    assert userAccruedFeeBefore == userAccruedFeeAfter;
 }

From 3cb941ceb5d8aa8e4e0c8039896f5f1b66a1223e Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Wed, 15 Apr 2026 16:29:54 +0200
Subject: [PATCH 17/27] renamed spec and conf to ContinuousFee

---
 .../confs/{ContinuousFeeProtection.conf => ContinuousFee.conf}    | 0
 .../specs/{ContinuousFeeProtection.spec => ContinuousFee.spec}    | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 rename certora/confs/{ContinuousFeeProtection.conf => ContinuousFee.conf} (100%)
 rename certora/specs/{ContinuousFeeProtection.spec => ContinuousFee.spec} (100%)

diff --git a/certora/confs/ContinuousFeeProtection.conf b/certora/confs/ContinuousFee.conf
similarity index 100%
rename from certora/confs/ContinuousFeeProtection.conf
rename to certora/confs/ContinuousFee.conf
diff --git a/certora/specs/ContinuousFeeProtection.spec b/certora/specs/ContinuousFee.spec
similarity index 100%
rename from certora/specs/ContinuousFeeProtection.spec
rename to certora/specs/ContinuousFee.spec

From 72db0a9fbb6412fdec40616d67d13f832c6ee765 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Wed, 15 Apr 2026 19:49:51 +0200
Subject: [PATCH 18/27] added comment and fixed Filename error in conf

---
 certora/confs/ContinuousFee.conf | 2 +-
 certora/specs/ContinuousFee.spec | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/certora/confs/ContinuousFee.conf b/certora/confs/ContinuousFee.conf
index 18393e95d..d5e45aa86 100644
--- a/certora/confs/ContinuousFee.conf
+++ b/certora/confs/ContinuousFee.conf
@@ -2,7 +2,7 @@
   "files": [
     "src/Midnight.sol"
   ],
-  "verify": "Midnight:certora/specs/ContinuousFeeProtection.spec",
+  "verify": "Midnight:certora/specs/ContinuousFee.spec",
   "solc": "solc-0.8.34",
   "solc_evm_version": "osaka",
   "optimistic_hashing": true,
diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index 7bd9ab7f1..b090443ff 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -9,8 +9,10 @@ methods {
     function continuousFeeCredit(bytes32 id) external returns (uint256) envfree;
 
     // Summarize internals irrelevant to continuous fee tracking.
-    function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET;
     function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET;
+
+    // Over-approximate view functions by summarising to NONDET.
+    function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET;
     function isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET;
     function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
     function tradingFee(bytes32 id, uint256 timeToMaturity) internal returns (uint256) => NONDET;
@@ -18,6 +20,8 @@ methods {
     // summaries over-approximating the behavior of transient storage.
     function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET;
     function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET;
+
+    // The callbacks are summarised as HAVOC_ECF by default. Hence, this spec assumes no reentrancy: callbacks and token transfers do not re-enter Midnight.
 }
 
 /// HELPERS ///

From 70c8b1c278aa6f7fd75aeb4cb6334d9c38552406 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Wed, 15 Apr 2026 22:15:23 +0200
Subject: [PATCH 19/27] reverted back to <= in
 continuousFeeNotOverchargedForBuyer

---
 certora/specs/ContinuousFee.spec | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index b090443ff..70dc9eed0 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -21,7 +21,8 @@ methods {
     function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET;
     function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET;
 
-    // The callbacks are summarised as HAVOC_ECF by default. Hence, this spec assumes no reentrancy: callbacks and token transfers do not re-enter Midnight.
+    // This spec assumes no reentrancy: callbacks and token transfers do not re-enter Midnight.
+    // Callbacks are summarised as HAVOC_ECF by default.
 }
 
 /// HELPERS ///
@@ -59,7 +60,7 @@ rule continuousFeeNotOverchargedForBuyer(env e, uint256 units, address taker, ad
     mathint creditDelta = to_mathint(creditOf(id, buyer)) - to_mathint(postUpdateCredit);
     mathint pendingFeeDelta = to_mathint(pendingFee(id, buyer)) - to_mathint(postUpdatePendingFee);
 
-    assert pendingFeeDelta == (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+    assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
 }
 
 // When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(PendingFee * creditDelta / postUpdateCredit).

From 5ee934bfd5158c9ada85dffe99d41f8a1ae49d14 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Mon, 20 Apr 2026 10:47:58 +0200
Subject: [PATCH 20/27] added back the NONDET summaries for callbacks

---
 certora/specs/ContinuousFee.spec | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index 70dc9eed0..368849d22 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -22,7 +22,9 @@ methods {
     function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET;
 
     // This spec assumes no reentrancy: callbacks and token transfers do not re-enter Midnight.
-    // Callbacks are summarised as HAVOC_ECF by default.
+    function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
+    function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
+    function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET;
 }
 
 /// HELPERS ///
@@ -60,7 +62,7 @@ rule continuousFeeNotOverchargedForBuyer(env e, uint256 units, address taker, ad
     mathint creditDelta = to_mathint(creditOf(id, buyer)) - to_mathint(postUpdateCredit);
     mathint pendingFeeDelta = to_mathint(pendingFee(id, buyer)) - to_mathint(postUpdatePendingFee);
 
-    assert pendingFeeDelta <= (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+    assert pendingFeeDelta == (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
 }
 
 // When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(PendingFee * creditDelta / postUpdateCredit).

From 4288c79d3e29b106c7ae9d1b865f748a719daf2a Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Mon, 20 Apr 2026 18:06:43 +0200
Subject: [PATCH 21/27] attempt at random seeds to resolve CI timeout issues

---
 certora/confs/ContinuousFee.conf | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/certora/confs/ContinuousFee.conf b/certora/confs/ContinuousFee.conf
index d5e45aa86..55a0c3e53 100644
--- a/certora/confs/ContinuousFee.conf
+++ b/certora/confs/ContinuousFee.conf
@@ -13,8 +13,11 @@
   "prover_args": [
     "-depth 5",
     "-timeout 3600",
-    "-splitParallel true",
-    "-dontStopAtFirstSplitTimeout true"
+    "-splitParallel",
+    "true",
+    "-dontStopAtFirstSplitTimeout",
+    "true",
+    "-s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
   ],
   "msg": "Midnight Continuous Fee"
 }

From 8430a09ca13cb13abef353e7742b8e0701d75f82 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Mon, 20 Apr 2026 18:41:54 +0200
Subject: [PATCH 22/27] tuned comment

---
 certora/specs/ContinuousFee.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index 368849d22..68c11975f 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -21,7 +21,7 @@ methods {
     function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET;
     function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET;
 
-    // This spec assumes no reentrancy: callbacks and token transfers do not re-enter Midnight.
+    // This spec assumes no reentrancy: callbacks do not re-enter Midnight.
     function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
     function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
     function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET;

From 6925b5b6843f00f0985b2e0e11faaf25e8be75a4 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Thu, 23 Apr 2026 23:17:01 +0200
Subject: [PATCH 23/27] removed callback summaries

---
 certora/specs/ContinuousFee.spec | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index 68c11975f..d41cdbd14 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -21,10 +21,7 @@ methods {
     function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET;
     function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET;
 
-    // This spec assumes no reentrancy: callbacks do not re-enter Midnight.
-    function _.onBuy(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
-    function _.onSell(bytes32, Midnight.Obligation, address, uint256, uint256, bytes) external => NONDET;
-    function _.onRatify(Midnight.Offer, bytes32, bytes) external => NONDET;
+    // This spec assumes no reentrancy: callbacks and token transfers are assumed to not re-enter Midnight, since they are summarised as HAVOC_ECF by default.
 }
 
 /// HELPERS ///

From d461b448854a82c03565e5fe64ac21edc76493d9 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Tue, 28 Apr 2026 14:55:23 +0200
Subject: [PATCH 24/27] added pendingFeeDecreasesProportionallyOnWithdraw

---
 certora/specs/ContinuousFee.spec | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index d41cdbd14..643efebcb 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -59,7 +59,8 @@ rule continuousFeeNotOverchargedForBuyer(env e, uint256 units, address taker, ad
     mathint creditDelta = to_mathint(creditOf(id, buyer)) - to_mathint(postUpdateCredit);
     mathint pendingFeeDelta = to_mathint(pendingFee(id, buyer)) - to_mathint(postUpdatePendingFee);
 
-    assert pendingFeeDelta == (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+    //assert pendingFeeDelta == (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+    assert pendingFee(id, buyer) <= postUpdatePendingFee + (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
 }
 
 // When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(PendingFee * creditDelta / postUpdateCredit).
@@ -91,6 +92,23 @@ rule pendingFeeDecreasesProportionallyForSeller(env e, uint256 units, address ta
     assert postUpdateCredit == 0 ? pendingFeeDelta == 0 : pendingFeeDelta == (to_mathint(postUpdatePendingFee) * creditDelta + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit);
 }
 
+// When credit decreases via withdraw, pendingFee decreases by ceil(pendingFee * units / postUpdateCredit).
+rule pendingFeeDecreasesProportionallyOnWithdraw(env e, Midnight.Obligation obligation, uint256 units, address onBehalf, address receiver) {
+    bytes32 id;
+    uint128 postUpdateCredit;
+    uint128 postUpdatePendingFee;
+
+    postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, obligation, id, onBehalf);
+
+    withdraw(e, obligation, units, onBehalf, receiver);
+
+    require id == lastId, "id should be derived from obligation";
+
+    mathint pendingFeeDelta = to_mathint(postUpdatePendingFee) - to_mathint(pendingFee(id, onBehalf));
+
+    assert postUpdateCredit > 0 => pendingFeeDelta == (to_mathint(postUpdatePendingFee) * to_mathint(units) + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit);
+}
+
 // take() increases continuousFeeCredit by exactly the sum of the accrued fees of the buyer and seller.
 rule continuousFeeCreditIncreasesByAccruedFees(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
     address buyer = offer.buy ? offer.maker : taker;

From 7ec8ec2c2c3e548a324634dd1426afa9552d7cad Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Tue, 28 Apr 2026 17:49:55 +0200
Subject: [PATCH 25/27] removed to_mathint; covered postUpdateCredit==0 case in
 pendingFeeDecreasesProportionallyOnWithdraw

---
 certora/specs/ContinuousFee.spec | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index 643efebcb..447090273 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -56,11 +56,9 @@ rule continuousFeeNotOverchargedForBuyer(env e, uint256 units, address taker, ad
     uint256 contFee = continuousFee(id);
     uint256 timeToMaturity = e.block.timestamp <= offer.obligation.maturity ? assert_uint256(offer.obligation.maturity - e.block.timestamp) : 0;
 
-    mathint creditDelta = to_mathint(creditOf(id, buyer)) - to_mathint(postUpdateCredit);
-    mathint pendingFeeDelta = to_mathint(pendingFee(id, buyer)) - to_mathint(postUpdatePendingFee);
+    mathint creditDelta = creditOf(id, buyer) - postUpdateCredit;
 
-    //assert pendingFeeDelta == (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
-    assert pendingFee(id, buyer) <= postUpdatePendingFee + (creditDelta * to_mathint(contFee) * to_mathint(timeToMaturity)) / WAD();
+    assert pendingFee(id, buyer) == postUpdatePendingFee + (creditDelta * contFee * timeToMaturity) / WAD();
 }
 
 // When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(PendingFee * creditDelta / postUpdateCredit).
@@ -84,12 +82,11 @@ rule pendingFeeDecreasesProportionallyForSeller(env e, uint256 units, address ta
 
     require creditAfter > 0 || pendingFeeAfter == 0, "See noRemainingContinuousFeeWithoutCredit in Midnight.spec";
 
-    mathint creditDelta = to_mathint(postUpdateCredit) - to_mathint(creditAfter);
-    mathint pendingFeeDelta = to_mathint(postUpdatePendingFee) - to_mathint(pendingFeeAfter);
+    mathint creditDelta = postUpdateCredit - creditAfter;
 
     // When postUpdateCredit == 0: noRemainingContinuousFeeWithoutCredit gives postUpdatePendingFee == 0; credit is non-increasing for a seller, therefore creditAfter == 0;
     // noRemainingContinuousFeeWithoutCredit gives pendingFeeAfter == 0; hence pendingFeeDelta == 0.
-    assert postUpdateCredit == 0 ? pendingFeeDelta == 0 : pendingFeeDelta == (to_mathint(postUpdatePendingFee) * creditDelta + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit);
+    assert postUpdateCredit == 0 ? postUpdatePendingFee == pendingFeeAfter : postUpdatePendingFee == pendingFeeAfter + (postUpdatePendingFee * creditDelta + postUpdateCredit - 1) / postUpdateCredit;
 }
 
 // When credit decreases via withdraw, pendingFee decreases by ceil(pendingFee * units / postUpdateCredit).
@@ -104,9 +101,8 @@ rule pendingFeeDecreasesProportionallyOnWithdraw(env e, Midnight.Obligation obli
 
     require id == lastId, "id should be derived from obligation";
 
-    mathint pendingFeeDelta = to_mathint(postUpdatePendingFee) - to_mathint(pendingFee(id, onBehalf));
-
-    assert postUpdateCredit > 0 => pendingFeeDelta == (to_mathint(postUpdatePendingFee) * to_mathint(units) + to_mathint(postUpdateCredit) - 1) / to_mathint(postUpdateCredit);
+    // When postUpdateCredit == 0, pendingFee(id, onBehalf) is unchanged on withdraw.
+    assert postUpdateCredit == 0 ? pendingFee(id, onBehalf) == postUpdatePendingFee : pendingFee(id, onBehalf) == postUpdatePendingFee - (postUpdatePendingFee * units + postUpdateCredit - 1) / postUpdateCredit;
 }
 
 // take() increases continuousFeeCredit by exactly the sum of the accrued fees of the buyer and seller.

From 5c3a01627a37b0770c4772b8a6bd27fd5d8c26aa Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Wed, 29 Apr 2026 08:21:06 +0200
Subject: [PATCH 26/27] tuned comment

---
 certora/specs/ContinuousFee.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index 447090273..a284b76c9 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -61,7 +61,7 @@ rule continuousFeeNotOverchargedForBuyer(env e, uint256 units, address taker, ad
     assert pendingFee(id, buyer) == postUpdatePendingFee + (creditDelta * contFee * timeToMaturity) / WAD();
 }
 
-// When a seller's credit decreases via a take, their pendingFee decreases by exactly ceil(PendingFee * creditDelta / postUpdateCredit).
+// When a seller's credit decreases via a take, their pendingFee decreases by ceil(PendingFee * creditDelta / postUpdateCredit).
 rule pendingFeeDecreasesProportionallyForSeller(env e, uint256 units, address taker, address takerCallback, bytes takerCallbackData, address receiver, Midnight.Offer offer, bytes ratifierData, bytes32 root, bytes32[] proof) {
     address seller = offer.buy ? taker : offer.maker;
 

From 851c270b4f393e4ba52eafba3dc014fdfffbd0f3 Mon Sep 17 00:00:00 2001
From: Bhargav <bhargav@morpho.xyz>
Date: Wed, 29 Apr 2026 23:01:56 +0200
Subject: [PATCH 27/27] added summary for hashOffer

---
 certora/specs/ContinuousFee.spec | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index a284b76c9..6c2891a6c 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -1,6 +1,8 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
 methods {
+    function multicall(bytes[]) external => HAVOC_ALL DELETE;
+
     function IdLib.toId(Midnight.Obligation memory obligation, uint256 chainId, address midnight) internal returns (bytes32) => CVL_toId(obligation, chainId, midnight);
 
     function creditOf(bytes32 id, address user) external returns (uint256) envfree;
@@ -10,18 +12,16 @@ methods {
 
     // Summarize internals irrelevant to continuous fee tracking.
     function IdLib.storeInCode(Midnight.Obligation memory) internal returns (address) => NONDET;
-
-    // Over-approximate view functions by summarising to NONDET.
+    function UtilsLib.hashOffer(Midnight.Offer memory) internal returns (bytes32) => NONDET;
+    function UtilsLib.msb(uint128) internal returns (uint256) => NONDET;
     function UtilsLib.isLeaf(bytes32, bytes32, bytes32[] memory) internal returns (bool) => NONDET;
-    function isHealthy(Midnight.Obligation memory, bytes32, address) internal returns (bool) => NONDET;
     function TickLib.tickToPrice(uint256 tick) internal returns (uint256) => NONDET;
-    function tradingFee(bytes32 id, uint256 timeToMaturity) internal returns (uint256) => NONDET;
 
     // summaries over-approximating the behavior of transient storage.
     function UtilsLib.tExchange(uint256, bytes32, address, bool) internal returns (bool) => NONDET;
     function UtilsLib.tGet(uint256, bytes32, address) internal returns (bool) => NONDET;
 
-    // This spec assumes no reentrancy: callbacks and token transfers are assumed to not re-enter Midnight, since they are summarised as HAVOC_ECF by default.
+    // Assume no reentrancy: callbacks and transfers do not re-enter Midnight.
 }
 
 /// HELPERS ///