diff --git a/runStableTokenCLI.sh b/runStableTokenCLI.sh
index 8903f2f9..f9d852b3 100644
--- a/runStableTokenCLI.sh
+++ b/runStableTokenCLI.sh
@@ -1 +1 @@
-certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging master
\ No newline at end of file
+certoraRun.py specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --staging
\ No newline at end of file
diff --git a/specs/StableDebtToken.spec b/specs/StableDebtToken.spec
index 0d6e0c5d..16fed3bb 100644
--- a/specs/StableDebtToken.spec
+++ b/specs/StableDebtToken.spec
@@ -14,82 +14,85 @@ rule integrityTimeStamp(address user, method f) {
 /**
 TotalSupply is the sum of all users’ balances
 	
-totalSupply(t) = Σaddress u. balanceOf(u,t)
+totalSupply(t) = Σaddress u. balanceOf(u,t).
 
-Check that each possible opertaion changes the balance of at most one user
+Checks that each possible operation changes the balance of at most one user.
 */
-rule balanceOfChange(address a, address b, method f )
+rule balanceOfChange(address a, address b, method f)
 {
 	env e;
 	require a!=b;
 	require sinvoke getIncentivesController(e) == 0;
-	uint256 balanceABefore = sinvoke balanceOf(e,a);
-	uint256 balanceBBefore = sinvoke balanceOf(e,b);
+	uint256 balanceABefore = sinvoke balanceOf(e, a);
+	uint256 balanceBBefore = sinvoke balanceOf(e, b);
 	 
 	calldataarg arg;
 	sinvoke f(e, arg); 
 
-	uint256 balanceAAfter = sinvoke balanceOf(e,a);
-	uint256 balanceBAfter = sinvoke balanceOf(e,b);
+	uint256 balanceAAfter = sinvoke balanceOf(e, a);
+	uint256 balanceBAfter = sinvoke balanceOf(e, b);
 	
-	assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
+	assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
 }
 
 /**
-Check that the change to total supply is coherent with the changes to balance
+Checks that the change to total supply is coherent with the change to balance due to an operation
+(which is not burn).
 */
 rule integirtyBalanceOfTotalSupply(address a, method f )
 {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
-	uint256 balanceABefore = sinvoke balanceOf(e,a);
+	uint256 balanceABefore = sinvoke balanceOf(e, a);
 	uint256 totalSupplyBefore = sinvoke totalSupply(e);
 	 
 	calldataarg arg;
 	sinvoke f(e, arg); 
-	require (f.selector != burn(address,uint256).selector );
-	uint256 balanceAAfter = sinvoke balanceOf(e,a);
+	require (f.selector != burn(address, uint256).selector);
+	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 totalSupplyAfter = sinvoke totalSupply(e);
 
-	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+	assert  (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
-/* Burn behaves differently and due to accumulation errors might have less total supply than the balance
+/**
+Burn behaves differently and due to accumulation errors might have less total supply than the balance.
 */
 rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f)
 {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
-	uint256 balanceABefore = sinvoke balanceOf(e,a);
+	uint256 balanceABefore = sinvoke balanceOf(e, a);
 	uint256 totalSupplyBefore = sinvoke totalSupply(e);
 	 
 	uint256 x;
 	sinvoke burn(e, a, x); 
-	uint256 balanceAAfter = sinvoke balanceOf(e,a);
+	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 totalSupplyAfter = sinvoke totalSupply(e);
 	if (totalSupplyBefore > x)
-		assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+		assert (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 	else
-		assert  (totalSupplyAfter == 0 );
+		assert (totalSupplyAfter == 0);
 }
 
 /**
-Mint inceases the balanceOf user a as expected
+Mint increases the balanceOf user a as expected.
 */
 rule integrityMint(address a, uint256 x) {
 	env e;
+	address delegatedUser;
 	require sinvoke getIncentivesController(e) == 0;
 	uint256 index;
 	uint256 balancebefore = sinvoke balanceOf(e,a);
-	sinvoke mint(e,a,x,index);
+	sinvoke mint(e, delegatedUser, a, x, index);
 	
 	uint256 balanceAfter = sinvoke balanceOf(e,a);
 	assert balanceAfter == balancebefore+x;
 }
 
 /**
-Mint is additive, can performed either all at once or gradually
-mint(u,x); mint(u,y) ~ mint(u,x+y) at the same timestamp
+Mint is additive, namely it can performed either all at once or gradually:
+mint(u, x); mint(u, y) ~ mint(u, x+y) at the same timestamp.
 
 Note: We assume that the stable rate of the user is 0.
 The case where the rate is non-zero takes much more time to prove,
@@ -97,18 +100,19 @@ and therefore it is currently excluded from the CI.
 */
 rule additiveMint(address a, uint256 x, uint256 y) {
 	env e;
+	address delegatedUser;
 	require sinvoke getIncentivesController(e) == 0;
-	require getUserStableRate(e,a) == 0;
+	require getUserStableRate(e, a) == 0;
 	uint256 index;
 	storage initialStorage = lastStorage;
-	sinvoke mint(e,a,x,index);
-	sinvoke mint(e,a,y,index);
-	uint256 balanceScenario1 = sinvoke balanceOf(e,a);
+	sinvoke mint(e, delegatedUser, a, x, index);
+	sinvoke mint(e, delegatedUser, a, y, index);
+	uint256 balanceScenario1 = sinvoke balanceOf(e, a);
 	
 	uint256 t = x + y;
-	sinvoke mint(e,a, t ,index) at initialStorage;
+	sinvoke mint(e, delegatedUser, a, t ,index) at initialStorage;
 	
-	uint256 balanceScenario2 = sinvoke balanceOf(e,a);
+	uint256 balanceScenario2 = sinvoke balanceOf(e, a);
 	assert balanceScenario1 == balanceScenario2, "mint is not additive";
 }
 
@@ -116,10 +120,10 @@ rule integrityBurn(address a, uint256 x) {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
 	uint256 index;
-	uint256 balancebefore = sinvoke balanceOf(e,a);
+	uint256 balancebefore = sinvoke balanceOf(e, a);
 	sinvoke burn(e,a,x);
 	
-	uint256 balanceAfter = sinvoke balanceOf(e,a);
+	uint256 balanceAfter = sinvoke balanceOf(e, a);
 	assert balanceAfter == balancebefore - x;
 }
 
@@ -139,17 +143,17 @@ rule additiveBurn(address a, uint256 x,  uint256 y) {
 
 
 /**
-mint and burn are inverse operations
-Thus, totalSupply is back to initial state
-BalanceOf user is back to initial state */
+Mint and burn are inverse operations.
+Therefore, both totalSupply and BalanceOf user are back to the initial state.
+*/
 rule inverseMintBurn(address a, uint256 x) {
 	env e;
+	address delegatedUser;
 	require sinvoke getIncentivesController(e) == 0;
 	uint256 index;
-	uint256 balancebefore = sinvoke balanceOf(e,a);
-	sinvoke mint(e,a,x,index);
-	sinvoke burn(e,a,x);
-	uint256 balanceAfter = sinvoke balanceOf(e,a);
-	assert balancebefore == balanceAfter, "burn is not inverse of mint";
-}
-
+	uint256 balancebefore = sinvoke balanceOf(e, a);
+	sinvoke mint(e, delegatedUser, a, x, index);
+	sinvoke burn(e, a, x);
+	uint256 balanceAfter = sinvoke balanceOf(e, a);
+	assert balancebefore == balanceAfter, "burn is not the inverse of mint";
+}
\ No newline at end of file