diff --git a/certora/confs/SupplyCap.conf b/certora/confs/SupplyCap.conf
index 2d4831a7..2dba5a04 100644
--- a/certora/confs/SupplyCap.conf
+++ b/certora/confs/SupplyCap.conf
@@ -3,6 +3,7 @@
         "lib/morpho-blue/certora/harness/MorphoHarness.sol",
         "certora/helpers/MetaMorphoHarness.sol",
         "certora/helpers/Util.sol",
+        "certora/dispatch/ERC20Standard.sol",
     ],
     "parametric_contracts": [
         "MetaMorphoHarness",
@@ -14,6 +15,7 @@
         "MorphoHarness": "solc-0.8.19",
         "MetaMorphoHarness": "solc-0.8.21",
         "Util": "solc-0.8.21",
+        "ERC20Standard": "solc-0.8.21",
     },
     "verify": "MetaMorphoHarness:certora/specs/SupplyCap.spec",
     "loop_iter": "2",
diff --git a/certora/specs/SupplyCap.spec b/certora/specs/SupplyCap.spec
index e29a20b1..e4d9ce29 100644
--- a/certora/specs/SupplyCap.spec
+++ b/certora/specs/SupplyCap.spec
@@ -15,7 +15,8 @@ methods {
     function Util.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree;
     function Util.toAssetsDown(uint256, uint256, uint256) external returns(uint256) envfree;
 
-    function _.balanceOf(address) external => NONDET;
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.transfer(address, uint256) external => DISPATCHER(true);
 }
 
 function supplyAssets(MetaMorphoHarness.Id id, address user) returns uint256 {