diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index e5b96af82..d47ff8f37 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -39,6 +39,10 @@ function summarySafeTransferFrom(address token, address from, address to, uint25
     }
 }
 
+function min(mathint a, mathint b) returns mathint {
+    return a < b ? a : b;
+}
+
 // Assume no fee.
 // Summarize the accrue interest to avoid having to deal with reverts with absurdly high borrow rates.
 function summaryAccrueInterest(env e, MorphoInternalAccess.MarketParams marketParams, MorphoInternalAccess.Id id) {
@@ -71,6 +75,7 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
 
     mathint sharesBefore = supplyShares(id, onBehalf);
     mathint balanceBefore = myBalances[marketParams.loanToken];
+    mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     uint256 suppliedAssets;
     uint256 suppliedShares;
@@ -78,11 +83,13 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
 
     mathint sharesAfter = supplyShares(id, onBehalf);
     mathint balanceAfter = myBalances[marketParams.loanToken];
+    mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     assert assets != 0 => suppliedAssets == assets;
     assert assets == 0 => suppliedShares == shares;
     assert sharesAfter == sharesBefore + suppliedShares;
     assert balanceAfter == balanceBefore + suppliedAssets;
+    assert liquidityAfter == liquidityBefore + suppliedAssets;
 }
 
 // Check that tokens and shares are properly accounted following a withdraw.
@@ -96,6 +103,7 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar
 
     mathint sharesBefore = supplyShares(id, onBehalf);
     mathint balanceBefore = myBalances[marketParams.loanToken];
+    mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     uint256 withdrawnAssets;
     uint256 withdrawnShares;
@@ -103,11 +111,13 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar
 
     mathint sharesAfter = supplyShares(id, onBehalf);
     mathint balanceAfter = myBalances[marketParams.loanToken];
+    mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     assert assets != 0 => withdrawnAssets == assets;
     assert assets == 0 => withdrawnShares == shares;
     assert sharesAfter == sharesBefore - withdrawnShares;
     assert balanceAfter == balanceBefore - withdrawnAssets;
+    assert liquidityAfter == liquidityBefore - withdrawnAssets;
 }
 
 // Check that tokens and shares are properly accounted following a borrow.
@@ -121,6 +131,7 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
 
     mathint sharesBefore = borrowShares(id, onBehalf);
     mathint balanceBefore = myBalances[marketParams.loanToken];
+    mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     uint256 borrowedAssets;
     uint256 borrowedShares;
@@ -128,11 +139,13 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
 
     mathint sharesAfter = borrowShares(id, onBehalf);
     mathint balanceAfter = myBalances[marketParams.loanToken];
+    mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     assert assets != 0 => borrowedAssets == assets;
     assert assets == 0 => borrowedShares == shares;
     assert sharesAfter == sharesBefore + borrowedShares;
     assert balanceAfter == balanceBefore - borrowedAssets;
+    assert liquidityAfter == liquidityBefore - borrowedAssets;
 }
 
 // Check that tokens and shares are properly accounted following a repay.
@@ -146,6 +159,9 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market
 
     mathint sharesBefore = borrowShares(id, onBehalf);
     mathint balanceBefore = myBalances[marketParams.loanToken];
+    mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id);
+
+    mathint borrowAssetsBefore = totalBorrowAssets(id);
 
     uint256 repaidAssets;
     uint256 repaidShares;
@@ -153,11 +169,14 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market
 
     mathint sharesAfter = borrowShares(id, onBehalf);
     mathint balanceAfter = myBalances[marketParams.loanToken];
+    mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id);
 
     assert assets != 0 => repaidAssets == assets;
     assert assets == 0 => repaidShares == shares;
     assert sharesAfter == sharesBefore - repaidShares;
     assert balanceAfter == balanceBefore + repaidAssets;
+    // Taking the min to handle the zeroFloorSub in the code.
+    assert liquidityAfter == liquidityBefore + min(repaidAssets, borrowAssetsBefore);
 }
 
 // Check that tokens and balances are properly accounted following a supplyCollateral.