diff --git a/certora/README.md b/certora/README.md
new file mode 100644
index 000000000..48e987103
--- /dev/null
+++ b/certora/README.md
@@ -0,0 +1,61 @@
+This folder contains the verification of the Morpho Blue protocol using CVL, Certora's Verification Language.
+
+## High-Level Description
+
+The Morpho Blue protocol relies on several different concepts, which are described below.
+These concepts have been verified using CVL.
+See the description of the specification files below (or those files directly) for more details.
+
+The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens.\
+**Transfers.** Token transfers are verified to behave as expected for the most common implementations, in particular the transferred amount is the amount passed as input.\
+**Markets**. Markets on Morpho Blue depend on a pair of assets, the borrowable asset that is supplied and borrowed, and the collateral asset.
+Markets are independent, which means that loans cannot be impacted by loans from other markets.
+Positions of users are also independent, so loans cannot be impacted by loans from other users.
+The accounting of the markets has been verified (such as the total amounts), as well as the fact that only market with enabled parameters are created.\
+**Supply.** When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism.
+Shares increase in value as interest is accrued.\
+**Borrow.** To borrow on Morpho Blue, collateral must be deposited.
+Collateral tokens remain idle, as well as any borrowable token that has not been borrowed.\
+**Liquidation.** To ensure proper collateralization, a liquidation system is put in place.
+In the absence of accrued interest, for example when creating a new position or when interacting multiple times in the same block, a position cannot be made unhealthy.\
+**Authorization.** Morpho Blue also defines a sound authorization system where users cannot modify positions of other users without proper authorization (except when liquidating).\
+**Safety.** Other safety properties are verified, particularly regarding reentrancy attacks and about input validation and revert conditions.\
+**Liveness.** Other liveness properties are verified as well, in particular it is always possible to exit a position without concern for the oracle.
+
+## Folder and File Structure
+
+The [`certora/specs`](./specs) folder contains the following files:
+
+- [`AccrueInterest.spec`](./specs/AccrueInterest.spec) checks that the main functions accrue interest at the start of the interaction.
+  This is done by ensuring that accruing interest before calling the function does not change the outcome compared to just calling the function.
+  View functions do not necessarily respect this property (for example, `totalSupplyShares`), and are filtered out.
+- [`ConsistentState.spec`](./specs/ConsistentState.spec) checks that the state (storage) of the Morpho contract is consistent.
+  This includes checking that the accounting of the total amount and shares is correct, that markets are independent from each other, that only enabled IRMs and LLTVs can be used, and that users cannot have their position made worse by an unauthorized account.
+- [`ExactMath.spec`](./specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division.
+  Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start.
+- [`ExitLiquidity.spec`](./specs/ExitLiquidity.spec) checks that when exiting a position with withdraw, withdrawCollateral, or repay, the user cannot get more than what was owed.
+- [`Health.spec`](./specs/Health.spec) checks properties about the health of the positions.
+  Notably, functions cannot render an account unhealthy, and debt positions always have some collateral (thanks to the bad debt realization mechanism).
+- [`LibSummary.spec`](./specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files.
+- [`Liveness.spec`](./specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position.
+- [`RatioMath.spec`](./specs/RatioMath.spec) checks that the ratio between shares and assets evolves predictably over time.
+- [`Reentrancy.spec`](./specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues.
+- [`Reverts.spec`](./specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated.
+- [`Transfer.spec`](./specs/Transfer.spec) checks the summarization of the safe transfer library functions that are used in other specification files.
+
+The [`certora/scripts`](./scripts) folder contains a script for each corresponding specification file.
+
+The [`certora/harness`](./harness) folder contains contracts that enable the verification of Morpho Blue.
+Notably, this allows handling the fact that library functions should be called from a contract to be verified independently, and it allows defining needed getters.
+
+The [`certora/dispatch`](./dispatch) folder contains different contracts similar to the ones that are expected to be called from Morpho Blue.
+
+## Usage
+
+To verify specification files, run the corresponding script in the [`certora/scripts`](./scripts) folder.
+It requires having set the `CERTORAKEY` environment variable to a valid Certora key.
+You can pass arguments to the script, which allows you to verify specific properties. For example, at the root of the repository:
+
+```
+./certora/scripts/verifyConsistentState.sh --rule borrowLessSupply
+```
diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol
index 2e48332aa..600515f4b 100644
--- a/certora/harness/MorphoHarness.sol
+++ b/certora/harness/MorphoHarness.sol
@@ -70,21 +70,21 @@ contract MorphoHarness is Morpho {
         return market[id].totalBorrowShares + SharesMathLib.VIRTUAL_SHARES;
     }
 
-    function marketId(MarketParams memory marketParams) external pure returns (Id) {
+    function libId(MarketParams memory marketParams) external pure returns (Id) {
         return marketParams.id();
     }
 
-    function marketLibId(MarketParams memory marketParams) external pure returns (Id marketParamsId) {
+    function optimizedId(MarketParams memory marketParams) external pure returns (Id marketParamsId) {
         assembly ("memory-safe") {
             marketParamsId := keccak256(marketParams, mul(5, 32))
         }
     }
 
-    function mathLibMulDivUp(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
+    function libMulDivUp(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
         return MathLib.mulDivUp(x, y, d);
     }
 
-    function mathLibMulDivDown(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
+    function libMulDivDown(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
         return MathLib.mulDivDown(x, y, d);
     }
 
diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol
index 1cf77f9e7..1227e3fc7 100644
--- a/certora/harness/TransferHarness.sol
+++ b/certora/harness/TransferHarness.sol
@@ -13,11 +13,11 @@ interface IERC20Extended is IERC20 {
 contract TransferHarness {
     using SafeTransferLib for IERC20;
 
-    function safeTransferFrom(address token, address from, address to, uint256 value) public {
+    function libSafeTransferFrom(address token, address from, address to, uint256 value) public {
         IERC20(token).safeTransferFrom(from, to, value);
     }
 
-    function safeTransfer(address token, address to, uint256 value) public {
+    function libSafeTransfer(address token, address to, uint256 value) public {
         IERC20(token).safeTransfer(to, value);
     }
 
diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
index 9cb819b76..8915e0301 100644
--- a/certora/specs/ConsistentState.spec
+++ b/certora/specs/ConsistentState.spec
@@ -10,7 +10,7 @@ methods {
     function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
     function fee(MorphoHarness.Id) external returns uint256 envfree;
     function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 
     function isAuthorized(address, address) external returns bool envfree;
     function isLltvEnabled(uint256) external returns bool envfree;
@@ -108,9 +108,9 @@ invariant borrowLessSupply(MorphoHarness.Id id)
 
 // This invariant is useful in the following rule, to link an id back to a market.
 invariant marketInvariant(MorphoHarness.MarketParams marketParams)
-    isCreated(marketId(marketParams)) =>
-    idToBorrowable[marketId(marketParams)] == marketParams.borrowableToken &&
-    idToCollateral[marketId(marketParams)] == marketParams.collateralToken;
+    isCreated(libId(marketParams)) =>
+    idToBorrowable[libId(marketParams)] == marketParams.borrowableToken &&
+    idToCollateral[libId(marketParams)] == marketParams.collateralToken;
 
 // 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 isLiquid(address token)
@@ -148,19 +148,19 @@ invariant isLiquid(address token)
 
 // Check that a market can only exist if its LLTV is enabled.
 invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams)
-    isCreated(marketId(marketParams)) => isLltvEnabled(marketParams.lltv);
+    isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv);
 
 // Check that a market can only exist if its IRM is enabled.
 invariant onlyEnabledIrm(MorphoHarness.MarketParams marketParams)
-    isCreated(marketId(marketParams)) => isIrmEnabled(marketParams.irm);
+    isCreated(libId(marketParams)) => isIrmEnabled(marketParams.irm);
 
 // Check the pseudo-injectivity of the hashing function id().
-rule marketIdUnique() {
+rule libIdUnique() {
     MorphoHarness.MarketParams marketParams1;
     MorphoHarness.MarketParams marketParams2;
 
     // Require the same arguments.
-    require marketId(marketParams1) == marketId(marketParams2);
+    require libId(marketParams1) == libId(marketParams2);
 
     assert marketParams1.borrowableToken == marketParams2.borrowableToken;
     assert marketParams1.collateralToken == marketParams2.collateralToken;
diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec
index 8d94adfbc..d55385975 100644
--- a/certora/specs/ExactMath.spec
+++ b/certora/specs/ExactMath.spec
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
@@ -26,8 +26,9 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
     return require_uint256((x * y) / d);
 }
 
+// Check that when not accruing interest, and when repaying all, the borrow ratio is at least reset to the initial ratio.
 rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onbehalf, bytes data) {
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     require fee(id) <= maxFee();
 
     mathint assetsBefore = virtualTotalBorrowAssets(id);
@@ -44,12 +45,13 @@ rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, u
     mathint sharesAfter = virtualTotalBorrowShares(id);
 
     assert assetsAfter == 1;
+    // There are at least as many shares as virtual shares.
 }
 
 // There should be no profit from supply followed immediately by withdraw.
 rule supplyWithdraw() {
     MorphoHarness.MarketParams marketParams;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     uint256 assets;
     uint256 shares;
     address onbehalf;
@@ -82,7 +84,7 @@ rule supplyWithdraw() {
 // There should be no profit from withdraw followed immediately by supply.
 rule withdrawSupply() {
     MorphoHarness.MarketParams marketParams;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     uint256 assets;
     uint256 shares;
     address onbehalf;
diff --git a/certora/specs/ExitLiquidity.spec b/certora/specs/ExitLiquidity.spec
index a54a8e582..9f3fdd7bd 100644
--- a/certora/specs/ExitLiquidity.spec
+++ b/certora/specs/ExitLiquidity.spec
@@ -11,22 +11,22 @@ methods {
 
     function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
 
-    function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
-    function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
+    function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 }
 
 // Check that it's not possible to withdraw more assets than what the user has supplied.
 rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
     env e;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
 
     require lastUpdate(id) == e.block.timestamp;
 
     uint256 initialShares = supplyShares(id, onBehalf);
     uint256 initialTotalSupply = virtualTotalSupplyAssets(id);
     uint256 initialTotalSupplyShares = virtualTotalSupplyShares(id);
-    uint256 owedAssets = mathLibMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares);
+    uint256 owedAssets = libMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares);
 
     uint256 withdrawnAssets;
     withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver);
@@ -37,7 +37,7 @@ rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets,
 // Check that it's not possible to withdraw more collateral than what the user has supplied.
 rule withdrawCollateralLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) {
     env e;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
 
     uint256 initialCollateral = collateral(id, onBehalf);
 
@@ -49,14 +49,14 @@ rule withdrawCollateralLiquidity(MorphoHarness.MarketParams marketParams, uint25
 // Check than when repaying the full outstanding debt requires more assets than what was borrowed.
 rule repayLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
     env e;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
 
     require lastUpdate(id) == e.block.timestamp;
 
     uint256 initialShares = borrowShares(id, onBehalf);
     uint256 initialTotalBorrow = virtualTotalBorrowAssets(id);
     uint256 initialTotalBorrowShares = virtualTotalBorrowShares(id);
-    uint256 assetsDue = mathLibMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares);
+    uint256 assetsDue = libMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares);
 
     uint256 repaidAssets;
     repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data);
diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec
index c68e3c43e..5db3c3724 100644
--- a/certora/specs/Health.spec
+++ b/certora/specs/Health.spec
@@ -7,7 +7,7 @@ methods {
     function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
     function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree;
     function isAuthorized(address, address user) external returns bool envfree;
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 
     function _.price() external => mockPrice() expect uint256;
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
@@ -52,7 +52,7 @@ filtered {
 }
 {
     MorphoHarness.MarketParams marketParams;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     address user;
 
     // Require that the position is healthy before the interaction.
@@ -78,7 +78,7 @@ rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data)
 filtered { f -> !f.isView }
 {
     MorphoHarness.MarketParams marketParams;
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     address user;
 
     // Require that the e.msg.sender is not authorized.
diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec
index 9adec259a..6b88f842d 100644
--- a/certora/specs/LibSummary.spec
+++ b/certora/specs/LibSummary.spec
@@ -1,26 +1,26 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 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 marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
-    function marketLibId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
+    function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function optimizedId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 }
 
 // Check the summary of mulDivUp required by RatioMath.spec
 rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) {
-    uint256 result = mathLibMulDivUp(x, y, d);
+    uint256 result = libMulDivUp(x, y, d);
     assert result * d >= x * y;
 }
 
 // Check the summary of mulDivDown required by RatioMath.spec
 rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) {
-    uint256 result = mathLibMulDivDown(x, y, d);
+    uint256 result = libMulDivDown(x, y, d);
     assert result * d <= x * y;
 }
 
 // Check the munging of the MarketParams.id function.
 // This rule cannot be checked because it is not possible disable the keccak256 summary for the moment.
 // rule checkSummaryId(MorphoHarness.MarketParams marketParams) {
-//     assert marketLibId(marketParams) == marketId(marketParams);
+//     assert optimizedId(marketParams) == libId(marketParams);
 // }
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 334a65fa4..d97bfedb2 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -10,7 +10,7 @@ methods {
     function collateral(MorphoInternalAccess.Id, address) external returns uint256 envfree;
     function fee(MorphoInternalAccess.Id) external returns uint256 envfree;
     function lastUpdate(MorphoInternalAccess.Id) external returns uint256 envfree;
-    function marketId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree;
+    function libId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree;
 
     function _._accrueInterest(MorphoInternalAccess.MarketParams memory marketParams, MorphoInternalAccess.Id id) internal with (env e) => summaryAccrueInterest(e, marketParams, id) expect void;
 
@@ -51,7 +51,7 @@ definition isCreated(MorphoInternalAccess.Id id) returns bool =
 
 // Check that tokens and shares are properly accounted following a supply.
 rule supplyMovesTokensAndIncreasesShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
-    MorphoInternalAccess.Id id = marketId(marketParams);
+    MorphoInternalAccess.Id id = libId(marketParams);
 
     // Safe require that Morpho is not the sender.
     require e.msg.sender != currentContract;
@@ -77,7 +77,7 @@ rule supplyMovesTokensAndIncreasesShares(env e, MorphoInternalAccess.MarketParam
 // This rule is commented out for the moment because of a bug in CVL where market IDs are not consistent accross a run.
 // Check that one can always repay the debt in full.
 // rule canRepayAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, bytes data) {
-//     MorphoInternalAccess.Id id = marketId(marketParams);
+//     MorphoInternalAccess.Id id = libId(marketParams);
 
 //     require data.length == 0;
 
@@ -97,7 +97,7 @@ rule supplyMovesTokensAndIncreasesShares(env e, MorphoInternalAccess.MarketParam
 
 // Check the one can always withdraw all, under the condition that there are no outstanding debt on the market.
 rule canWithdrawAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address receiver) {
-    MorphoInternalAccess.Id id = marketId(marketParams);
+    MorphoInternalAccess.Id id = libId(marketParams);
 
     // Require to ensure a withdraw all.
     require shares == supplyShares(id, e.msg.sender);
@@ -122,7 +122,7 @@ rule canWithdrawAll(env e, MorphoInternalAccess.MarketParams marketParams, uint2
 // Check that a user can always withdraw all, under the condition that this user does not have an outstanding debt.
 // Combined with the canRepayAll rule, this ensures that a borrower can always fully exit a market.
 rule canWithdrawCollateralAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address receiver) {
-    MorphoInternalAccess.Id id = marketId(marketParams);
+    MorphoInternalAccess.Id id = libId(marketParams);
 
     // Ensure a withdrawCollateral all.
     require assets == collateral(id, e.msg.sender);
diff --git a/certora/specs/RatioMath.spec b/certora/specs/RatioMath.spec
index 36d4520ca..0844e834f 100644
--- a/certora/specs/RatioMath.spec
+++ b/certora/specs/RatioMath.spec
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
@@ -129,10 +129,10 @@ filtered {
 
 // Check that when not accruing interest, repay is decreasing the value of borrow shares.
 // Check the case where the market is not repaid fully.
-// The other case requires exact math (ie not summarizing mulDivUp and mulDivDown), so it is checked separately in ExactMath.spec
+// The other case requires exact math (ie not over-approximating mulDivUp and mulDivDown), so it is checked separately in ExactMath.spec
 rule repayDecreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data)
 {
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     requireInvariant feeInRange(id);
 
     mathint assetsBefore = virtualTotalBorrowAssets(id);
diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
index 0d009a898..82ebeabde 100644
--- a/certora/specs/Reentrancy.spec
+++ b/certora/specs/Reentrancy.spec
@@ -50,7 +50,7 @@ rule reentrancySafe(method f, calldataarg data, env e) {
     require !callIsBorrowRate;
     require !hasAccessedStorage && !hasCallAfterAccessingStorage && !hasReentrancyUnsafeCall;
     f(e,data);
-    assert !hasReentrancyUnsafeCall, "Method is not safe for reentrancy.";
+    assert !hasReentrancyUnsafeCall;
 }
 
 rule noDelegateCalls(method f, calldataarg data, env e) {
diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
index 5b9ef4d6f..7edcc6dce 100644
--- a/certora/specs/Reverts.spec
+++ b/certora/specs/Reverts.spec
@@ -13,7 +13,7 @@ methods {
     function isIrmEnabled(address) external returns bool envfree;
     function isAuthorized(address, address) external returns bool envfree;
 
-    function marketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function maxFee() external returns uint256 envfree;
     function wad() external returns uint256 envfree;
 }
@@ -83,7 +83,7 @@ rule enableLltvRevertCondition(env e, uint256 lltv) {
 // Check that setFee reverts when its inputs are not validated.
 // setFee can also revert if the accrueInterest reverts.
 rule setFeeInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 newFee) {
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     address oldOwner = owner();
     bool wasCreated = isCreated(id);
     setFee@withrevert(e, marketParams, newFee);
@@ -101,7 +101,7 @@ rule setFeeRecipientRevertCondition(env e, address newFeeRecipient) {
 
 // Check the revert condition for the createMarket function.
 rule createMarketRevertCondition(env e, MorphoHarness.MarketParams marketParams) {
-    MorphoHarness.Id id = marketId(marketParams);
+    MorphoHarness.Id id = libId(marketParams);
     bool irmEnabled = isIrmEnabled(marketParams.irm);
     bool lltvEnabled = isLltvEnabled(marketParams.lltv);
     uint256 lastUpdated = lastUpdate(id);
diff --git a/certora/specs/Transfer.spec b/certora/specs/Transfer.spec
index 25c744e4c..665acc248 100644
--- a/certora/specs/Transfer.spec
+++ b/certora/specs/Transfer.spec
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function safeTransfer(address, address, uint256) external envfree;
-    function safeTransferFrom(address, address, address, uint256) external envfree;
+    function libSafeTransfer(address, address, uint256) external envfree;
+    function libSafeTransferFrom(address, address, address, uint256) external envfree;
     function balanceOf(address, address) external returns (uint256) envfree;
     function allowance(address, address, address) external returns (uint256) envfree;
     function totalSupply(address) external returns (uint256) envfree;
@@ -32,7 +32,7 @@ rule checkTransferSummary(address token, address to, uint256 amount) {
     mathint initialBalance = balanceOf(token, currentContract);
     require to != currentContract => initialBalance + balanceOf(token, to) <= to_mathint(totalSupply(token));
 
-    safeTransfer(token, to, amount);
+    libSafeTransfer(token, to, amount);
     mathint finalBalance = balanceOf(token, currentContract);
 
     require myBalances[token] == initialBalance;
@@ -45,7 +45,7 @@ rule checkTransferFromSummary(address token, address from, uint256 amount) {
     mathint initialBalance = balanceOf(token, currentContract);
     require from != currentContract => initialBalance + balanceOf(token, from) <= to_mathint(totalSupply(token));
 
-    safeTransferFrom(token, from, currentContract, amount);
+    libSafeTransferFrom(token, from, currentContract, amount);
     mathint finalBalance = balanceOf(token, currentContract);
 
     require myBalances[token] == initialBalance;
@@ -60,7 +60,7 @@ rule transferRevertCondition(address token, address to, uint256 amount) {
     require to != currentContract => initialBalance + toInitialBalance <= to_mathint(totalSupply(token));
     require currentContract != 0 && to != 0;
 
-    safeTransfer@withrevert(token, to, amount);
+    libSafeTransfer@withrevert(token, to, amount);
 
     assert lastReverted == (initialBalance < amount);
 }
@@ -73,7 +73,7 @@ rule transferFromRevertCondition(address token, address from, address to, uint25
     require to != from => initialBalance + toInitialBalance <= to_mathint(totalSupply(token));
     require from != 0 && to != 0;
 
-    safeTransferFrom@withrevert(token, from, to, amount);
+    libSafeTransferFrom@withrevert(token, from, to, amount);
 
     assert lastReverted == (initialBalance < amount) || allowance < amount;
 }