diff --git a/certora/specs/Delegation.spec b/certora/specs/Delegation.spec
index 587bc21..a02f278 100644
--- a/certora/specs/Delegation.spec
+++ b/certora/specs/Delegation.spec
@@ -216,28 +216,28 @@ rule delegatingWithSigUpdatesVotingPower(env e, DelegationToken.Delegation deleg
 }
 
 // Check that the updated voting power of a delegatee after a transfer is lesser than or equal to the total supply of tokens.
-rule updatedDelegatedVPLTEqTotalSupply(address from, address to, uint256 amount) {
-    require from != 0;
-
+rule updatedDelegatedVPLTEqTotalSupply(address from, address to) {
+    uint256 balanceOfFromBefore = balanceOf(from);
+    uint256 delegatedVotingPowerDelegateeToBefore = delegatedVotingPower(delegatee(to));
+    uint256 totalSupplyBefore = totalSupply();
     env e;
+
     require e.msg.value == 0;
     require e.msg.sender == from;
 
-    require amount <= balanceOf(from);
+    require from != 0;
     require delegatee(to) != delegatee(from);
 
     requireInvariant sumOfTwoDelegatedVPLTEqTotalVP();
     assert isTotalSupplyGTEqSumOfVotingPower();
 
     // This require avoids an impossible revert as zeroVirtualVotingPower operations comme from munging.
-    require delegatee(from) == 0 => currentContract._zeroVirtualVotingPower >= balanceOf(from);
+    require delegatee(from) == 0 => currentContract._zeroVirtualVotingPower >=  balanceOfFromBefore;
 
-    uint256 delegatedVotingPowerDelegateeToBefore = delegatedVotingPower(delegatee(to));
-    uint256 totalSupplyBefore = totalSupply();
 
     // This invariant can't be required as it's using a parameterized variable.
     // But it is proven by delegatedLTEqDelegateeVP.
-    require delegatee(from) != 0 => delegatedVotingPower(delegatee(from)) >= balanceOf(from);
+    require delegatee(from) != 0 => delegatedVotingPower(delegatee(from)) >= balanceOfFromBefore;
 
     delegate@withrevert(e, from);
 
@@ -245,5 +245,5 @@ rule updatedDelegatedVPLTEqTotalSupply(address from, address to, uint256 amount)
 
     assert delegatee(from) == from;
 
-    assert delegatedVotingPowerDelegateeToBefore + amount <= totalSupplyBefore;
+    assert delegatedVotingPowerDelegateeToBefore + balanceOfFromBefore <= totalSupplyBefore;
 }
diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index 731ba7a..379a93b 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -22,8 +22,7 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
     // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
     require
       e.msg.sender != 0 =>
-      amount <= balanceOfSenderBefore =>
-      delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply();
+      delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + balanceOfSenderBefore <= totalSupply();
 
     transfer@withrevert(e, to, amount);
     assert lastReverted <=> e.msg.sender == 0 || to == 0 || balanceOfSenderBefore < amount || e.msg.value != 0;
@@ -44,8 +43,7 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
     // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
     require
       from != 0 =>
-      amount <= balanceOfHolderBefore =>
-      delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply();
+      delegatee(to) != delegatee(from) => recipientVotingPowerBefore +  balanceOfHolderBefore <= totalSupply();
 
     transferFrom@withrevert(e, from, to, amount);