diff --git a/certora/specs/ContinuousFee.spec b/certora/specs/ContinuousFee.spec
index 847f314d..e865878b 100644
--- a/certora/specs/ContinuousFee.spec
+++ b/certora/specs/ContinuousFee.spec
@@ -98,10 +98,13 @@ rule pendingFeeDecreasesProportionallyOnWithdraw(env e, Midnight.Market market,
 
     postUpdateCredit, postUpdatePendingFee, _ = updatePositionView(e, market, id, onBehalf);
 
-    withdraw(e, market, units, onBehalf, receiver);
+    uint128 returnedPendingFeeDecrease;
+    returnedPendingFeeDecrease = withdraw(e, market, units, onBehalf, receiver);
 
     require id == lastId, "id should be derived from market";
 
+    assert postUpdatePendingFee == pendingFee(id, onBehalf) + returnedPendingFeeDecrease;
+
     // 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;
 }
diff --git a/src/Midnight.sol b/src/Midnight.sol
index 2f6fc6e7..e571035b 100644
--- a/src/Midnight.sol
+++ b/src/Midnight.sol
@@ -503,7 +503,11 @@ contract Midnight is IMidnight {
         return (buyerAssets, sellerAssets);
     }
 
-    function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external {
+    /// @dev Returns the pending fee decrease.
+    function withdraw(Market memory market, uint256 units, address onBehalf, address receiver)
+        external
+        returns (uint128)
+    {
         require(onBehalf == msg.sender || isAuthorized[onBehalf][msg.sender], Unauthorized());
         bytes32 id = touchMarket(market);
         MarketState storage _marketState = marketState[id];
@@ -522,6 +526,7 @@ contract Midnight is IMidnight {
         emit EventsLib.Withdraw(msg.sender, id, units, onBehalf, receiver, pendingFeeDecrease);
 
         SafeTransferLib.safeTransfer(market.loanToken, receiver, units);
+        return pendingFeeDecrease;
     }
 
     function repay(Market memory market, uint256 units, address onBehalf, address callback, bytes calldata data)
diff --git a/src/interfaces/IMidnight.sol b/src/interfaces/IMidnight.sol
index 7d93054d..a7dee2a4 100644
--- a/src/interfaces/IMidnight.sol
+++ b/src/interfaces/IMidnight.sol
@@ -153,7 +153,7 @@ interface IMidnight {
 
     /// ENTRY-POINTS ///
     function take(Offer memory offer, bytes memory ratifierData, uint256 units, address taker, address receiverIfTakerIsSeller, address takerCallback, bytes memory takerCallbackData) external returns (uint256 buyerAssets, uint256 sellerAssets);
-    function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external;
+    function withdraw(Market memory market, uint256 units, address onBehalf, address receiver) external returns (uint128);
     function repay(Market memory market, uint256 units, address onBehalf, address callback, bytes memory data) external;
     function supplyCollateral(Market memory market, uint256 collateralIndex, uint256 assets, address onBehalf) external;
     function withdrawCollateral(Market memory market, uint256 collateralIndex, uint256 assets, address onBehalf, address receiver) external;