diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf
index 4d064514..76b62919 100644
--- a/certora/confs/ConsistentState.conf
+++ b/certora/confs/ConsistentState.conf
@@ -1,17 +1,20 @@
 {
-    "files": [
-        "certora/helpers/MetaMorphoHarness.sol",
-        "certora/helpers/Util.sol",
-    ],
-    "solc": "solc-0.8.21",
-    "parametric_contracts": [
-        "MetaMorphoHarness",
-    ],
-    "verify": "MetaMorphoHarness:certora/specs/ConsistentState.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "smt_timeout": "600",
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Consistent State"
+  "files": [
+    "lib/morpho-blue/certora/harness/Util.sol",
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc_map": {
+    "Util": "solc-0.8.19",
+    "MetaMorphoHarness": "solc-0.8.21"
+  },
+  "parametric_contracts": [
+    "MetaMorphoHarness"
+  ],
+  "verify": "MetaMorphoHarness:certora/specs/ConsistentState.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "smt_timeout": "600",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Consistent State"
 }
diff --git a/certora/confs/DistinctIdentifiers.conf b/certora/confs/DistinctIdentifiers.conf
index 59de60bc..38fc7516 100644
--- a/certora/confs/DistinctIdentifiers.conf
+++ b/certora/confs/DistinctIdentifiers.conf
@@ -1,18 +1,18 @@
 {
-    "files": [
-        "certora/helpers/MetaMorphoHarness.sol",
-    ],
-    "solc": "solc-0.8.21",
-    "verify": "MetaMorphoHarness:certora/specs/DistinctIdentifiers.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-solvers [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:lia2]",
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 2000",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Distinct Identifiers"
+  "files": [
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.21",
+  "verify": "MetaMorphoHarness:certora/specs/DistinctIdentifiers.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-solvers [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:lia2]",
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 2000"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Distinct Identifiers"
 }
diff --git a/certora/confs/Enabled.conf b/certora/confs/Enabled.conf
index 703bacd5..2f69fd3a 100644
--- a/certora/confs/Enabled.conf
+++ b/certora/confs/Enabled.conf
@@ -1,20 +1,19 @@
 {
-    "files": [
-        "certora/helpers/MetaMorphoHarness.sol",
-    ],
-    "solc": "solc-0.8.21",
-    "verify": "MetaMorphoHarness:certora/specs/Enabled.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-solvers [z3:lia2,cvc5:nonlinNoDio,cvc4:nonlin,yices:def,z3:arith2]",
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 1000",
-        "-smt_easy_LIA true",
-    ],
-    "smt_timeout": "7000",
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Enabled"
+  "files": [
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.21",
+  "verify": "MetaMorphoHarness:certora/specs/Enabled.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-solvers [z3:lia2,cvc5:nonlinNoDio,cvc4:nonlin,yices:def,z3:arith2]",
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 1000"
+  ],
+  "smt_timeout": "7000",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Enabled"
 }
diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
index 2e3802f7..70c48632 100644
--- a/certora/confs/Immutability.conf
+++ b/certora/confs/Immutability.conf
@@ -1,17 +1,17 @@
 {
-    "files": [
-        "certora/helpers/MetaMorphoHarness.sol",
-    ],
-    "solc": "solc-0.8.21",
-    "verify": "MetaMorphoHarness:certora/specs/Immutability.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Immutability",
+  "files": [
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.21",
+  "verify": "MetaMorphoHarness:certora/specs/Immutability.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Immutability"
 }
diff --git a/certora/confs/LastUpdated.conf b/certora/confs/LastUpdated.conf
index 81bc168c..3f2a6d72 100644
--- a/certora/confs/LastUpdated.conf
+++ b/certora/confs/LastUpdated.conf
@@ -1,23 +1,25 @@
 {
-    "files": [
-        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
-        "certora/helpers/MetaMorphoHarness.sol",
-        "certora/helpers/Util.sol",
-    ],
-    "solc_map": {
-        "MorphoHarness": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
-        "Util": "solc-0.8.21",
-    },
-    "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 300",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Last Updated"
+  "files": [
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
+    "certora/helpers/MetaMorphoHarness.sol",
+    "certora/helpers/ERC20Helper.sol"
+  ],
+  "solc_map": {
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
+    "MetaMorphoHarness": "solc-0.8.21",
+    "ERC20Helper": "solc-0.8.21"
+  },
+  "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 300"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Last Updated"
 }
diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
index f391344c..3acab47b 100644
--- a/certora/confs/Liveness.conf
+++ b/certora/confs/Liveness.conf
@@ -1,25 +1,27 @@
 {
-    "files": [
-        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
-        "certora/helpers/MetaMorphoHarness.sol",
-        "certora/helpers/Util.sol",
-    ],
-    "link": [
-        "MetaMorphoHarness:MORPHO=MorphoHarness",
-    ],
-    "solc_map": {
-        "MorphoHarness": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
-        "Util": "solc-0.8.21",
-    },
-    "verify": "MetaMorphoHarness:certora/specs/Liveness.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-smt_easy_LIA true",
-    ],
-    "smt_timeout": "7000",
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Liveness"
+  "files": [
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
+    "certora/helpers/MetaMorphoHarness.sol",
+    "certora/helpers/ERC20Helper.sol"
+  ],
+  "link": [
+    "MetaMorphoHarness:MORPHO=MorphoHarness"
+  ],
+  "solc_map": {
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
+    "MetaMorphoHarness": "solc-0.8.21",
+    "ERC20Helper": "solc-0.8.21"
+  },
+  "verify": "MetaMorphoHarness:certora/specs/Liveness.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 0"
+  ],
+  "smt_timeout": "7000",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Liveness"
 }
