From 50639fd8d07438803a7c053f214e680d88567316 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 18 Nov 2024 17:27:29 +0100
Subject: [PATCH 01/19] feat: add revert checks

---
 .github/workflows/certora.yml              |  4 ++
 certora/README.md                          |  5 +++
 certora/confs/RevertsERC20Ethereum.conf    | 18 +++++++++
 certora/confs/RevertsERC20Optimism.conf    | 18 +++++++++
 certora/confs/RevertsMintBurnEthereum.conf | 18 +++++++++
 certora/confs/RevertsMintBurnOptimis.conf  | 18 +++++++++
 certora/specs/RevertsERC20.spec            | 47 ++++++++++++++++++++++
 certora/specs/RevertsMintBurnEthereum.spec | 32 +++++++++++++++
 certora/specs/RevertsMintBurnOptimism.spec | 31 ++++++++++++++
 9 files changed, 191 insertions(+)
 create mode 100644 certora/confs/RevertsERC20Ethereum.conf
 create mode 100644 certora/confs/RevertsERC20Optimism.conf
 create mode 100644 certora/confs/RevertsMintBurnEthereum.conf
 create mode 100644 certora/confs/RevertsMintBurnOptimis.conf
 create mode 100644 certora/specs/RevertsERC20.spec
 create mode 100644 certora/specs/RevertsMintBurnEthereum.spec
 create mode 100644 certora/specs/RevertsMintBurnOptimism.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index ca7c2ce..7c9f8fe 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -18,6 +18,10 @@ jobs:
         conf:
           - ExternalCallsEthereum
           - ExternalCallsOptimism
+          - RevertsERC20Ethereum
+          - RevertsERC20Optimism
+          - RevertsMintBurnEthereum
+          - RevertsMintBurnOptimism
 
     steps:
       - uses: actions/checkout@v4
diff --git a/certora/README.md b/certora/README.md
index 5eb6271..530861e 100644
--- a/certora/README.md
+++ b/certora/README.md
@@ -24,6 +24,10 @@ Note: the compiled contracts may include loops related to handling strings from
 
 This is checked in [`ExternalCalls.spec`](specs/ExternalCalls.spec).
 
+### Reverts
+
+This is checks in [`RevertsERC20.spec`](specs/RevertsERC20.spec), [`RevertsMintBurnEthereum.spec`](specs/RevertsMintBurnEthereum.spec) and [`RevertsMintBurnOptimism.spec`](specs/RevertsMintBurnOptimism.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
@@ -31,5 +35,6 @@ This is checked in [`ExternalCalls.spec`](specs/ExternalCalls.spec).
 The [`certora/specs`](specs) folder contains the following files:
 
 - [`ExternalCalls.spec`](specs/Reentrancy.spec) checks that the Morpho token implementation is reentrancy safe by ensuring that no function is making and external calls and, that the implementation is immutable as it doesn't perform any delegate call.
+- [`RevertsERC20.spec`](specs/RevertsERC20.spec), [`RevertsMintBurnEthereum.spec`](specs/RevertsMintBurnEthereum.spec) and [`RevertsMintBurnOptimism.spec`](specs/RevertsMintBurnOptimism.spec) check that conditions for reverts and inputs are correctly validated.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file for both the Ethereum and the Optimism version.
diff --git a/certora/confs/RevertsERC20Ethereum.conf b/certora/confs/RevertsERC20Ethereum.conf
new file mode 100644
index 0000000..395290f
--- /dev/null
+++ b/certora/confs/RevertsERC20Ethereum.conf
@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenEthereum.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenEthereum"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenEthereum:certora/specs/RevertsERC20.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Reverts Ethereum"
+}
diff --git a/certora/confs/RevertsERC20Optimism.conf b/certora/confs/RevertsERC20Optimism.conf
new file mode 100644
index 0000000..af72342
--- /dev/null
+++ b/certora/confs/RevertsERC20Optimism.conf
@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenOptimism.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenOptimism"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenOptimism:certora/specs/RevertsERC20.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Reverts Optimism"
+}
diff --git a/certora/confs/RevertsMintBurnEthereum.conf b/certora/confs/RevertsMintBurnEthereum.conf
new file mode 100644
index 0000000..44d9375
--- /dev/null
+++ b/certora/confs/RevertsMintBurnEthereum.conf
@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenEthereum.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenEthereum"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenEthereum:certora/specs/RevertsMintBurnEthereum.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Mint Burn Reverts"
+}
diff --git a/certora/confs/RevertsMintBurnOptimis.conf b/certora/confs/RevertsMintBurnOptimis.conf
new file mode 100644
index 0000000..dce299b
--- /dev/null
+++ b/certora/confs/RevertsMintBurnOptimis.conf
@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/MorphoTokenOptimism.sol"
+  ],
+  "parametric_contracts": [
+    "MorphoTokenOptimism"
+  ],
+  "solc": "solc-0.8.27",
+  "verify": "MorphoTokenOptimism:certora/specs/RevertsMintBurnOptimism.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "packages": [
+    "@openzeppelin/contracts/=lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
+  ],
+  "loop_iter": "3",
+  "optimistic_loop": true,
+  "msg": "Morpho token ERC20 Mint Burn Reverts"
+}
diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
new file mode 100644
index 0000000..97a2aae
--- /dev/null
+++ b/certora/specs/RevertsERC20.spec
@@ -0,0 +1,47 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function balanceOf(address) external returns uint256 envfree;
+    function allowance(address, address) external returns uint256 envfree;
+
+    // Avoids checking delegation related overflows.
+    function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
+}
+
+// Check that transfers with zero address or too large amounts revert.
+rule transferReverts(env e, address to,uint256 amount) {
+    // Safe require as transfer is a non-payable function.
+    require e.msg.value == 0;
+
+    uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+
+    transfer@withrevert(e, to, amount);
+    assert !lastReverted <=> e.msg.sender != 0 && to !=0 && balanceOfSenderBefore >= amount;
+}
+
+
+// Check that transfersFrom with zero address or too large allowances revert.
+rule transferFromReverts(env e, address from, address to,uint256 amount) {
+    // Safe require as transferFrom is a non-payable function.
+    require e.msg.value == 0;
+
+    uint256 allowanceOfSenderBefore = allowance(from, e.msg.sender);
+
+    // Safe require that implies allowance is infinite.
+    require allowanceOfSenderBefore != max_uint256;
+
+    uint256 balanceOfFromBefore = balanceOf(from);
+
+    transferFrom@withrevert(e, from, to, amount);
+    assert !lastReverted <=> e.msg.sender != 0 && from != 0 && to !=0 && balanceOfFromBefore >= amount && allowanceOfSenderBefore >= amount;
+
+}
+
+// Check that approving with zero address reverts.
+rule approveReverts(env e, address to, uint256 value) {
+    // Safe require as approve is a non-payable function.
+    require e.msg.value == 0;
+
+    approve@withrevert(e, to, value);
+    assert !(lastReverted) <=> e.msg.sender != 0 && to != 0;
+}
diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
new file mode 100644
index 0000000..39d800c
--- /dev/null
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -0,0 +1,32 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function owner() external returns address envfree;
+    function totalSupply() external returns uint256 envfree;
+    function balanceOf(address) external returns uint256 envfree;
+
+    // Avoids checking delegation related overflows.
+    function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
+}
+
+// Check that minting to zero address or minter is not owner revert.
+rule mintReverts(env e, address to, uint256 amount) {
+    // Safe require as mint is a non-payable function.
+    require e.msg.value == 0;
+
+    require totalSupply() + amount <= max_uint256;
+
+    mint@withrevert(e, to, amount);
+    assert   !(lastReverted) <=> e.msg.sender == owner() && to != 0;
+}
+
+// Check that burnning from zero address or too large amounts revert.
+rule burnReverts(env e, address from, uint256 amount) {
+    // Safe require as burn is a non-payable function.
+
+    uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+    require e.msg.value == 0 ;
+
+    burn@withrevert(e, amount);
+    assert !lastReverted <=> e.msg.sender != 0 && balanceOfSenderBefore >= amount;
+}
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
new file mode 100644
index 0000000..94d20c1
--- /dev/null
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -0,0 +1,31 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function totalSupply() external returns uint256 envfree;
+    function balanceOf(address) external returns uint256 envfree;
+
+    // Avoids checking delegation related overflows.
+    function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
+}
+
+// Check that minting to zero address or msg.sender is not bridge revert.
+rule mintReverts(env e, address to, uint256 amount) {
+    // Safe require as mint is a non-payable function.
+    require e.msg.value == 0;
+
+    require totalSupply() + amount <= max_uint256;
+
+    mint@withrevert(e, to, amount);
+    assert   !(lastReverted) <=> e.msg.sender == currentContract.bridge && to != 0;
+}
+
+// Check that burnning from zero address, msg.sender is not bridge or too large amounts revert.
+rule burnReverts(env e, address from, uint256 amount) {
+    // Safe require as burn is a non-payable function.
+
+    uint256 balanceOfFromBefore = balanceOf(from);
+    require e.msg.value == 0 ;
+
+    burn@withrevert(e, from, amount);
+    assert !lastReverted <=> e.msg.sender == currentContract.bridge && from != 0 && balanceOfFromBefore >= amount;
+}

