diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch
index 6b7d547fd..8b490be5c 100644
--- a/certora/applyMunging.patch
+++ b/certora/applyMunging.patch
@@ -1,14 +1,4 @@
-diff -ruN interfaces/IMorpho.sol interfaces/IMorpho.sol
---- interfaces/IMorpho.sol	2023-08-29 09:58:51.628147127 +0200
-+++ interfaces/IMorpho.sol	2023-08-29 10:15:36.946593577 +0200
-@@ -292,7 +292,4 @@
-     /// @param authorization The `Authorization` struct.
-     /// @param signature The signature.
-     function setAuthorizationWithSig(Authorization calldata authorization, Signature calldata signature) external;
--
--    /// @notice Returns the data stored on the different `slots`.
--    function extSloads(bytes32[] memory slots) external view returns (bytes32[] memory);
- }
+
 diff -ruN libraries/MarketParamsLib.sol libraries/MarketParamsLib.sol
 --- libraries/MarketParamsLib.sol	2023-08-29 09:59:37.937583556 +0200
 +++ libraries/MarketParamsLib.sol	2023-08-29 10:16:10.519752188 +0200
@@ -22,28 +12,3 @@ diff -ruN libraries/MarketParamsLib.sol libraries/MarketParamsLib.sol
 +        marketParamsId = Id.wrap(keccak256(abi.encode(marketParams)));
      }
  }
-diff -ruN Morpho.sol Morpho.sol
---- Morpho.sol	2023-08-29 09:58:43.158169812 +0200
-+++ Morpho.sol	2023-08-29 10:15:20.650012827 +0200
-@@ -502,21 +502,4 @@
- 
-         return maxBorrow >= borrowed;
-     }
--
--    /* STORAGE VIEW */
--
--    /// @inheritdoc IMorpho
--    function extSloads(bytes32[] calldata slots) external view returns (bytes32[] memory res) {
--        uint256 nSlots = slots.length;
--
--        res = new bytes32[](nSlots);
--
--        for (uint256 i; i < nSlots;) {
--            bytes32 slot = slots[i++];
--
--            assembly ("memory-safe") {
--                mstore(add(res, mul(i, 32)), sload(slot))
--            }
--        }
--    }
- }
diff --git a/certora/specs/Blue.spec b/certora/specs/Blue.spec
index 55a56b668..6655a094f 100644
--- a/certora/specs/Blue.spec
+++ b/certora/specs/Blue.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function getTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
     function getTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
diff --git a/certora/specs/BlueAccrueInterests.spec b/certora/specs/BlueAccrueInterests.spec
index 0ac324321..fb8aa5075 100644
--- a/certora/specs/BlueAccrueInterests.spec
+++ b/certora/specs/BlueAccrueInterests.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivDown(a,b,c);
     function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivUp(a,b,c);
     function MathLib.wTaylorCompounded(uint256 a, uint256 b) internal returns uint256 => ghostTaylorCompounded(a, b);
diff --git a/certora/specs/BlueExitLiquidity.spec b/certora/specs/BlueExitLiquidity.spec
index b8f1e6337..4d925c11b 100644
--- a/certora/specs/BlueExitLiquidity.spec
+++ b/certora/specs/BlueExitLiquidity.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getSupplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function getBorrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function getCollateral(MorphoHarness.Id, address) external returns uint256 envfree;
diff --git a/certora/specs/BlueLibSummary.spec b/certora/specs/BlueLibSummary.spec
index 9f41296a0..827304a37 100644
--- a/certora/specs/BlueLibSummary.spec
+++ b/certora/specs/BlueLibSummary.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
     function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
     function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
diff --git a/certora/specs/BlueLiveness.spec b/certora/specs/BlueLiveness.spec
index c3b631978..a2725210a 100644
--- a/certora/specs/BlueLiveness.spec
+++ b/certora/specs/BlueLiveness.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getTotalSupplyAssets(MorphoInternalAccess.Id) external returns uint256 envfree;
     function getTotalSupplyShares(MorphoInternalAccess.Id) external returns uint256 envfree;
     function getTotalBorrowAssets(MorphoInternalAccess.Id) external returns uint256 envfree;
diff --git a/certora/specs/BlueRatioMath.spec b/certora/specs/BlueRatioMath.spec
index 3c192c4c1..8281d7208 100644
--- a/certora/specs/BlueRatioMath.spec
+++ b/certora/specs/BlueRatioMath.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function getVirtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
diff --git a/certora/specs/BlueReverts.spec b/certora/specs/BlueReverts.spec
index 751c1c452..f501fe82f 100644
--- a/certora/specs/BlueReverts.spec
+++ b/certora/specs/BlueReverts.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function owner() external returns address envfree;
     function getTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function getTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
diff --git a/certora/specs/DifficultMath.spec b/certora/specs/DifficultMath.spec
index 382626c34..a7b18a52a 100644
--- a/certora/specs/DifficultMath.spec
+++ b/certora/specs/DifficultMath.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function getVirtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec
index 42bcb4db2..99403f8a6 100644
--- a/certora/specs/Health.spec
+++ b/certora/specs/Health.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getLastUpdate(MorphoHarness.Id) external returns uint256 envfree;
     function getTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
     function getBorrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
index 86ad76679..3f7bfdf1f 100644
--- a/certora/specs/Reentrancy.spec
+++ b/certora/specs/Reentrancy.spec
@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256;
 }