diff --git a/certora/confs/MarketInteractions.conf b/certora/confs/MarketInteractions.conf
index f38dbb84..44e68878 100644
--- a/certora/confs/MarketInteractions.conf
+++ b/certora/confs/MarketInteractions.conf
@@ -1,22 +1,25 @@
 {
-    "files": [
-        "certora/helpers/MetaMorphoHarness.sol",
-        "certora/helpers/Util.sol",
-    ],
-    "solc": "solc-0.8.21",
-    "parametric_contracts": [
-        "MetaMorphoHarness",
-    ],
-    "verify": "MetaMorphoHarness:certora/specs/MarketInteractions.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-        "-smt_nonLinearArithmetic false",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Market Interactions"
+  "files": [
+    "lib/morpho-blue/certora/harness/Util.sol",
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc_map": {
+    "Util": "solc-0.8.19",
+    "MetaMorphoHarness": "solc-0.8.21"
+  },
+  "parametric_contracts": [
+    "MetaMorphoHarness"
+  ],
+  "verify": "MetaMorphoHarness:certora/specs/MarketInteractions.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120",
+    "-smt_nonLinearArithmetic false"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Market Interactions"
 }
diff --git a/certora/confs/PendingValues.conf b/certora/confs/PendingValues.conf
index 7db7a5e8..e608ff22 100644
--- a/certora/confs/PendingValues.conf
+++ b/certora/confs/PendingValues.conf
@@ -1,17 +1,17 @@
 {
-    "files": [
-        "certora/helpers/MetaMorphoHarness.sol",
-    ],
-    "solc": "solc-0.8.21",
-    "verify": "MetaMorphoHarness:certora/specs/PendingValues.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 3600",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Pending Values"
+  "files": [
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.21",
+  "verify": "MetaMorphoHarness:certora/specs/PendingValues.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 3600"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Pending Values"
 }
diff --git a/certora/confs/Range.conf b/certora/confs/Range.conf
index 13b869d3..045025a1 100644
--- a/certora/confs/Range.conf
+++ b/certora/confs/Range.conf
@@ -1,19 +1,19 @@
 {
-    "files": [
-        "certora/helpers/MetaMorphoHarness.sol",
-    ],
-    "solc": "solc-0.8.21",
-    "verify": "MetaMorphoHarness:certora/specs/Range.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 0",
-        "-timeout 300",
-        "-smt_nonLinearArithmetic true",
-        "-adaptiveSolverConfig false",
-        "-solvers [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}]",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Range"
+  "files": [
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.21",
+  "verify": "MetaMorphoHarness:certora/specs/Range.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 0",
+    "-timeout 300",
+    "-smt_nonLinearArithmetic true",
+    "-adaptiveSolverConfig false",
+    "-solvers [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}]"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Range"
 }
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
index 2c078aef..c9dd0692 100644
--- a/certora/confs/Reentrancy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -1,18 +1,18 @@
 {
-    "files": [
-        "certora/helpers/MetaMorphoHarness.sol",
-    ],
-    "solc": "solc-0.8.21",
-    "verify": "MetaMorphoHarness:certora/specs/Reentrancy.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-        "-enableStorageSplitting false",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Reentrancy",
+  "files": [
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.21",
+  "verify": "MetaMorphoHarness:certora/specs/Reentrancy.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120",
+    "-enableStorageSplitting false"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Reentrancy"
 }
diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index 0960539b..7d5fb42c 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -1,33 +1,35 @@
 {
-    "files": [
-        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
-        "certora/helpers/MetaMorphoHarness.sol",
-        "certora/helpers/Util.sol",
-        "certora/dispatch/ERC20Standard.sol",
-    ],
-    "link": [
-        "MetaMorphoHarness:MORPHO=MorphoHarness",
-    ],
-    "solc_map": {
-        "MorphoHarness": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
-        "Util": "solc-0.8.21",
-        "ERC20Standard": "solc-0.8.21",
-    },
-    "verify": "MetaMorphoHarness:certora/specs/Reverts.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 5",
-        "-mediumTimeout 40",
-        "-splitParallel true",
-        "-splitParallelInitialDepth 4",
-        "-splitParallelTimelimit 7000",
-        "-adaptiveSolverConfig false",
-        "-smt_nonLinearArithmetic true",
-        "-solvers [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}]"
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Reverts",
+  "files": [
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
+    "certora/helpers/MetaMorphoHarness.sol",
+    "certora/helpers/ERC20Helper.sol",
+    "certora/dispatch/ERC20Standard.sol"
+  ],
+  "link": [
+    "MetaMorphoHarness:MORPHO=MorphoHarness"
+  ],
+  "solc_map": {
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
+    "MetaMorphoHarness": "solc-0.8.21",
+    "ERC20Helper": "solc-0.8.21",
+    "ERC20Standard": "solc-0.8.21"
+  },
+  "verify": "MetaMorphoHarness:certora/specs/Reverts.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 5",
+    "-mediumTimeout 40",
+    "-splitParallel true",
+    "-splitParallelInitialDepth 4",
+    "-splitParallelTimelimit 7000",
+    "-adaptiveSolverConfig false",
+    "-smt_nonLinearArithmetic true",
+    "-solvers [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}]"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Reverts"
 }
diff --git a/certora/confs/Roles.conf b/certora/confs/Roles.conf
index 0db5cb2d..cc71f1da 100644
--- a/certora/confs/Roles.conf
+++ b/certora/confs/Roles.conf
@@ -1,18 +1,18 @@
 {
-    "files": [
-        "certora/helpers/MetaMorphoHarness.sol",
-    ],
-    "solc": "solc-0.8.21",
-    "verify": "MetaMorphoHarness:certora/specs/Roles.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
-        "-superOptimisticReturnsize true",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Roles",
+  "files": [
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.21",
+  "verify": "MetaMorphoHarness:certora/specs/Roles.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 120",
+    "-superOptimisticReturnsize true"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Roles"
 }
diff --git a/certora/confs/Timelock.conf b/certora/confs/Timelock.conf
index e80470a5..1829751d 100644
--- a/certora/confs/Timelock.conf
+++ b/certora/confs/Timelock.conf
@@ -1,24 +1,24 @@
 {
-    "files": [
-        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
-        "certora/helpers/MetaMorphoHarness.sol",
-    ],
-    "parametric_contracts": [
-        "MetaMorphoHarness",
-    ],
-    "solc_map": {
-        "MorphoHarness": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
-    },
-    "verify": "MetaMorphoHarness:certora/specs/Timelock.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 3600",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Timelock"
+  "files": [
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "parametric_contracts": [
+    "MetaMorphoHarness"
+  ],
+  "solc_map": {
+    "MorphoHarness": "solc-0.8.19",
+    "MetaMorphoHarness": "solc-0.8.21"
+  },
+  "verify": "MetaMorphoHarness:certora/specs/Timelock.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 3600"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Timelock"
 }
diff --git a/certora/confs/Tokens.conf b/certora/confs/Tokens.conf
index e533c66b..403d8d5b 100644
--- a/certora/confs/Tokens.conf
+++ b/certora/confs/Tokens.conf
@@ -1,36 +1,37 @@
 {
-    "files": [
-        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
-        "certora/helpers/MetaMorphoHarness.sol",
-        "certora/helpers/Util.sol",
-        "certora/dispatch/ERC20NoRevert.sol",
-        "certora/dispatch/ERC20Standard.sol",
-        "certora/dispatch/ERC20USDT.sol",
-    ],
-    "link": [
-        "MetaMorphoHarness:MORPHO=MorphoHarness",
-    ],
-    "solc_map": {
-        "MorphoHarness": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
-        "Util": "solc-0.8.21",
-        "ERC20NoRevert": "solc-0.8.21",
-        "ERC20Standard": "solc-0.8.21",
-        "ERC20USDT": "solc-0.8.21",
-    },
-    "verify": "MetaMorphoHarness:certora/specs/Tokens.spec",
-    "loop_iter": "2",
-    "optimistic_loop": true,
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 3600",
-        "-adaptiveSolverConfig false",
-        "-smt_nonLinearArithmetic false",
-        "-smt_hashingScheme plaininjectivity",
-        "-smt_easy_LIA true",
-    ],
-    "rule_sanity": "basic",
-    "server": "production",
-    "msg": "MetaMorpho Tokens",
+  "files": [
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
+    "certora/helpers/MetaMorphoHarness.sol",
+    "certora/helpers/ERC20Helper.sol",
+    "certora/dispatch/ERC20NoRevert.sol",
+    "certora/dispatch/ERC20Standard.sol",
+    "certora/dispatch/ERC20USDT.sol"
+  ],
+  "link": [
+    "MetaMorphoHarness:MORPHO=MorphoHarness"
+  ],
+  "solc_map": {
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
+    "MetaMorphoHarness": "solc-0.8.21",
+    "ERC20Helper": "solc-0.8.21",
+    "ERC20NoRevert": "solc-0.8.21",
+    "ERC20Standard": "solc-0.8.21",
+    "ERC20USDT": "solc-0.8.21"
+  },
+  "verify": "MetaMorphoHarness:certora/specs/Tokens.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 3",
+    "-mediumTimeout 20",
+    "-timeout 3600",
+    "-adaptiveSolverConfig false",
+    "-smt_nonLinearArithmetic false",
+    "-smt_hashingScheme plaininjectivity"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho Tokens"
 }
diff --git a/certora/helpers/ERC20Helper.sol b/certora/helpers/ERC20Helper.sol
new file mode 100644
index 00000000..e92a243c
--- /dev/null
+++ b/certora/helpers/ERC20Helper.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.21;
+
+import {IERC20, SafeERC20} from "../munged/MetaMorpho.sol";
+
+contract ERC20Helper {
+    using SafeERC20 for IERC20;
+
+    function balanceOf(address token, address user) external view returns (uint256) {
+        return IERC20(token).balanceOf(user);
+    }
+
+    function totalSupply(address token) external view returns (uint256) {
+        return IERC20(token).totalSupply();
+    }
+
+    function safeTransferFrom(address token, address from, address to, uint256 amount) external {
+        IERC20(token).safeTransferFrom(from, to, amount);
+    }
+}
diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol
deleted file mode 100644
index b38f9e03..00000000
--- a/certora/helpers/Util.sol
+++ /dev/null
@@ -1,48 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-pragma solidity 0.8.21;
-
-import {
-    MarketParams,
-    MarketParamsLib,
-    IERC20,
-    SafeERC20,
-    IMorphoHarness,
-    SharesMathLib,
-    Id,
-    Market
-} from "../munged/MetaMorpho.sol";
-
-contract Util {
-    using SafeERC20 for IERC20;
-    using SharesMathLib for uint256;
-    using MarketParamsLib for MarketParams;
-
-    function balanceOf(address token, address user) external view returns (uint256) {
-        return IERC20(token).balanceOf(user);
-    }
-
-    function totalSupply(address token) external view returns (uint256) {
-        return IERC20(token).totalSupply();
-    }
-
-    function safeTransferFrom(address token, address from, address to, uint256 amount) external {
-        IERC20(token).safeTransferFrom(from, to, amount);
-    }
-
-    function withdrawnAssets(IMorphoHarness morpho, Id id, uint256 assets, uint256 shares)
-        external
-        view
-        returns (uint256)
-    {
-        if (shares == 0) {
-            return assets;
-        } else {
-            Market memory market = morpho.market(id);
-            return shares.toAssetsDown(market.totalSupplyAssets, market.totalSupplyShares);
-        }
-    }
-
-    function libId(MarketParams memory marketParams) external pure returns (Id) {
-        return marketParams.id();
-    }
-}
diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
index fd2a7c15..0fb4d71a 100644
--- a/certora/specs/ConsistentState.spec
+++ b/certora/specs/ConsistentState.spec
@@ -5,10 +5,7 @@ using Util as Util;
 
 methods {
     function Util.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree;
-    function Util.balanceOf(address, address) external returns(uint256) envfree;
-    function Util.totalSupply(address) external returns(uint256) envfree;
-    function Util.safeTransferFrom(address, address, address, uint256) external envfree;
-    function Util.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree;
+    function Util.libMulDivDown(uint256, uint256, uint256) external returns(uint256) envfree;
 }
 
 // Check that the fee cannot accrue to an unset fee recipient.
diff --git a/certora/specs/LastUpdated.spec b/certora/specs/LastUpdated.spec
index 8e36b3b9..74a751e0 100644
--- a/certora/specs/LastUpdated.spec
+++ b/certora/specs/LastUpdated.spec
@@ -2,9 +2,16 @@
 import "ConsistentState.spec";
 
 using MorphoHarness as Morpho;
+using ERC20Helper as ERC20;
 
 methods {
+    function ERC20.balanceOf(address, address) external returns(uint256) envfree;
+    function ERC20.totalSupply(address) external returns(uint256) envfree;
+    function ERC20.safeTransferFrom(address, address, address, uint256) external envfree;
+
     function Morpho.lastUpdate(MorphoHarness.Id) external returns(uint256) envfree;
+    function Morpho.virtualTotalSupplyAssets(MorphoHarness.Id) external returns(uint256) envfree;
+    function Morpho.virtualTotalSupplyShares(MorphoHarness.Id) external returns(uint256) envfree;
 }
 
 function hasCuratorRole(address user) returns bool {
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index b8e66951..a95c1719 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -290,7 +290,7 @@ rule acceptCapInputValidation(env e, MetaMorphoHarness.MarketParams marketParams
 rule skimRevertCondition(env e, address token) {
     address skimRecipient = skimRecipient();
 
-    require skimRecipient != currentContract => Util.balanceOf(token, skimRecipient) + Util.balanceOf(token, currentContract) <= to_mathint(Util.totalSupply(token));
+    require skimRecipient != currentContract => ERC20.balanceOf(token, skimRecipient) + ERC20.balanceOf(token, currentContract) <= to_mathint(ERC20.totalSupply(token));
 
     skim@withrevert(e, token);
 
diff --git a/certora/specs/Tokens.spec b/certora/specs/Tokens.spec
index 0c4eca41..d67be838 100644
--- a/certora/specs/Tokens.spec
+++ b/certora/specs/Tokens.spec
@@ -35,7 +35,7 @@ function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 asse
     requireInvariant enabledHasConsistentAsset(marketParams);
 
     // Summarize supply as just a transfer for the purpose of this specification file, which is sound because only the properties about tokens are verified in this file.
-    Util.safeTransferFrom(marketParams.loanToken, currentContract, MORPHO(), assets);
+    ERC20.safeTransferFrom(marketParams.loanToken, currentContract, MORPHO(), assets);
 
     return (assets, shares);
 }
@@ -51,9 +51,16 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     requireInvariant enabledHasConsistentAsset(marketParams);
 
     // Use effective withdrawn assets if shares are given as input.
-    uint256 withdrawn = Util.withdrawnAssets(MORPHO(), id, assets, shares);
+    uint256 withdrawn;
+    if (shares == 0) {
+        require withdrawn == assets;
+    } else {
+        uint256 totalAssets = Morpho.virtualTotalSupplyAssets(id);
+        uint256 totalShares = Morpho.virtualTotalSupplyShares(id);
+        require withdrawn == Util.libMulDivDown(shares, totalAssets, totalShares);
+    }
     // Summarize withdraw as just a transfer for the purpose of this specification file, which is sound because only the properties about tokens are verified in this file.
-    Util.safeTransferFrom(marketParams.loanToken, MORPHO(), currentContract, withdrawn);
+    ERC20.safeTransferFrom(marketParams.loanToken, MORPHO(), currentContract, withdrawn);
 
     return (withdrawn, shares);
 }
@@ -69,13 +76,13 @@ rule depositTokenChange(env e, uint256 assets, address receiver) {
     require currentContract == 0x12;
     require e.msg.sender == 0x13;
 
-    uint256 balanceMorphoBefore = Util.balanceOf(asset, morpho);
-    uint256 balanceMetaMorphoBefore = Util.balanceOf(asset, currentContract);
-    uint256 balanceSenderBefore = Util.balanceOf(asset, e.msg.sender);
+    uint256 balanceMorphoBefore = ERC20.balanceOf(asset, morpho);
+    uint256 balanceMetaMorphoBefore = ERC20.balanceOf(asset, currentContract);
+    uint256 balanceSenderBefore = ERC20.balanceOf(asset, e.msg.sender);
     deposit(e, assets, receiver);
-    uint256 balanceMorphoAfter = Util.balanceOf(asset, morpho);
-    uint256 balanceMetaMorphoAfter = Util.balanceOf(asset, currentContract);
-    uint256 balanceSenderAfter = Util.balanceOf(asset, e.msg.sender);
+    uint256 balanceMorphoAfter = ERC20.balanceOf(asset, morpho);
+    uint256 balanceMetaMorphoAfter = ERC20.balanceOf(asset, currentContract);
+    uint256 balanceSenderAfter = ERC20.balanceOf(asset, e.msg.sender);
 
     assert assert_uint256(balanceMorphoAfter - balanceMorphoBefore) == assets;
     assert balanceMetaMorphoAfter == balanceMetaMorphoBefore;
@@ -93,13 +100,13 @@ rule withdrawTokenChange(env e, uint256 assets, address receiver, address owner)
     require currentContract == 0x12;
     require receiver == 0x13;
 
-    uint256 balanceMorphoBefore = Util.balanceOf(asset, morpho);
-    uint256 balanceMetaMorphoBefore = Util.balanceOf(asset, currentContract);
-    uint256 balanceReceiverBefore = Util.balanceOf(asset, receiver);
+    uint256 balanceMorphoBefore = ERC20.balanceOf(asset, morpho);
+    uint256 balanceMetaMorphoBefore = ERC20.balanceOf(asset, currentContract);
+    uint256 balanceReceiverBefore = ERC20.balanceOf(asset, receiver);
     withdraw(e, assets, receiver, owner);
-    uint256 balanceMorphoAfter = Util.balanceOf(asset, morpho);
-    uint256 balanceMetaMorphoAfter = Util.balanceOf(asset, currentContract);
-    uint256 balanceReceiverAfter = Util.balanceOf(asset, receiver);
+    uint256 balanceMorphoAfter = ERC20.balanceOf(asset, morpho);
+    uint256 balanceMetaMorphoAfter = ERC20.balanceOf(asset, currentContract);
+    uint256 balanceReceiverAfter = ERC20.balanceOf(asset, receiver);
 
     assert assert_uint256(balanceMorphoBefore - balanceMorphoAfter) == assets;
     assert balanceMetaMorphoAfter == balanceMetaMorphoBefore;
@@ -116,13 +123,13 @@ rule reallocateTokenChange(env e, MetaMorphoHarness.MarketAllocation[] allocatio
     require asset == 0x11;
     require currentContract == 0x12;
 
-    uint256 balanceMorphoBefore = Util.balanceOf(asset, morpho);
-    uint256 balanceMetaMorphoBefore = Util.balanceOf(asset, currentContract);
-    uint256 balanceSenderBefore = Util.balanceOf(asset, e.msg.sender);
+    uint256 balanceMorphoBefore = ERC20.balanceOf(asset, morpho);
+    uint256 balanceMetaMorphoBefore = ERC20.balanceOf(asset, currentContract);
+    uint256 balanceSenderBefore = ERC20.balanceOf(asset, e.msg.sender);
     reallocate(e, allocations);
-    uint256 balanceMorphoAfter = Util.balanceOf(asset, morpho);
-    uint256 balanceMetaMorphoAfter = Util.balanceOf(asset, currentContract);
-    uint256 balanceSenderAfter = Util.balanceOf(asset, e.msg.sender);
+    uint256 balanceMorphoAfter = ERC20.balanceOf(asset, morpho);
+    uint256 balanceMetaMorphoAfter = ERC20.balanceOf(asset, currentContract);
+    uint256 balanceSenderAfter = ERC20.balanceOf(asset, e.msg.sender);
 
     assert balanceMorphoAfter == balanceMorphoAfter;
     assert balanceMetaMorphoAfter == balanceMetaMorphoBefore;
diff --git a/lib/morpho-blue b/lib/morpho-blue
index 731e3f7e..3de2df4e 160000
--- a/lib/morpho-blue
+++ b/lib/morpho-blue
@@ -1 +1 @@
-Subproject commit 731e3f7ed97cf15f8fe00b86e4be5365eb3802ac
+Subproject commit 3de2df4eb94c3f6118963039d4f177839a228e2a