From ffb92d82365aa990a6a17f1fd52d7263d7942cf5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 18 Nov 2024 17:32:12 +0100
Subject: [PATCH 02/19] fix: conf pathname

---
 .../{RevertsMintBurnOptimis.conf => RevertsMintBurnOptimism.conf} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename certora/confs/{RevertsMintBurnOptimis.conf => RevertsMintBurnOptimism.conf} (100%)

diff --git a/certora/confs/RevertsMintBurnOptimis.conf b/certora/confs/RevertsMintBurnOptimism.conf
similarity index 100%
rename from certora/confs/RevertsMintBurnOptimis.conf
rename to certora/confs/RevertsMintBurnOptimism.conf

From 0530fa60e78c0e504becd3b20ac3014a65a07379 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 19 Nov 2024 16:36:39 +0100
Subject: [PATCH 03/19] fix: implement review comments

---
 certora/specs/RevertsERC20.spec            | 37 ++++++++--------------
 certora/specs/RevertsMintBurnEthereum.spec | 19 ++++-------
 certora/specs/RevertsMintBurnOptimism.spec | 21 ++++--------
 3 files changed, 28 insertions(+), 49 deletions(-)

diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index 97a2aae..38fa186 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -8,40 +8,31 @@ methods {
     function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
 }
 
