diff --git a/certora/README.md b/certora/README.md
index c2156b68..7d7a94cb 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -90,7 +90,7 @@ Note also that these properties are ensured to always hold, because the contract
 
 ### Consistent asset
 
-For deposit and withdraw, it is checked that markets have a the same loan token as the loan token of the vault.
+For deposit and withdraw, it is checked that markets have the same loan token as the loan token of the vault.
 We say that such market has a consistent asset.
 The following function defined in [`ConsistentState.spec`](specs/ConsistentState.spec) is verified to always return `true` and contributes to verifying the property above.
 
diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
index 7e825094..fd2a7c15 100644
--- a/certora/specs/ConsistentState.spec
+++ b/certora/specs/ConsistentState.spec
@@ -11,7 +11,7 @@ methods {
     function Util.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree;
 }
 
-// Check that fee cannot accrue to an unset fee recipient.
+// Check that the fee cannot accrue to an unset fee recipient.
 invariant noFeeToUnsetFeeRecipient()
     feeRecipient() == 0 => fee() == 0;
 
diff --git a/certora/specs/LastUpdated.spec b/certora/specs/LastUpdated.spec
index 4fee4e59..8e36b3b9 100644
--- a/certora/specs/LastUpdated.spec
+++ b/certora/specs/LastUpdated.spec
@@ -19,10 +19,10 @@ function hasGuardianRole(address user) returns bool {
     return user == owner() || user == guardian();
 }
 
-// Check that any market with positive cap is created on Morpho Blue.
+// Check that any market with a positive cap is created on Morpho Blue.
 // The corresponding invariant is difficult to verify because it requires to check properties on MetaMorpho and on Blue at the same time:
 // - on MetaMorpho, that it holds when the cap is positive for the first time
-// - on Blue, that a created market always has positive last update
+// - on Blue, that a created market always has a positive last update
 function hasPositiveSupplyCapIsUpdated(MetaMorphoHarness.Id id) returns bool {
     return config_(id).cap > 0 => Morpho.lastUpdate(id) > 0;
 }
diff --git a/certora/specs/Roles.spec b/certora/specs/Roles.spec
index e04fb8d3..0d1f8fec 100644
--- a/certora/specs/Roles.spec
+++ b/certora/specs/Roles.spec
@@ -13,7 +13,7 @@ methods {
     function guardian() external returns(address) envfree;
     function isAllocator(address target) external returns(bool) envfree;
 
-    // Sumarize Morpho external calls, as they don't depend on the authorization system of MetaMorpho.
+    // Summarize Morpho external calls, as they don't depend on the authorization system of MetaMorpho.
     function _.idToMarketParams(MetaMorphoHarness.Id) external => CONSTANT;
     function _.supplyShares(MetaMorphoHarness.Id, address) external => CONSTANT;
     function _.accrueInterest(MetaMorphoHarness.MarketParams) external => CONSTANT;
diff --git a/certora/specs/Timelock.spec b/certora/specs/Timelock.spec
index 734e93e3..f2435d5d 100644
--- a/certora/specs/Timelock.spec
+++ b/certora/specs/Timelock.spec
@@ -97,7 +97,7 @@ rule capIncreaseTime(env e_next, method f, calldataarg args) {
     f(e_next, args);
 
     if (e_next.block.timestamp < nextTime)  {
-        // Check that cap cannot increase.
+        // Check that the cap cannot increase.
         assert config_(id).cap <= prevCap;
         // Increasing nextCapIncreaseTime with an interaction;
         assert nextCapIncreaseTime(e_next, id) >= nextCapIncreaseTimeBeforeInteraction;