diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index e4bcbbacf..47e091715 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -43,7 +43,7 @@ jobs:
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.19
 
       - name: Verify ${{ matrix.conf }}
         run: certoraRun certora/confs/${{ matrix.conf }}.conf
diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf
index 3ae9ec84b..b5adb6adc 100644
--- a/certora/confs/AccrueInterest.conf
+++ b/certora/confs/AccrueInterest.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
     "prover_args": [
         "-depth 3",
diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf
index e8a011349..b31cecfa3 100644
--- a/certora/confs/AssetsAccounting.conf
+++ b/certora/confs/AssetsAccounting.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec",
     "rule_sanity": "basic",
     "server": "production",
diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf
index 45c0c672f..e946d31df 100644
--- a/certora/confs/ConsistentState.conf
+++ b/certora/confs/ConsistentState.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
     "rule_sanity": "basic",
     "server": "production",
diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf
index 35d755e27..c7fd84c69 100644
--- a/certora/confs/ExactMath.conf
+++ b/certora/confs/ExactMath.conf
@@ -2,12 +2,14 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/ExactMath.spec",
     "rule_sanity": "basic",
     "prover_args": [
         "-depth 3",
         "-smt_hashingScheme plaininjectivity",
         "-mediumTimeout 30",
+        "-timeout 3600",
     ],
     "server": "production",
     "msg": "Morpho Blue Exact Math"
diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf
index 9238fde6b..0b4cf1895 100644
--- a/certora/confs/Health.conf
+++ b/certora/confs/Health.conf
@@ -3,6 +3,7 @@
         "certora/harness/MorphoHarness.sol",
         "src/mocks/OracleMock.sol"
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/Health.spec",
     "rule_sanity": "basic",
     "prover_args": [
diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf
index 6f944ed00..58d83ca43 100644
--- a/certora/confs/LibSummary.conf
+++ b/certora/confs/LibSummary.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/LibSummary.spec",
     "rule_sanity": "basic",
     "server": "production",
diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
index b3788c685..2dafcec5e 100644
--- a/certora/confs/Liveness.conf
+++ b/certora/confs/Liveness.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoInternalAccess.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",
     "rule_sanity": "basic",
     "server": "production",
diff --git a/certora/confs/RatioMath.conf b/certora/confs/RatioMath.conf
index a0ac6df8b..4cba64fbe 100644
--- a/certora/confs/RatioMath.conf
+++ b/certora/confs/RatioMath.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/RatioMath.spec",
     "rule_sanity": "basic",
     "prover_args": [
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
index db93b6a23..15c3577f2 100644
--- a/certora/confs/Reentrancy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/Reentrancy.spec",
     "rule_sanity": "basic",
     "prover_args": [
diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
index a31c697d4..7f8175a1a 100644
--- a/certora/confs/Reverts.conf
+++ b/certora/confs/Reverts.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/harness/MorphoHarness.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/Reverts.spec",
     "rule_sanity": "basic",
     "server": "production",
diff --git a/certora/confs/Transfer.conf b/certora/confs/Transfer.conf
index bedba566c..a02ea90f8 100644
--- a/certora/confs/Transfer.conf
+++ b/certora/confs/Transfer.conf
@@ -5,6 +5,7 @@
         "certora/dispatch/ERC20USDT.sol",
         "certora/dispatch/ERC20NoRevert.sol",
     ],
+    "solc": "solc-0.8.19",
     "verify": "TransferHarness:certora/specs/Transfer.spec",
     "rule_sanity": "basic",
     "server": "production",
diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
index d84995d8d..22a787a2f 100644
--- a/certora/specs/ConsistentState.spec
+++ b/certora/specs/ConsistentState.spec
@@ -46,24 +46,24 @@ persistent ghost mapping(address => mathint) idleAmount {
     init_state axiom (forall address token. idleAmount[token] == 0);
 }
 
-hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].supplyShares uint256 newShares (uint256 oldShares) STORAGE {
+hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].supplyShares uint256 newShares (uint256 oldShares) {
     sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares;
 }
 
-hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares uint128 newShares (uint128 oldShares) STORAGE {
+hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares uint128 newShares (uint128 oldShares) {
     sumBorrowShares[id] = sumBorrowShares[id] - oldShares + newShares;
 }
 
-hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE {
+hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) {
     sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
     idleAmount[toMarketParams(id).collateralToken] = idleAmount[toMarketParams(id).collateralToken] - oldAmount + newAmount;
 }
 
-hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) STORAGE {
+hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) {
     idleAmount[toMarketParams(id).loanToken] = idleAmount[toMarketParams(id).loanToken] - oldAmount + newAmount;
 }
 
-hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) STORAGE {
+hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) {
     idleAmount[toMarketParams(id).loanToken] = idleAmount[toMarketParams(id).loanToken] + oldAmount - newAmount;
 }
 
@@ -107,11 +107,7 @@ invariant hashOfMarketParamsOf(MorphoHarness.Id id)
 // This invariant is useful in the following rule, to link an id back to a market.
 invariant marketParamsOfHashOf(MorphoHarness.MarketParams marketParams)
     isCreated(libId(marketParams)) =>
-    toMarketParams(libId(marketParams)).loanToken == marketParams.loanToken &&
-    toMarketParams(libId(marketParams)).collateralToken == marketParams.collateralToken &&
-    toMarketParams(libId(marketParams)).oracle == marketParams.oracle &&
-    toMarketParams(libId(marketParams)).lltv == marketParams.lltv &&
-    toMarketParams(libId(marketParams)).irm == marketParams.irm;
+    toMarketParams(libId(marketParams)) == marketParams;
 
 // Check that the idle amount on the singleton is greater to the sum amount, that is the sum over all the markets of the total supply plus the total collateral minus the total borrow.
 invariant idleAmountLessThanBalance(address token)
@@ -167,11 +163,7 @@ rule libIdUnique() {
     // Assume that arguments are the same.
     require libId(marketParams1) == libId(marketParams2);
 
-    assert marketParams1.loanToken == marketParams2.loanToken;
-    assert marketParams1.collateralToken == marketParams2.collateralToken;
-    assert marketParams1.oracle == marketParams2.oracle;
-    assert marketParams1.irm == marketParams2.irm;
-    assert marketParams1.lltv == marketParams2.lltv;
+    assert marketParams1 == marketParams2;
 }
 
 // Check that only the user is able to change who is authorized to manage his position.
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 531db22f8..f2c6c204a 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -27,7 +27,7 @@ persistent ghost mapping(MorphoHarness.Id => mathint) sumCollateral
 {
     init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0);
 }
-hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE {
+hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) {
     sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
 }