-// Check that transfers with zero address or too large amounts revert.
-rule transferReverts(env e, address to,uint256 amount) {
-    // Safe require as transfer is a non-payable function.
-    require e.msg.value == 0;
-
+// Check the revert conditions for the transfer function.
+rule transferRevertConditions(env e, address to,uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
 
     transfer@withrevert(e, to, amount);
-    assert !lastReverted <=> e.msg.sender != 0 && to !=0 && balanceOfSenderBefore >= amount;
+    assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
 }
 
-
-// Check that transfersFrom with zero address or too large allowances revert.
-rule transferFromReverts(env e, address from, address to,uint256 amount) {
-    // Safe require as transferFrom is a non-payable function.
-    require e.msg.value == 0;
-
+// Check the revert conditions for the transferFrom function.
+rule transferFromRevertConditions(env e, address from, address to,uint256 amount) {
     uint256 allowanceOfSenderBefore = allowance(from, e.msg.sender);
-
-    // Safe require that implies allowance is infinite.
-    require allowanceOfSenderBefore != max_uint256;
-
     uint256 balanceOfFromBefore = balanceOf(from);
 
     transferFrom@withrevert(e, from, to, amount);
-    assert !lastReverted <=> e.msg.sender != 0 && from != 0 && to !=0 && balanceOfFromBefore >= amount && allowanceOfSenderBefore >= amount;
+    bool generalRevertConditions = from == 0 || to == 0 || balanceOfFromBefore < amount || e.msg.value != 0;
+    if (allowanceOfSenderBefore != max_uint256) {
+        assert lastReverted <=>  e.msg.sender == 0 || allowanceOfSenderBefore < amount || generalRevertConditions;
+    } else {
+        assert lastReverted <=> generalRevertConditions;
+    }
 
 }
 
-// Check that approving with zero address reverts.
-rule approveReverts(env e, address to, uint256 value) {
-    // Safe require as approve is a non-payable function.
-    require e.msg.value == 0;
-
+// Check the revert conditions for the approve function.
+rule approveRevertConditions(env e, address to, uint256 value) {
     approve@withrevert(e, to, value);
-    assert !(lastReverted) <=> e.msg.sender != 0 && to != 0;
+    assert lastReverted <=> e.msg.sender == 0 || to == 0 || e.msg.value != 0;
 }
diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
index 39d800c..3d93ba2 100644
--- a/certora/specs/RevertsMintBurnEthereum.spec
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -9,24 +9,19 @@ methods {
     function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
 }
 
-// Check that minting to zero address or minter is not owner revert.
-rule mintReverts(env e, address to, uint256 amount) {
-    // Safe require as mint is a non-payable function.
-    require e.msg.value == 0;
-
-    require totalSupply() + amount <= max_uint256;
+// Check the revert conditions for the burn function.
+rule mintRevertConditions(env e, address to, uint256 amount) {
+    mathint totalSupplyBefore = totalSupply();
 
     mint@withrevert(e, to, amount);
-    assert   !(lastReverted) <=> e.msg.sender == owner() && to != 0;
+    assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
 }
 
-// Check that burnning from zero address or too large amounts revert.
-rule burnReverts(env e, address from, uint256 amount) {
-    // Safe require as burn is a non-payable function.
-
+// Check the revert conditions for the burn function.
+rule burnRevertConditions(env e, address from, uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     require e.msg.value == 0 ;
 
     burn@withrevert(e, amount);
-    assert !lastReverted <=> e.msg.sender != 0 && balanceOfSenderBefore >= amount;
+    assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
 }
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index 94d20c1..04ce133 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -8,24 +8,17 @@ methods {
     function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
 }
 
-// Check that minting to zero address or msg.sender is not bridge revert.
-rule mintReverts(env e, address to, uint256 amount) {
-    // Safe require as mint is a non-payable function.
-    require e.msg.value == 0;
-
-    require totalSupply() + amount <= max_uint256;
+// Check the revert conditions for the mint function.
+rule mintRevertConditions(env e, address to, uint256 amount) {
+    mathint totalSupplyBefore = totalSupply();
 
     mint@withrevert(e, to, amount);
-    assert   !(lastReverted) <=> e.msg.sender == currentContract.bridge && to != 0;
+    assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || (totalSupplyBefore + amount) > max_uint256;
 }
 
-// Check that burnning from zero address, msg.sender is not bridge or too large amounts revert.
-rule burnReverts(env e, address from, uint256 amount) {
-    // Safe require as burn is a non-payable function.
-
+// Check the revert conditions for the burn function.
+rule burnRevertConditions(env e, address from, uint256 amount) {
     uint256 balanceOfFromBefore = balanceOf(from);
-    require e.msg.value == 0 ;
-
     burn@withrevert(e, from, amount);
-    assert !lastReverted <=> e.msg.sender == currentContract.bridge && from != 0 && balanceOfFromBefore >= amount;
+    assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;
 }

From 9025f3b5c34e16082305e6d4b97dc5bf96eb67f5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Wed, 20 Nov 2024 20:01:12 +0100
Subject: [PATCH 04/19] fix: cosmetics

---
 certora/specs/RevertsERC20.spec            | 4 ++--
 certora/specs/RevertsMintBurnOptimism.spec | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index 38fa186..b75657f 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -9,7 +9,7 @@ methods {
 }
 
 // Check the revert conditions for the transfer function.
-rule transferRevertConditions(env e, address to,uint256 amount) {
+rule transferRevertConditions(env e, address to, uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
 
     transfer@withrevert(e, to, amount);
@@ -17,7 +17,7 @@ rule transferRevertConditions(env e, address to,uint256 amount) {
 }
 
 // Check the revert conditions for the transferFrom function.
-rule transferFromRevertConditions(env e, address from, address to,uint256 amount) {
+rule transferFromRevertConditions(env e, address from, address to, uint256 amount) {
     uint256 allowanceOfSenderBefore = allowance(from, e.msg.sender);
     uint256 balanceOfFromBefore = balanceOf(from);
 
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index 04ce133..63da041 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -13,7 +13,7 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     mathint totalSupplyBefore = totalSupply();
 
     mint@withrevert(e, to, amount);
-    assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || (totalSupplyBefore + amount) > max_uint256;
+    assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
 }
 
 // Check the revert conditions for the burn function.

From a61550f74f2d08419d12aaf5204aaebb8a085608 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Thu, 21 Nov 2024 15:57:26 +0100
Subject: [PATCH 05/19] fix: delegatees voting power assumptions

---
 certora/specs/RevertsERC20.spec            | 24 +++++++++++++++++-----
 certora/specs/RevertsMintBurnEthereum.spec | 23 ++++++++++++++++-----
 certora/specs/RevertsMintBurnOptimism.spec | 21 ++++++++++++++++---
 3 files changed, 55 insertions(+), 13 deletions(-)

diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index b75657f..946f8a0 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -1,16 +1,23 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
 methods {
+    function totalSupply() external returns uint256 envfree;
     function balanceOf(address) external returns uint256 envfree;
     function allowance(address, address) external returns uint256 envfree;
-
-    // Avoids checking delegation related overflows.
-    function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
+    function delegatee(address) external returns address envfree;
+    function delegatedVotingPower(address) external returns uint256 envfree;
 }
 
 // Check the revert conditions for the transfer function.
 rule transferRevertConditions(env e, address to, uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+    uint256 senderVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
+    uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
+
+    // Assume that the delegatee voting power is greater or equal to the holder's balance.
+    require delegatee(e.msg.sender) !=0 => senderVotingPowerBefore >= balanceOfSenderBefore;
+    // Assume that if the holder's and recipient's delegatees are different and not the zero address then, the recipient delegatee's voting power doesn't count the holder's voting power.
+    require delegatee(to) !=0 && delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;
 
     transfer@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
@@ -19,10 +26,17 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
 // Check the revert conditions for the transferFrom function.
 rule transferFromRevertConditions(env e, address from, address to, uint256 amount) {
     uint256 allowanceOfSenderBefore = allowance(from, e.msg.sender);
-    uint256 balanceOfFromBefore = balanceOf(from);
+    uint256 balanceOfHolderBefore = balanceOf(from);
+    uint256 holderVotingPowerBefore = delegatedVotingPower(delegatee(from));
+    uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
+
+    // Assume that the delegatee voting power is greater or equal to the holder's balance.
+    require delegatee(from) !=0 => holderVotingPowerBefore >= balanceOfHolderBefore;
+    // Assume that if the holder's and recipient's delegatees are different and not the zero address then, the recipient delegatee's voting power doesn't count the holder's voting power.
+    require delegatee(to) !=0 && delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;
 
     transferFrom@withrevert(e, from, to, amount);
-    bool generalRevertConditions = from == 0 || to == 0 || balanceOfFromBefore < amount || e.msg.value != 0;
+    bool generalRevertConditions = from == 0 || to == 0 || balanceOfHolderBefore < amount || e.msg.value != 0;
     if (allowanceOfSenderBefore != max_uint256) {
         assert lastReverted <=>  e.msg.sender == 0 || allowanceOfSenderBefore < amount || generalRevertConditions;
     } else {
diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
index 3d93ba2..0980b92 100644
--- a/certora/specs/RevertsMintBurnEthereum.spec
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -4,23 +4,36 @@ methods {
     function owner() external returns address envfree;
     function totalSupply() external returns uint256 envfree;
     function balanceOf(address) external returns uint256 envfree;
-
-    // Avoids checking delegation related overflows.
-    function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
+    function delegatee(address) external returns address envfree;
+    function delegatedVotingPower(address) external returns uint256 envfree;
 }
 
 // Check the revert conditions for the burn function.
 rule mintRevertConditions(env e, address to, uint256 amount) {
     mathint totalSupplyBefore = totalSupply();
+    uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
+    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
+
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
+
+    // Assume that if the delegatee of the recipient is not the zero address then the newly minted amount is not counted in the delegatee's voting power.
+    require delegatee(to) !=0 => toVotingPowerBefore <= totalSupply() - amount;
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
 }
 
 // Check the revert conditions for the burn function.
-rule burnRevertConditions(env e, address from, uint256 amount) {
+rule burnRevertConditions(env e, uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
-    require e.msg.value == 0 ;
+    uint256 senderVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
+
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
+
+    // Assume that the delegatee's voting power is greater or equal to the holder's balance.
+    require delegatee(e.msg.sender) !=0 => senderVotingPowerBefore >= balanceOfSenderBefore;
 
     burn@withrevert(e, amount);
     assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index 63da041..ce8eca5 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -3,14 +3,21 @@
 methods {
     function totalSupply() external returns uint256 envfree;
     function balanceOf(address) external returns uint256 envfree;
-
-    // Avoids checking delegation related overflows.
-    function _._moveDelegateVotes(address, address, uint256) internal => CONSTANT;
+    function delegatee(address) external returns address envfree;
+    function delegatedVotingPower(address) external returns uint256 envfree;
 }
 
 // Check the revert conditions for the mint function.
 rule mintRevertConditions(env e, address to, uint256 amount) {
     mathint totalSupplyBefore = totalSupply();
+    uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
+
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
+
+    // Assume that if the delegatee of the recipient is not the zero address then the newly minted amount is not counted in the delegatee's voting power.
+    require delegatee(to) !=0 => toVotingPowerBefore <= totalSupply() - amount;
+
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
@@ -19,6 +26,14 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
 // Check the revert conditions for the burn function.
 rule burnRevertConditions(env e, address from, uint256 amount) {
     uint256 balanceOfFromBefore = balanceOf(from);
+    uint256 fromVotingPowerBefore = delegatedVotingPower(delegatee(from));
+
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
+
+    // Assume that the delegatee's voting power is greater or equal to the holder's balance.
+    require delegatee(from) !=0 => fromVotingPowerBefore >= balanceOfFromBefore;
+
     burn@withrevert(e, from, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;
 }

From db1e19bef5c9cff45b3ae2afe5d67da7b33b6260 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20=7C=20Morpho=20=F0=9F=A6=8B?= <colin@morpho.xyz>
Date: Fri, 22 Nov 2024 09:39:53 +0100
Subject: [PATCH 06/19] fix: formatting
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com>
Signed-off-by: Colin | Morpho 🦋 <colin@morpho.xyz>
---
 certora/specs/RevertsERC20.spec            | 8 ++++----
 certora/specs/RevertsMintBurnEthereum.spec | 4 ++--
 certora/specs/RevertsMintBurnOptimism.spec | 4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index 946f8a0..b75536a 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -15,9 +15,9 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
     // Assume that the delegatee voting power is greater or equal to the holder's balance.
-    require delegatee(e.msg.sender) !=0 => senderVotingPowerBefore >= balanceOfSenderBefore;
+    require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
     // Assume that if the holder's and recipient's delegatees are different and not the zero address then, the recipient delegatee's voting power doesn't count the holder's voting power.
-    require delegatee(to) !=0 && delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;
+    require delegatee(to) != 0 && delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;
 
     transfer@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
@@ -31,9 +31,9 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
     // Assume that the delegatee voting power is greater or equal to the holder's balance.
-    require delegatee(from) !=0 => holderVotingPowerBefore >= balanceOfHolderBefore;
+    require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore;
     // Assume that if the holder's and recipient's delegatees are different and not the zero address then, the recipient delegatee's voting power doesn't count the holder's voting power.
-    require delegatee(to) !=0 && delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;
+    require delegatee(to) != 0 && delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;
 
     transferFrom@withrevert(e, from, to, amount);
     bool generalRevertConditions = from == 0 || to == 0 || balanceOfHolderBefore < amount || e.msg.value != 0;
diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
index 0980b92..1afdd44 100644
--- a/certora/specs/RevertsMintBurnEthereum.spec
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -18,7 +18,7 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     require delegatee(0) == 0;
 
     // Assume that if the delegatee of the recipient is not the zero address then the newly minted amount is not counted in the delegatee's voting power.
-    require delegatee(to) !=0 => toVotingPowerBefore <= totalSupply() - amount;
+    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply() - amount;
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
@@ -33,7 +33,7 @@ rule burnRevertConditions(env e, uint256 amount) {
     require delegatee(0) == 0;
 
     // Assume that the delegatee's voting power is greater or equal to the holder's balance.
-    require delegatee(e.msg.sender) !=0 => senderVotingPowerBefore >= balanceOfSenderBefore;
+    require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
 
     burn@withrevert(e, amount);
     assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index ce8eca5..e2bec96 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -16,7 +16,7 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     require delegatee(0) == 0;
 
     // Assume that if the delegatee of the recipient is not the zero address then the newly minted amount is not counted in the delegatee's voting power.
-    require delegatee(to) !=0 => toVotingPowerBefore <= totalSupply() - amount;
+    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply() - amount;
 
 
     mint@withrevert(e, to, amount);
@@ -32,7 +32,7 @@ rule burnRevertConditions(env e, address from, uint256 amount) {
     require delegatee(0) == 0;
 
     // Assume that the delegatee's voting power is greater or equal to the holder's balance.
-    require delegatee(from) !=0 => fromVotingPowerBefore >= balanceOfFromBefore;
+    require delegatee(from) != 0 => fromVotingPowerBefore >= balanceOfFromBefore;
 
     burn@withrevert(e, from, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;

From 5b3c0b33b625517b61136705039ab332467074e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 22 Nov 2024 10:12:24 +0100
Subject: [PATCH 07/19] fix: change comments

---
 certora/specs/RevertsERC20.spec            | 12 ++++++------
 certora/specs/RevertsMintBurnEthereum.spec |  4 ++--
 certora/specs/RevertsMintBurnOptimism.spec |  5 ++---
 3 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index b75536a..1fa7738 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -14,10 +14,10 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
     uint256 senderVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Assume that the delegatee voting power is greater or equal to the holder's balance.
+    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
     require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
-    // Assume that if the holder's and recipient's delegatees are different and not the zero address then, the recipient delegatee's voting power doesn't count the holder's voting power.
-    require delegatee(to) != 0 && delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;
+    // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance.
+    require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;
 
     transfer@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
@@ -30,10 +30,10 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
     uint256 holderVotingPowerBefore = delegatedVotingPower(delegatee(from));
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Assume that the delegatee voting power is greater or equal to the holder's balance.
+    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
     require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore;
-    // Assume that if the holder's and recipient's delegatees are different and not the zero address then, the recipient delegatee's voting power doesn't count the holder's voting power.
-    require delegatee(to) != 0 && delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;
+    // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance.
+    require delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;
 
     transferFrom@withrevert(e, from, to, amount);
     bool generalRevertConditions = from == 0 || to == 0 || balanceOfHolderBefore < amount || e.msg.value != 0;
diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
index 1afdd44..92f3760 100644
--- a/certora/specs/RevertsMintBurnEthereum.spec
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -17,7 +17,7 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     // Safe require as zero address can't possibly delegate voting power.
     require delegatee(0) == 0;
 
-    // Assume that if the delegatee of the recipient is not the zero address then the newly minted amount is not counted in the delegatee's voting power.
+    // Safe require because if the delegatee is not zero the recipient's voting power excludes the newly minted value.
     require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply() - amount;
 
     mint@withrevert(e, to, amount);
@@ -32,7 +32,7 @@ rule burnRevertConditions(env e, uint256 amount) {
     // Safe require as zero address can't possibly delegate voting power.
     require delegatee(0) == 0;
 
-    // Assume that the delegatee's voting power is greater or equal to the holder's balance.
+    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
     require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
 
     burn@withrevert(e, amount);
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index e2bec96..78495b2 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -15,10 +15,9 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     // Safe require as zero address can't possibly delegate voting power.
     require delegatee(0) == 0;
 
-    // Assume that if the delegatee of the recipient is not the zero address then the newly minted amount is not counted in the delegatee's voting power.
+    // Safe require because if the delegatee is not zero the recipient's voting power excludes the newly minted value.
     require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply() - amount;
 
-
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
 }
@@ -31,7 +30,7 @@ rule burnRevertConditions(env e, address from, uint256 amount) {
     // Safe require as zero address can't possibly delegate voting power.
     require delegatee(0) == 0;
 
-    // Assume that the delegatee's voting power is greater or equal to the holder's balance.
+    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
     require delegatee(from) != 0 => fromVotingPowerBefore >= balanceOfFromBefore;
 
     burn@withrevert(e, from, amount);

From 408a9357565e98c4ea6dd884a07e00044a798761 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 22 Nov 2024 15:03:53 +0100
Subject: [PATCH 08/19] fix: improve specs

---
 certora/specs/RevertsMintBurnEthereum.spec | 4 ++--
 certora/specs/RevertsMintBurnOptimism.spec | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
index 92f3760..f08b3d6 100644
--- a/certora/specs/RevertsMintBurnEthereum.spec
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -17,8 +17,8 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     // Safe require as zero address can't possibly delegate voting power.
     require delegatee(0) == 0;
 
-    // Safe require because if the delegatee is not zero the recipient's voting power excludes the newly minted value.
-    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply() - amount;
+    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
+    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index 78495b2..5d2b1fe 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -15,8 +15,8 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     // Safe require as zero address can't possibly delegate voting power.
     require delegatee(0) == 0;
 
-    // Safe require because if the delegatee is not zero the recipient's voting power excludes the newly minted value.
-    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply() - amount;
+    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
+    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;

From 1b679307ba4245b7d591ba01045c16ca01ef07f4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 26 Nov 2024 09:25:33 +0100
Subject: [PATCH 09/19] fix: naming

---
 certora/specs/RevertsMintBurnEthereum.spec | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
index f08b3d6..63a1d1f 100644
--- a/certora/specs/RevertsMintBurnEthereum.spec
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -27,13 +27,13 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
 // Check the revert conditions for the burn function.
 rule burnRevertConditions(env e, uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
-    uint256 senderVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
+    uint256 delegateeVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
 
     // Safe require as zero address can't possibly delegate voting power.
     require delegatee(0) == 0;
 
     // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
+    require delegatee(e.msg.sender) != 0 => delegateeVotingPowerBefore >= balanceOfSenderBefore;
 
     burn@withrevert(e, amount);
     assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;

From 94fef53c70387af12e07e830685f67c5fdd127cf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Fri, 6 Dec 2024 18:59:24 +0100
Subject: [PATCH 10/19] chore: update specs

---
 certora/confs/RevertsMintBurnEthereum.conf |  7 ++++---
 certora/confs/RevertsMintBurnOptimism.conf |  7 ++++---
 certora/specs/RevertsMintBurnEthereum.spec | 24 ++++++++++++++--------
 certora/specs/RevertsMintBurnOptimism.spec | 20 ++++++++++++------
 4 files changed, 38 insertions(+), 20 deletions(-)

diff --git a/certora/confs/RevertsMintBurnEthereum.conf b/certora/confs/RevertsMintBurnEthereum.conf
index 44d9375..586b14c 100644
--- a/certora/confs/RevertsMintBurnEthereum.conf
+++ b/certora/confs/RevertsMintBurnEthereum.conf
@@ -1,12 +1,13 @@
 {
   "files": [
-    "src/MorphoTokenEthereum.sol"
+    "certora/helpers/MorphoTokenEthereumHarness.sol",
+    "certora/helpers/MorphoTokenOptimismHarness.sol"
   ],
   "parametric_contracts": [
-    "MorphoTokenEthereum"
+    "MorphoTokenEthereumHarness"
   ],
   "solc": "solc-0.8.27",
-  "verify": "MorphoTokenEthereum:certora/specs/RevertsMintBurnEthereum.spec",
+  "verify": "MorphoTokenEthereumHarness:certora/specs/RevertsMintBurnEthereum.spec",
   "rule_sanity": "basic",
   "server": "production",
   "packages": [
diff --git a/certora/confs/RevertsMintBurnOptimism.conf b/certora/confs/RevertsMintBurnOptimism.conf
index dce299b..75a27fd 100644
--- a/certora/confs/RevertsMintBurnOptimism.conf
+++ b/certora/confs/RevertsMintBurnOptimism.conf
@@ -1,12 +1,13 @@
 {
   "files": [
-    "src/MorphoTokenOptimism.sol"
+    "certora/helpers/MorphoTokenEthereumHarness.sol",
+    "certora/helpers/MorphoTokenOptimismHarness.sol"
   ],
   "parametric_contracts": [
-    "MorphoTokenOptimism"
+    "MorphoTokenOptimismHarness"
   ],
   "solc": "solc-0.8.27",
-  "verify": "MorphoTokenOptimism:certora/specs/RevertsMintBurnOptimism.spec",
+  "verify": "MorphoTokenOptimismHarness:certora/specs/RevertsMintBurnOptimism.spec",
   "rule_sanity": "basic",
   "server": "production",
   "packages": [
diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
index 63a1d1f..94772b0 100644
--- a/certora/specs/RevertsMintBurnEthereum.spec
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -1,5 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
+import "Delegation.spec";
+
 methods {
     function owner() external returns address envfree;
     function totalSupply() external returns uint256 envfree;
@@ -10,30 +12,36 @@ methods {
 
 // Check the revert conditions for the burn function.
 rule mintRevertConditions(env e, address to, uint256 amount) {
+    requireInvariant zeroAddressNoVotingPower();
+    assert isTotalSupplyGTEqSumOfVotingPower();
     mathint totalSupplyBefore = totalSupply();
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require as zero address can't possibly delegate voting power.
-    require delegatee(0) == 0;
-
-    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
+    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens.
     require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
 
+    // Safe require thats avoid absurd counter-examples introduced by munging the sources.
+    require toVotingPowerBefore <= sumOfVotingPower;
+
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
 }
 
 // Check the revert conditions for the burn function.
 rule burnRevertConditions(env e, uint256 amount) {
+    requireInvariant zeroAddressNoVotingPower();
+    assert isTotalSupplyGTEqSumOfVotingPower();
+
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 delegateeVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
 
-    // Safe require as zero address can't possibly delegate voting power.
-    require delegatee(0) == 0;
+    // Safe requires because a holder's balance is added to the delegatee's voting power upon delegation.
+    require delegatee(e.msg.sender) != 0 => balanceOfSenderBefore <= delegateeVotingPowerBefore;
 
-    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(e.msg.sender) != 0 => delegateeVotingPowerBefore >= balanceOfSenderBefore;
+    // Safe requires thats avoid absurd counter-examples introduced by munging the sources.
+    require delegateeVotingPowerBefore <= sumOfVotingPower;
+    require amount <= delegateeVotingPowerBefore;
 
     burn@withrevert(e, amount);
     assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index 5d2b1fe..54fa5dc 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -1,5 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
+import "Delegation.spec";
+
 methods {
     function totalSupply() external returns uint256 envfree;
     function balanceOf(address) external returns uint256 envfree;
@@ -9,30 +11,36 @@ methods {
 
 // Check the revert conditions for the mint function.
 rule mintRevertConditions(env e, address to, uint256 amount) {
+    requireInvariant zeroAddressNoVotingPower();
+    assert isTotalSupplyGTEqSumOfVotingPower();
     mathint totalSupplyBefore = totalSupply();
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require as zero address can't possibly delegate voting power.
-    require delegatee(0) == 0;
-
     // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
     require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
 
+    // Safe require thats avoid absurd counter-examples introduced by munging the sources.
+    require toVotingPowerBefore <= sumOfVotingPower;
+
+
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
 }
 
 // Check the revert conditions for the burn function.
 rule burnRevertConditions(env e, address from, uint256 amount) {
+    requireInvariant zeroAddressNoVotingPower();
+    assert isTotalSupplyGTEqSumOfVotingPower();
     uint256 balanceOfFromBefore = balanceOf(from);
     uint256 fromVotingPowerBefore = delegatedVotingPower(delegatee(from));
 
-    // Safe require as zero address can't possibly delegate voting power.
-    require delegatee(0) == 0;
-
     // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
     require delegatee(from) != 0 => fromVotingPowerBefore >= balanceOfFromBefore;
 
+    // Safe requires thats avoid absurd counter-examples introduced by munging the sources.
+    require fromVotingPowerBefore <= sumOfVotingPower;
+    require amount <= fromVotingPowerBefore;
+
     burn@withrevert(e, from, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;
 }

From f53d88d91efa7b48557af6f8353e8616600fb806 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 9 Dec 2024 15:35:39 +0100
Subject: [PATCH 11/19] Revert "chore: update specs"

This reverts commit 94fef53c70387af12e07e830685f67c5fdd127cf.
---
 certora/confs/RevertsMintBurnEthereum.conf |  7 +++----
 certora/confs/RevertsMintBurnOptimism.conf |  7 +++----
 certora/specs/RevertsMintBurnEthereum.spec | 24 ++++++++--------------
 certora/specs/RevertsMintBurnOptimism.spec | 20 ++++++------------
 4 files changed, 20 insertions(+), 38 deletions(-)

diff --git a/certora/confs/RevertsMintBurnEthereum.conf b/certora/confs/RevertsMintBurnEthereum.conf
index 586b14c..44d9375 100644
--- a/certora/confs/RevertsMintBurnEthereum.conf
+++ b/certora/confs/RevertsMintBurnEthereum.conf
@@ -1,13 +1,12 @@
 {
   "files": [
-    "certora/helpers/MorphoTokenEthereumHarness.sol",
-    "certora/helpers/MorphoTokenOptimismHarness.sol"
+    "src/MorphoTokenEthereum.sol"
   ],
   "parametric_contracts": [
-    "MorphoTokenEthereumHarness"
+    "MorphoTokenEthereum"
   ],
   "solc": "solc-0.8.27",
-  "verify": "MorphoTokenEthereumHarness:certora/specs/RevertsMintBurnEthereum.spec",
+  "verify": "MorphoTokenEthereum:certora/specs/RevertsMintBurnEthereum.spec",
   "rule_sanity": "basic",
   "server": "production",
   "packages": [
diff --git a/certora/confs/RevertsMintBurnOptimism.conf b/certora/confs/RevertsMintBurnOptimism.conf
index 75a27fd..dce299b 100644
--- a/certora/confs/RevertsMintBurnOptimism.conf
+++ b/certora/confs/RevertsMintBurnOptimism.conf
@@ -1,13 +1,12 @@
 {
   "files": [
-    "certora/helpers/MorphoTokenEthereumHarness.sol",
-    "certora/helpers/MorphoTokenOptimismHarness.sol"
+    "src/MorphoTokenOptimism.sol"
   ],
   "parametric_contracts": [
-    "MorphoTokenOptimismHarness"
+    "MorphoTokenOptimism"
   ],
   "solc": "solc-0.8.27",
-  "verify": "MorphoTokenOptimismHarness:certora/specs/RevertsMintBurnOptimism.spec",
+  "verify": "MorphoTokenOptimism:certora/specs/RevertsMintBurnOptimism.spec",
   "rule_sanity": "basic",
   "server": "production",
   "packages": [
diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
index 94772b0..63a1d1f 100644
--- a/certora/specs/RevertsMintBurnEthereum.spec
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -1,7 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-import "Delegation.spec";
-
 methods {
     function owner() external returns address envfree;
     function totalSupply() external returns uint256 envfree;
@@ -12,17 +10,15 @@ methods {
 
 // Check the revert conditions for the burn function.
 rule mintRevertConditions(env e, address to, uint256 amount) {
-    requireInvariant zeroAddressNoVotingPower();
-    assert isTotalSupplyGTEqSumOfVotingPower();
     mathint totalSupplyBefore = totalSupply();
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens.
-    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
 
-    // Safe require thats avoid absurd counter-examples introduced by munging the sources.
-    require toVotingPowerBefore <= sumOfVotingPower;
+    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
+    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
@@ -30,18 +26,14 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
 
 // Check the revert conditions for the burn function.
 rule burnRevertConditions(env e, uint256 amount) {
-    requireInvariant zeroAddressNoVotingPower();
-    assert isTotalSupplyGTEqSumOfVotingPower();
-
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 delegateeVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
 
-    // Safe requires because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(e.msg.sender) != 0 => balanceOfSenderBefore <= delegateeVotingPowerBefore;
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
 
-    // Safe requires thats avoid absurd counter-examples introduced by munging the sources.
-    require delegateeVotingPowerBefore <= sumOfVotingPower;
-    require amount <= delegateeVotingPowerBefore;
+    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
+    require delegatee(e.msg.sender) != 0 => delegateeVotingPowerBefore >= balanceOfSenderBefore;
 
     burn@withrevert(e, amount);
     assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index 54fa5dc..5d2b1fe 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -1,7 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-import "Delegation.spec";
-
 methods {
     function totalSupply() external returns uint256 envfree;
     function balanceOf(address) external returns uint256 envfree;
@@ -11,36 +9,30 @@ methods {
 
 // Check the revert conditions for the mint function.
 rule mintRevertConditions(env e, address to, uint256 amount) {
-    requireInvariant zeroAddressNoVotingPower();
-    assert isTotalSupplyGTEqSumOfVotingPower();
     mathint totalSupplyBefore = totalSupply();
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
+
     // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
     require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
 
-    // Safe require thats avoid absurd counter-examples introduced by munging the sources.
-    require toVotingPowerBefore <= sumOfVotingPower;
-
-
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
 }
 
 // Check the revert conditions for the burn function.
 rule burnRevertConditions(env e, address from, uint256 amount) {
-    requireInvariant zeroAddressNoVotingPower();
-    assert isTotalSupplyGTEqSumOfVotingPower();
     uint256 balanceOfFromBefore = balanceOf(from);
     uint256 fromVotingPowerBefore = delegatedVotingPower(delegatee(from));
 
+    // Safe require as zero address can't possibly delegate voting power.
+    require delegatee(0) == 0;
+
     // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
     require delegatee(from) != 0 => fromVotingPowerBefore >= balanceOfFromBefore;
 
-    // Safe requires thats avoid absurd counter-examples introduced by munging the sources.
-    require fromVotingPowerBefore <= sumOfVotingPower;
-    require amount <= fromVotingPowerBefore;
-
     burn@withrevert(e, from, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;
 }

From 1c09db876fdef798444ac9922867c90f8d816660 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 9 Dec 2024 16:53:48 +0100
Subject: [PATCH 12/19] refactor: change require-statements and improve docs

---
 certora/specs/RevertsERC20.spec            |  9 +++++----
 certora/specs/RevertsMintBurnEthereum.spec | 12 ++++++------
 certora/specs/RevertsMintBurnOptimism.spec | 10 +++++-----
 3 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index 1fa7738..22567a4 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -14,8 +14,8 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
     uint256 senderVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require senderVotingPowerBefore >= balanceOfSenderBefore;
     // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance.
     require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;
 
@@ -30,8 +30,9 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
     uint256 holderVotingPowerBefore = delegatedVotingPower(delegatee(from));
     uint256 recipientVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require holderVotingPowerBefore >= balanceOfHolderBefore;
+
     // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance.
     require delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;
 
diff --git a/certora/specs/RevertsMintBurnEthereum.spec b/certora/specs/RevertsMintBurnEthereum.spec
index 63a1d1f..bbc5d1b 100644
--- a/certora/specs/RevertsMintBurnEthereum.spec
+++ b/certora/specs/RevertsMintBurnEthereum.spec
@@ -14,11 +14,11 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require as zero address can't possibly delegate voting power.
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower .
     require delegatee(0) == 0;
 
-    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
-    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
+    // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
+    require toVotingPowerBefore <= totalSupply();
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != owner() || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
@@ -29,11 +29,11 @@ rule burnRevertConditions(env e, uint256 amount) {
     uint256 balanceOfSenderBefore = balanceOf(e.msg.sender);
     uint256 delegateeVotingPowerBefore = delegatedVotingPower(delegatee(e.msg.sender));
 
-    // Safe require as zero address can't possibly delegate voting power.
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower .
     require delegatee(0) == 0;
 
-    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(e.msg.sender) != 0 => delegateeVotingPowerBefore >= balanceOfSenderBefore;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require delegateeVotingPowerBefore >= balanceOfSenderBefore;
 
     burn@withrevert(e, amount);
     assert lastReverted <=> e.msg.sender == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index 5d2b1fe..cfcb818 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -12,11 +12,11 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     mathint totalSupplyBefore = totalSupply();
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require as zero address can't possibly delegate voting power.
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower .
     require delegatee(0) == 0;
 
-    // Safe require because if the delegatee is not zero the recipient's delegatee's voting power is lesser than or equal to the total supply of tokens
-    require delegatee(to) != 0 => toVotingPowerBefore <= totalSupply();
+    // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
+    require toVotingPowerBefore <= totalSupply();
 
     mint@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || to == 0 || e.msg.value != 0 || totalSupplyBefore + amount > max_uint256;
@@ -30,8 +30,8 @@ rule burnRevertConditions(env e, address from, uint256 amount) {
     // Safe require as zero address can't possibly delegate voting power.
     require delegatee(0) == 0;
 
-    // Safe require because a holder's balance is added to the delegatee's voting power upon delegation.
-    require delegatee(from) != 0 => fromVotingPowerBefore >= balanceOfFromBefore;
+    // Safe require as it is verified in delegatedLTEqDelegateeVP.
+    require fromVotingPowerBefore >= balanceOfFromBefore;
 
     burn@withrevert(e, from, amount);
     assert lastReverted <=> e.msg.sender != currentContract.bridge || from == 0 || balanceOfFromBefore < amount ||  e.msg.value != 0;

From 7db9d33e3c25fbec5380c17ff872e57edd4fa93b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Mon, 9 Dec 2024 19:46:14 +0100
Subject: [PATCH 13/19] feat: add more invariants on delegation

---
 certora/specs/Delegation.spec | 104 ++++++++++++++++++++++++----------
 1 file changed, 75 insertions(+), 29 deletions(-)

diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec
index 6578434..a653b08 100644
--- a/certora/specs/Delegation.spec
+++ b/certora/specs/Delegation.spec
@@ -6,8 +6,7 @@ methods {
     function delegationNonce(address) external returns uint256 envfree;
 }
 
-// Ghost variable to hold the sum of voting power.
-// To reason exhaustively on the value of of delegated voting power we proceed to compute the partial sum of balances for each possible address.
+// To reason exhaustively on the value of of delegated voting power we proceed to compute the partial sum of delegated votes to parametre A for each possible address.
 // We call the partial sum of votes to parameter A up to an addrress a, to sum of delegated votes to parameter A for all addresses within the range [0..a[.
 // Formally, we write ∀ a:address, sumsOfVotesDelegatedToA[a] = Σ balanceOf(i), where the sum ranges over addresses i such that i < a and delegatee(i) = A, provided that the address zero holds no voting power and that it never performs transactions.
 // With this approach, we are able to write and check more abstract properties about the computation of the total delegated voting power using universal quantifiers.
@@ -15,8 +14,10 @@ methods {
 // In particular, we have the equality sumsOfVotesDelegatedToA[2^160] = delegatedVotingPower(A).
 // Finally, we reason by parametricity to observe since we have ∀ a:address, delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A).
 // We also have ∀ A:address, ∀ a:address, A ≠ 0 ∧ delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A), which is what we want to show.
-ghost mathint sumOfVotingPower {
-    init_state axiom sumOfVotingPower == 0;
+
+// Ghost variable to hold the sum of voting power.
+ghost mapping (mathint => mathint) sumOfVotes {
+    init_state axiom forall mathint account. sumOfVotes[account] == 0;
 }
 
 // Ghost copy of DelegationTokenStorage._delegatedVotingPower.
@@ -32,8 +33,10 @@ hook Sload uint256 votingPower (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b
 hook Sstore (slot 0x669be2f4ee1b0b5f3858e4135f31064efe8fa923b09bf21bf538f64f2c3e1101)[KEY address account] uint256 votingPower (uint256 votingPowerOld) {
     // Update DelegationTokenStorage._delegatedVotingPower
     ghostDelegatedVotingPower[account] = votingPower;
-    // Track changes of total voting power.
-    sumOfVotingPower = sumOfVotingPower - votingPowerOld + votingPower;
+    // Track balance changes in sum of votes.
+    havoc sumOfVotes assuming
+        forall mathint x. sumOfVotes@new[x] ==
+            sumOfVotes@old[x] + (to_mathint(account) < x ? votingPower - votingPowerOld : 0);
 }
 
 // Check that zero address has no voting power assuming that zero address can't make transactions.
@@ -42,19 +45,19 @@ invariant zeroAddressNoVotingPower()
     { preserved with (env e) { require e.msg.sender != 0; } }
 
 // Check that initially zero votes are delegated to parameterized address A.
-invariant sumOfVotesStartsAtZero()
+invariant sumOfVotesDelegatedToAStartsAtZero()
     sumsOfVotesDelegatedToA[0] == 0;
 
-invariant sumOfVotesGrowsCorrectly()
+invariant sumOfVotesDelegatedToAGrowsCorrectly()
     forall address account. sumsOfVotesDelegatedToA[to_mathint(account) + 1] ==
     sumsOfVotesDelegatedToA[to_mathint(account)] + (ghostDelegatee[account] == A ? ghostBalances[account] : 0) ;
 
-invariant sumOfVotesMonotone()
+invariant sumOfVotesDelegatedToAMonotone()
     forall mathint i. forall mathint j. i <= j => sumsOfVotesDelegatedToA[i] <= sumsOfVotesDelegatedToA[j]
     {
         preserved {
-            requireInvariant sumOfVotesStartsAtZero();
-            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesDelegatedToAStartsAtZero();
+            requireInvariant sumOfVotesDelegatedToAGrowsCorrectly();
         }
     }
 
@@ -63,21 +66,21 @@ invariant delegatedLTEqPartialSum()
       ghostBalances[account] <= sumsOfVotesDelegatedToA[to_mathint(account)+1]
     {
         preserved {
-            requireInvariant sumOfVotesStartsAtZero();
-            requireInvariant sumOfVotesGrowsCorrectly();
-            requireInvariant sumOfVotesMonotone();
+            requireInvariant sumOfVotesDelegatedToAStartsAtZero();
+            requireInvariant sumOfVotesDelegatedToAGrowsCorrectly();
+            requireInvariant sumOfVotesDelegatedToAMonotone();
         }
     }
 
 
-invariant sumOfVotesIsDelegatedToA()
+invariant sumOfVotesDelegatedToAIsDelegatedToA()
     sumsOfVotesDelegatedToA[2^160] == ghostDelegatedVotingPower[A]
     {
         preserved {
             requireInvariant zeroAddressNoVotingPower();
-            requireInvariant sumOfVotesStartsAtZero();
-            requireInvariant sumOfVotesGrowsCorrectly();
-            requireInvariant sumOfVotesMonotone();
+            requireInvariant sumOfVotesDelegatedToAStartsAtZero();
+            requireInvariant sumOfVotesDelegatedToAGrowsCorrectly();
+            requireInvariant sumOfVotesDelegatedToAMonotone();
         }
     }
 
@@ -88,38 +91,81 @@ invariant delegatedLTEqDelegateeVP()
     {
         preserved with (env e){
             requireInvariant zeroAddressNoVotingPower();
+            requireInvariant sumOfVotesDelegatedToAStartsAtZero();
+            requireInvariant sumOfVotesDelegatedToAGrowsCorrectly();
+            requireInvariant sumOfVotesDelegatedToAMonotone();
+            requireInvariant delegatedLTEqPartialSum();
+            requireInvariant sumOfVotesDelegatedToAIsDelegatedToA();
+        }
+    }
+
+invariant sumOfVotesStartsAtZero()
+    sumOfVotes[0] == 0;
+
+invariant sumOfVotesGrowsCorrectly()
+    forall address addr. sumOfVotes[to_mathint(addr) + 1] ==
+      sumOfVotes[to_mathint(addr)] + ghostDelegatedVotingPower[addr];
+
+invariant sumOfVotesMonotone()
+    forall mathint i. forall mathint j. i <= j => sumOfVotes[i] <= sumOfVotes[j]
+    {
+        preserved {
             requireInvariant sumOfVotesStartsAtZero();
             requireInvariant sumOfVotesGrowsCorrectly();
-            requireInvariant sumOfVotesMonotone();
-            requireInvariant delegatedLTEqPartialSum();
-            requireInvariant sumOfVotesIsDelegatedToA();
         }
     }
 
 // Check that the voting power plus the virtual voting power of address zero is equal to the total supply of tokens.
 invariant totalSupplyIsSumOfVirtualVotingPower()
-    to_mathint(totalSupply()) == sumOfVotingPower + currentContract._zeroVirtualVotingPower
+    sumOfVotes[2^160] + currentContract._zeroVirtualVotingPower == to_mathint(totalSupply())
     {
+        preserved {
+            requireInvariant sumOfBalancesStartsAtZero();
+            requireInvariant sumOfBalancesGrowsCorrectly();
+            requireInvariant sumOfBalancesMonotone();
+            requireInvariant totalSupplyIsSumOfBalances();
+            requireInvariant zeroAddressNoVotingPower();
+            requireInvariant balancesLTEqTotalSupply();
+
+        }
         preserved MorphoTokenOptimismHarness.initialize(address _) with (env e) {
-            // Safe requires because the proxy contract should be initialized right after construction.
+            // Safe require because the proxy contract should be initialized right after construction.
             require totalSupply() == 0;
-            require sumOfVotingPower == 0;
         }
         preserved MorphoTokenEthereumHarness.initialize(address _, address _) with (env e) {
             // Safe requires because the proxy contract should be initialized right after construction.
             require totalSupply() == 0;
-            require sumOfVotingPower == 0;
+            require forall mathint account. sumOfVotes[account] == 0;
         }
+    }
+
+invariant delegatedVotingPowerLTEqTotalVotingPower()
+    forall address a. ghostDelegatedVotingPower[a] <= sumOfVotes[2^160]
+    {
         preserved {
-            requireInvariant totalSupplyIsSumOfBalances();
-            requireInvariant zeroAddressNoVotingPower();
-            requireInvariant balancesLTEqTotalSupply();
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesMonotone();
+            requireInvariant totalSupplyIsSumOfVirtualVotingPower();
         }
     }
 
+invariant sumOfTwoDelegatedVPLTEqTotalVP()
+    forall address a. forall address b. a != b => ghostDelegatedVotingPower[a] + ghostDelegatedVotingPower[b] <= sumOfVotes[2^160]
+    {
+        preserved {
+            requireInvariant delegatedVotingPowerLTEqTotalVotingPower();
+            requireInvariant sumOfVotesStartsAtZero();
+            requireInvariant sumOfVotesGrowsCorrectly();
+            requireInvariant sumOfVotesMonotone();
+            requireInvariant totalSupplyIsSumOfVirtualVotingPower();
+        }
+    }
+
+
 function isTotalSupplyGTEqSumOfVotingPower() returns bool {
     requireInvariant totalSupplyIsSumOfVirtualVotingPower();
-    return totalSupply() >= sumOfVotingPower;
+    return totalSupply() >= sumOfVotes[2^160];
 }
 
 // Check that the total supply of tokens is greater than or equal to the sum of voting power.

From a712cf9f63f88bc4d8dd86cee65e8a97d3658a8a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20=7C=20Morpho=20=F0=9F=A6=8B?= <colin@morpho.xyz>
Date: Mon, 9 Dec 2024 19:52:46 +0100
Subject: [PATCH 14/19] chore: formatting
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com>
Signed-off-by: Colin | Morpho 🦋 <colin@morpho.xyz>
---
 certora/specs/RevertsMintBurnOptimism.spec | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/certora/specs/RevertsMintBurnOptimism.spec b/certora/specs/RevertsMintBurnOptimism.spec
index cfcb818..4e65492 100644
--- a/certora/specs/RevertsMintBurnOptimism.spec
+++ b/certora/specs/RevertsMintBurnOptimism.spec
@@ -12,7 +12,7 @@ rule mintRevertConditions(env e, address to, uint256 amount) {
     mathint totalSupplyBefore = totalSupply();
     uint256 toVotingPowerBefore = delegatedVotingPower(delegatee(to));
 
-    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower .
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower.
     require delegatee(0) == 0;
 
     // Safe require as it is verified in totalSupplyGTEqSumOfVotingPower.
@@ -27,7 +27,7 @@ rule burnRevertConditions(env e, address from, uint256 amount) {
     uint256 balanceOfFromBefore = balanceOf(from);
     uint256 fromVotingPowerBefore = delegatedVotingPower(delegatee(from));
 
-    // Safe require as zero address can't possibly delegate voting power.
+    // Safe require as zero address can't possibly delegate voting power which is verified in zeroAddressNoVotingPower.
     require delegatee(0) == 0;
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.

From de8f6e2206c977080efc8182a7ba459f77ec0e7a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20=7C=20Morpho=20=F0=9F=A6=8B?= <colin@morpho.xyz>
Date: Tue, 10 Dec 2024 14:20:46 +0100
Subject: [PATCH 15/19] docs: apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Colin | Morpho 🦋 <colin@morpho.xyz>
---
 certora/specs/RevertsERC20.spec | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index 22567a4..ac12d3b 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -16,7 +16,7 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
     require senderVotingPowerBefore >= balanceOfSenderBefore;
-    // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance.
+    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP(), delegatedLTEqDelegateeVP() and totalSupplyIsSumOfVirtualVotingPower().
     require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;
 
     transfer@withrevert(e, to, amount);
@@ -33,7 +33,7 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
     require holderVotingPowerBefore >= balanceOfHolderBefore;
 
-    // Safe require because if delegatees are different the recipient's voting power excludes the holder's balance.
+    // Safe require that follows from  sumOfTwoDelegatedVPLTEqTotalVP(), delegatedLTEqDelegateeVP() and totalSupplyIsSumOfVirtualVotingPower().
     require delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;
 
     transferFrom@withrevert(e, from, to, amount);

From 75370ef69778f70d168ff454e7dd6bb1291bff49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 10 Dec 2024 14:28:33 +0100
Subject: [PATCH 16/19] refactor: simplify require statements

---
 certora/specs/RevertsERC20.spec | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index ac12d3b..026f1bf 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -16,8 +16,8 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
     require senderVotingPowerBefore >= balanceOfSenderBefore;
-    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP(), delegatedLTEqDelegateeVP() and totalSupplyIsSumOfVirtualVotingPower().
-    require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore <= totalSupply() - balanceOfSenderBefore;
+    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower().
+    require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + senderVotingPowerBefore <= totalSupply();
 
     transfer@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
@@ -33,11 +33,13 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
     require holderVotingPowerBefore >= balanceOfHolderBefore;
 
-    // Safe require that follows from  sumOfTwoDelegatedVPLTEqTotalVP(), delegatedLTEqDelegateeVP() and totalSupplyIsSumOfVirtualVotingPower().
-    require delegatee(to) != delegatee(from) => recipientVotingPowerBefore <= totalSupply() - balanceOfHolderBefore;
+    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower().
+    require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + holderVotingPowerBefore <= totalSupply();
 
     transferFrom@withrevert(e, from, to, amount);
+
     bool generalRevertConditions = from == 0 || to == 0 || balanceOfHolderBefore < amount || e.msg.value != 0;
+
     if (allowanceOfSenderBefore != max_uint256) {
         assert lastReverted <=>  e.msg.sender == 0 || allowanceOfSenderBefore < amount || generalRevertConditions;
     } else {

From 9a935dd44f6503428181604b55ee6074f46864d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 10 Dec 2024 14:37:35 +0100
Subject: [PATCH 17/19] docs: improve docs

---
 certora/specs/Delegation.spec      | 16 +++++++---------
 certora/specs/ERC20Invariants.spec | 11 ++++++++++-
 2 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec
index a653b08..8f71e75 100644
--- a/certora/specs/Delegation.spec
+++ b/certora/specs/Delegation.spec
@@ -6,16 +6,14 @@ methods {
     function delegationNonce(address) external returns uint256 envfree;
 }
 
-// To reason exhaustively on the value of of delegated voting power we proceed to compute the partial sum of delegated votes to parametre A for each possible address.
-// We call the partial sum of votes to parameter A up to an addrress a, to sum of delegated votes to parameter A for all addresses within the range [0..a[.
-// Formally, we write ∀ a:address, sumsOfVotesDelegatedToA[a] = Σ balanceOf(i), where the sum ranges over addresses i such that i < a and delegatee(i) = A, provided that the address zero holds no voting power and that it never performs transactions.
-// With this approach, we are able to write and check more abstract properties about the computation of the total delegated voting power using universal quantifiers.
-// From this follows the property such that, ∀ a:address, delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A).
-// In particular, we have the equality sumsOfVotesDelegatedToA[2^160] = delegatedVotingPower(A).
-// Finally, we reason by parametricity to observe since we have ∀ a:address, delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A).
-// We also have ∀ A:address, ∀ a:address, A ≠ 0 ∧ delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A), which is what we want to show.
-
 // Ghost variable to hold the sum of voting power.
+// To reason exhaustively on the value of the sum of voting power we proceed to compute the partial sum of voting power for each possible address.
+// We call the partial sum of balances up to an addrress a, to sum of balances for all addresses within the range [0..a[.
+// Formally, we write ∀ a:address, sumOfVotes[a] = Σ delegatedVotingPower(i) where the sum ranges over addresses i < a, provided that the address zero holds no token and that it never performs transactions.
+// With this approach, we are able to write and check more abstract properties about the computation of the total supply of tokens using universal quantifiers.
+// From this follows the property such that, ∀ a:address, delegatedVotingpower(a) ≤ total sum of votes.
+// In particular we have the equality, sumOfVotes[2^160] + _zeroVirtualVotingPower = totalSupply() from which we can deduce that the sum of voting power is lesser than or equal to the totalSupply();
+// and we are able to to show that the sum of two different balances is lesser than or equal to the total sum of votes.
 ghost mapping (mathint => mathint) sumOfVotes {
     init_state axiom forall mathint account. sumOfVotes[account] == 0;
 }
diff --git a/certora/specs/ERC20Invariants.spec b/certora/specs/ERC20Invariants.spec
index e7bd7fe..3a1542b 100644
--- a/certora/specs/ERC20Invariants.spec
+++ b/certora/specs/ERC20Invariants.spec
@@ -13,7 +13,16 @@ persistent ghost address A {
     axiom A != 0;
 }
 
-// Partial sum of delegated votes to parameterized address A.
+// Ghost variable to hold the sum of delegated votes to parameterized address A.
+// To reason exhaustively on the value of of delegated voting power we proceed to compute the partial sum of delegated votes to parametre A for each possible address.
+// We call the partial sum of votes to parameter A up to an addrress a, to sum of delegated votes to parameter A for all addresses within the range [0..a[.
+// Formally, we write ∀ a:address, sumsOfVotesDelegatedToA[a] = Σ balanceOf(i), where the sum ranges over addresses i such that i < a and delegatee(i) = A, provided that the address zero holds no voting power and that it never performs transactions.
+// With this approach, we are able to write and check more abstract properties about the computation of the total delegated voting power using universal quantifiers.
+// From this follows the property such that, ∀ a:address, delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A).
+// In particular, we have the equality sumsOfVotesDelegatedToA[2^160] = delegatedVotingPower(A).
+// Finally, we reason by parametricity to observe since we have ∀ a:address, delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A).
+// We also have ∀ A:address, ∀ a:address, A ≠ 0 ∧ delegatee(a) = A ⇒ balanceOf(a) ≤ delegatedVotingPower(A), which is what we want to show.
+
 // sumOfvotes[x] = \sum_{i=0}^{x-1} balances[i] when delegatee[i] == A;
 ghost mapping(mathint => mathint) sumsOfVotesDelegatedToA {
     init_state axiom forall mathint account. sumsOfVotesDelegatedToA[account] == 0;

From 7ed32541d3d4d087c7109d75d93c940e81a9392a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= <colin@morpho.xyz>
Date: Tue, 10 Dec 2024 14:57:42 +0100
Subject: [PATCH 18/19] fix: typo

---
 certora/specs/RevertsERC20.spec | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index 026f1bf..a8e8d96 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -32,9 +32,8 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
     require holderVotingPowerBefore >= balanceOfHolderBefore;
-
     // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower().
-    require delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + holderVotingPowerBefore <= totalSupply();
+    require delegatee(to) != delegatee(from) => recipientVotingPowerBefore + holderVotingPowerBefore <= totalSupply();
 
     transferFrom@withrevert(e, from, to, amount);
 

From 9da610b65b15812482d41591f7d9978637694622 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Colin=20=7C=20Morpho=20=F0=9F=A6=8B?= <colin@morpho.xyz>
Date: Tue, 10 Dec 2024 16:14:47 +0100
Subject: [PATCH 19/19] docs: apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Quentin Garchery <garchery.quentin@gmail.com>
Signed-off-by: Colin | Morpho 🦋 <colin@morpho.xyz>
---
 certora/specs/Delegation.spec      | 5 ++---
 certora/specs/ERC20Invariants.spec | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec
index 8f71e75..3e081bc 100644
--- a/certora/specs/Delegation.spec
+++ b/certora/specs/Delegation.spec
@@ -10,10 +10,9 @@ methods {
 // To reason exhaustively on the value of the sum of voting power we proceed to compute the partial sum of voting power for each possible address.
 // We call the partial sum of balances up to an addrress a, to sum of balances for all addresses within the range [0..a[.
 // Formally, we write ∀ a:address, sumOfVotes[a] = Σ delegatedVotingPower(i) where the sum ranges over addresses i < a, provided that the address zero holds no token and that it never performs transactions.
-// With this approach, we are able to write and check more abstract properties about the computation of the total supply of tokens using universal quantifiers.
+// With this approach, we are able to write and check more abstract properties about the computation of the total voting power using universal quantifiers.
 // From this follows the property such that, ∀ a:address, delegatedVotingpower(a) ≤ total sum of votes.
-// In particular we have the equality, sumOfVotes[2^160] + _zeroVirtualVotingPower = totalSupply() from which we can deduce that the sum of voting power is lesser than or equal to the totalSupply();
-// and we are able to to show that the sum of two different balances is lesser than or equal to the total sum of votes.
+// In particular, we are able to to show that the sum voting powers of two different accounts is lesser than or equal to the total sum of votes.
 ghost mapping (mathint => mathint) sumOfVotes {
     init_state axiom forall mathint account. sumOfVotes[account] == 0;
 }
diff --git a/certora/specs/ERC20Invariants.spec b/certora/specs/ERC20Invariants.spec
index 3a1542b..17b47bf 100644
--- a/certora/specs/ERC20Invariants.spec
+++ b/certora/specs/ERC20Invariants.spec
@@ -14,7 +14,7 @@ persistent ghost address A {
 }
 
 // Ghost variable to hold the sum of delegated votes to parameterized address A.
-// To reason exhaustively on the value of of delegated voting power we proceed to compute the partial sum of delegated votes to parametre A for each possible address.
+// To reason exhaustively on the value of of delegated voting power we proceed to compute the partial sum of delegated votes to parameter A for each possible address.
 // We call the partial sum of votes to parameter A up to an addrress a, to sum of delegated votes to parameter A for all addresses within the range [0..a[.
 // Formally, we write ∀ a:address, sumsOfVotesDelegatedToA[a] = Σ balanceOf(i), where the sum ranges over addresses i such that i < a and delegatee(i) = A, provided that the address zero holds no voting power and that it never performs transactions.
 // With this approach, we are able to write and check more abstract properties about the computation of the total delegated voting power using universal quantifiers.