diff --git a/contracts/lendingpool/LendingPool.sol b/contracts/lendingpool/LendingPool.sol
index 99734898..6afe0219 100644
--- a/contracts/lendingpool/LendingPool.sol
+++ b/contracts/lendingpool/LendingPool.sol
@@ -695,7 +695,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
    * @param asset the address of the reserve
    * @return the reserve normalized income
    */
-  function getReserveNormalizedIncome(address asset) external override view returns (uint256) {
+  function getReserveNormalizedIncome(address asset) external virtual override view returns (uint256) {
     return _reserves[asset].getNormalizedIncome();
   }
 
diff --git a/contracts/tokenization/StableDebtToken.sol b/contracts/tokenization/StableDebtToken.sol
index 29781919..c339317f 100644
--- a/contracts/tokenization/StableDebtToken.sol
+++ b/contracts/tokenization/StableDebtToken.sol
@@ -288,7 +288,7 @@ contract StableDebtToken is IStableDebtToken, DebtTokenBase {
    * @param avgRate the average rate at which calculate the total supply
    * @return The debt balance of the user since the last burn/mint action
    **/
-  function _calcTotalSupply(uint256 avgRate) internal view returns (uint256) {
+  function _calcTotalSupply(uint256 avgRate) internal virtual view returns (uint256) {
     uint256 principalSupply = super.totalSupply();
 
     if (principalSupply == 0) {
diff --git a/runStableTokenCLI.sh b/runStableTokenCLI.sh
new file mode 100644
index 00000000..8903f2f9
--- /dev/null
+++ b/runStableTokenCLI.sh
@@ -0,0 +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
diff --git a/runUserConfigCLI.sh b/runUserConfigCLI.sh
new file mode 100644
index 00000000..f3ddbacc
--- /dev/null
+++ b/runUserConfigCLI.sh
@@ -0,0 +1 @@
+certoraRun specs/harness/UserConfigurationHarness.sol  --solc solc6.8 --verify UserConfigurationHarness:specs/UserConfiguration.spec --settings -useBitVectorTheory --staging master
diff --git a/runVariableTokenCLI.sh b/runVariableTokenCLI.sh
new file mode 100644
index 00000000..483e152e
--- /dev/null
+++ b/runVariableTokenCLI.sh
@@ -0,0 +1 @@
+certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc solc6.8 --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic --cache VariableDebtToken --staging
\ No newline at end of file
diff --git a/specs/StableDebtToken.spec b/specs/StableDebtToken.spec
new file mode 100644
index 00000000..0d6e0c5d
--- /dev/null
+++ b/specs/StableDebtToken.spec
@@ -0,0 +1,155 @@
+methods {
+	getUserLastUpdated(address) returns uint40 envfree
+}
+
+rule integrityTimeStamp(address user, method f) {
+	env e;
+	require sinvoke getIncentivesController(e) == 0;
+	require getUserLastUpdated(user) <= e.block.timestamp;
+	calldataarg arg;
+	sinvoke f(e,arg);
+	assert getUserLastUpdated(user) <= e.block.timestamp;
+}
+
+/**
+TotalSupply is the sum of all users’ balances
+	
+totalSupply(t) = Σaddress u. balanceOf(u,t)
+
+Check that each possible opertaion changes the balance of at most one user
+*/
+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);
+	 
+	calldataarg arg;
+	sinvoke f(e, arg); 
+
+	uint256 balanceAAfter = sinvoke balanceOf(e,a);
+	uint256 balanceBAfter = sinvoke balanceOf(e,b);
+	
+	assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
+}
+
+/**
+Check that the change to total supply is coherent with the changes to balance
+*/
+rule integirtyBalanceOfTotalSupply(address a, method f )
+{
+	env e;
+	require sinvoke getIncentivesController(e) == 0;
+	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);
+	uint256 totalSupplyAfter = sinvoke totalSupply(e);
+
+	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+}
+
+/* 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 totalSupplyBefore = sinvoke totalSupply(e);
+	 
+	uint256 x;
+	sinvoke burn(e, a, x); 
+	uint256 balanceAAfter = sinvoke balanceOf(e,a);
+	uint256 totalSupplyAfter = sinvoke totalSupply(e);
+	if (totalSupplyBefore > x)
+		assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+	else
+		assert  (totalSupplyAfter == 0 );
+}
+
+/**
+Mint inceases the balanceOf user a as expected
+*/
+rule integrityMint(address a, uint256 x) {
+	env e;
+	require sinvoke getIncentivesController(e) == 0;
+	uint256 index;
+	uint256 balancebefore = sinvoke balanceOf(e,a);
+	sinvoke mint(e,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
+
+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,
+and therefore it is currently excluded from the CI.
+*/
+rule additiveMint(address a, uint256 x, uint256 y) {
+	env e;
+	require sinvoke getIncentivesController(e) == 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);
+	
+	uint256 t = x + y;
+	sinvoke mint(e,a, t ,index) at initialStorage;
+	
+	uint256 balanceScenario2 = sinvoke balanceOf(e,a);
+	assert balanceScenario1 == balanceScenario2, "mint is not additive";
+}
+
+rule integrityBurn(address a, uint256 x) {
+	env e;
+	require sinvoke getIncentivesController(e) == 0;
+	uint256 index;
+	uint256 balancebefore = sinvoke balanceOf(e,a);
+	sinvoke burn(e,a,x);
+	
+	uint256 balanceAfter = sinvoke balanceOf(e,a);
+	assert balanceAfter == balancebefore - x;
+}
+
+rule additiveBurn(address a, uint256 x,  uint256 y) {
+	env e;
+	require sinvoke getIncentivesController(e) == 0;
+	storage initialStorage = lastStorage;
+	sinvoke burn(e, a, x);
+	sinvoke burn(e, a, y);
+	uint256 balanceScenario1 = balanceOf(e, a);
+	uint256 t = x + y;
+	sinvoke burn(e, a, t) at initialStorage;
+
+	uint256 balanceScenario2 = balanceOf(e, a);
+	assert balanceScenario1 == balanceScenario2, "burn is not additive";
+}
+
+
+/**
+mint and burn are inverse operations
+Thus, totalSupply is back to initial state
+BalanceOf user is back to initial state */
+rule inverseMintBurn(address a, uint256 x) {
+	env e;
+	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";
+}
+
diff --git a/specs/UserConfiguration.spec b/specs/UserConfiguration.spec
new file mode 100644
index 00000000..14fce3a6
--- /dev/null
+++ b/specs/UserConfiguration.spec
@@ -0,0 +1,66 @@
+methods {
+	setBorrowing(address, uint256, bool) envfree
+	setUsingAsCollateral(address, uint256, bool) envfree
+	isUsingAsCollateralOrBorrowing(address, uint256) returns bool envfree
+	isBorrowing(address, uint256) returns bool envfree
+	isUsingAsCollateral(address, uint256) returns bool envfree
+	isBorrowingAny(address ) returns bool envfree
+ 	isEmpty(address ) returns bool envfree
+}
+
+invariant empty(address user, uint256 reserveIndex ) 
+	 isEmpty(user) => !isBorrowingAny(user) && !isUsingAsCollateralOrBorrowing(user, reserveIndex)
+
+invariant notEmpty(address user, uint256 reserveIndex ) 
+	( isBorrowingAny(user) ||  isUsingAsCollateral(user, reserveIndex)) => !isEmpty(user)
+
+
+invariant borrowing(address user, uint256 reserveIndex ) 
+	 isBorrowing(user, reserveIndex) =>  isBorrowingAny(user) 
+
+invariant collateralOrBorrowing(address user, uint256 reserveIndex ) 
+	( isUsingAsCollateral(user, reserveIndex) ||  isBorrowing(user, reserveIndex) ) <=>  isUsingAsCollateralOrBorrowing(user, reserveIndex) 
+
+
+
+rule setBorrowing(address user, uint256 reserveIndex, bool borrowing)
+{
+	require reserveIndex < 128;
+	
+	setBorrowing(user, reserveIndex, borrowing);
+	assert isBorrowing(user, reserveIndex) == borrowing, "unexpected result";
+}
+
+rule setBorrowingNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing)
+{
+	require reserveIndexOther != reserveIndex;
+	require reserveIndexOther < 128 && reserveIndex < 128;
+	bool otherReserveBorrowing =  isBorrowing(user, reserveIndexOther);
+	bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
+
+	setBorrowing(user, reserveIndex, borrowing);
+	assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
+		otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
+}
+
+
+rule  setUsingAsCollateral(address user, uint256 reserveIndex, bool usingAsCollateral)
+{
+	require reserveIndex < 128;
+	
+	setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
+	assert isUsingAsCollateral(user, reserveIndex) == usingAsCollateral, "unexpected result";
+}
+
+
+rule setUsingAsCollateralNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral)
+{
+	require reserveIndexOther != reserveIndex;
+	require reserveIndexOther < 128 && reserveIndex < 128;
+	bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
+	bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
+	
+	setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
+	assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
+		otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
+}
diff --git a/specs/VariableDebtToken.spec b/specs/VariableDebtToken.spec
new file mode 100644
index 00000000..73e7e39c
--- /dev/null
+++ b/specs/VariableDebtToken.spec
@@ -0,0 +1,173 @@
+using LendingPoolHarnessForVariableDebtToken as POOL
+/**
+TotalSupply is the sum of all users’ balances
+	
+totalSupply(t) = Σaddress u. balanceOf(u,t)
+
+Check that each possible opertaion changes the balance of at most one user
+*/
+rule balanceOfChange(address a, address b, method f)
+{
+	env e;
+	require a!=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);
+	
+	assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
+}
+
+/*
+Check that the changed to total supply is coherent with the changes to balance
+*/
+
+rule integirtyBalanceOfTotalSupply(address a, method f )
+{
+	env e;
+	
+	uint256 balanceABefore = balanceOf(e, a);
+	uint256 totalSupplyBefore = totalSupply(e);
+	 
+	calldataarg arg;
+	sinvoke f(e, arg); 
+	require (f.selector != burn(address, uint256, uint256).selector  &&
+		f.selector != mint(address, uint256, uint256).selector ) ;
+	uint256 balanceAAfter = balanceOf(e, a);
+	uint256 totalSupplyAfter = totalSupply(e);
+
+	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+}
+
+/* Burn behaves deferently and due to accumulation errors might hace less total supply then the balance
+*/
+
+rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f )
+{
+	env e;
+	
+	uint256 balanceABefore = balanceOf(e, a);
+	uint256 totalSupplyBefore = totalSupply(e);
+	 
+	uint256 x;
+	address asset;
+	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
+	sinvoke burn(e, a, x, index); 
+	uint256 balanceAAfter = balanceOf(e, a);
+	uint256 totalSupplyAfter = totalSupply(e);
+	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+}
+
+rule integirtyBalanceOfTotalSupplyOnMint(address a, method f )
+{
+	env e;
+	
+	uint256 balanceABefore = balanceOf(e, a);
+	uint256 totalSupplyBefore = totalSupply(e);
+	 
+	uint256 x;
+	address asset;
+	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
+	sinvoke mint(e, a, x, index); 
+	uint256 balanceAAfter = balanceOf(e, a);
+	uint256 totalSupplyAfter = totalSupply(e);
+	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+}
+
+/**
+Minting an amount of x tokens for user u increases their balance by x, up to rounding errors. 
+{ b= balanceOf(u,t) } 
+mint(u,x,index) 
+{ balanceOf(u,t) = b + x }
+
+*/
+rule integrityMint(address a, uint256 x) {
+	env e;
+	address asset;
+	uint256 index = POOL.getReserveNormalizedVariableDebt(e,asset);
+	uint256 balancebefore = balanceOf(e, a);
+	sinvoke mint(e, a, x, index);
+	
+	uint256 balanceAfter = 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
+*/
+rule additiveMint(address a, uint256 x, uint256 y) {
+	env e;
+	address asset;
+	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
+	storage initialStorage = lastStorage;
+	sinvoke mint(e, a, x, index);
+	sinvoke mint(e, a, y, index);
+	uint256 balanceScenario1 = balanceOf(e, a);
+	uint t = x + y;
+	sinvoke mint(e, a, t ,index) at initialStorage;
+
+	uint256 balanceScenario2 = balanceOf(e, a);
+	assert balanceScenario1 == balanceScenario2, "mint is not additive";
+}
+
+/** 
+Transfer of x amount of tokens from user u  where receiver is user u’
+{bu = balanceOf(u) } 
+	burn(u, u’, x)
+{balanceOf(u) = bu - x } 
+*/
+rule integrityBurn(address a, uint256 x) {
+	env e;
+	address asset;
+	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
+	uint256 balancebefore = balanceOf(e, a);
+	sinvoke burn(e, a, x, index);
+	
+	uint256 balanceAfter = balanceOf(e, a);
+	assert balanceAfter == balancebefore - x;
+}
+/**
+Minting is additive, i.e., it can be performed either all at once or in steps.
+
+burn(u, u’, x); burn(u, u’, y) ~ burn(u, u’, x+y) 
+*/
+rule additiveBurn(address a, uint256 x,  uint256 y) {
+	env e;
+	address asset;
+	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
+	storage initialStorage = lastStorage;
+	sinvoke burn(e, a, x, index);
+	sinvoke burn(e, a, y, index);
+	uint256 balanceScenario1 = balanceOf(e, a);
+	uint t = x + y;
+	sinvoke burn(e, a, t ,index) at initialStorage;
+
+	uint256 balanceScenario2 = balanceOf(e, a);
+	assert balanceScenario1 == balanceScenario2, "burn is not additive";
+}
+
+/**
+Minting and burning are inverse operations.
+
+{bu = balanceOf(u) } 
+mint(u,x); burn(u, u, x) 
+	{balanceOf(u) = bu } 
+*/
+rule inverseMintBurn(address a, uint256 x) {
+	env e;
+	address asset;
+	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
+	uint256 balancebefore = balanceOf(e, a);
+	sinvoke mint(e, a, x, index);
+	sinvoke burn(e, a, x, index);
+	uint256 balanceAfter =  balanceOf(e, a);
+	assert balancebefore == balanceAfter, "burn is not inverse of mint";
+}
+
+
+
diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
new file mode 100644
index 00000000..1fdeffb0
--- /dev/null
+++ b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol
@@ -0,0 +1,198 @@
+pragma solidity ^0.6.8;
+pragma experimental ABIEncoderV2;
+
+import {ReserveConfiguration} from '../../contracts/libraries/configuration/ReserveConfiguration.sol';
+import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
+import {ReserveLogic} from '../../contracts/libraries/logic/ReserveLogic.sol';
+import {ILendingPool} from '../../contracts/interfaces/ILendingPool.sol';
+import {LendingPool} from '../../contracts/lendingpool/LendingPool.sol';
+
+/*
+Certora: Harness that delegates calls to the original LendingPool.
+Used for the verification of the VariableDebtToken contract.
+*/
+contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
+
+  LendingPool private originalPool;
+
+  function deposit(
+    address asset,
+    uint256 amount,
+    address onBehalfOf,
+    uint16 referralCode
+  ) external override {
+    originalPool.deposit(asset, amount, onBehalfOf, referralCode);
+  }
+
+  function withdraw(address asset, uint256 amount) external override {
+    originalPool.withdraw(asset, amount);
+  }
+
+  function getBorrowAllowance(
+    address fromUser,
+    address toUser,
+    address asset,
+    uint256 interestRateMode
+  ) external override view returns (uint256) {
+    return originalPool.getBorrowAllowance(fromUser, toUser, asset, interestRateMode);
+  }
+
+  function delegateBorrowAllowance(
+    address asset,
+    address user,
+    uint256 interestRateMode,
+    uint256 amount
+  ) external override {
+    originalPool.delegateBorrowAllowance(asset, user, interestRateMode, amount);
+  }
+
+  function borrow(
+    address asset,
+    uint256 amount,
+    uint256 interestRateMode,
+    uint16 referralCode,
+    address onBehalfOf
+  ) external override {
+    originalPool.borrow(asset, amount, interestRateMode, referralCode, onBehalfOf);
+  }
+
+  function repay(
+    address asset,
+    uint256 amount,
+    uint256 rateMode,
+    address onBehalfOf
+  ) external override {
+    originalPool.repay(asset, amount, rateMode, onBehalfOf);
+  }
+
+  function swapBorrowRateMode(address asset, uint256 rateMode) external override {
+    originalPool.swapBorrowRateMode(asset, rateMode);
+  }
+
+  function rebalanceStableBorrowRate(address asset, address user) external override {
+    originalPool.rebalanceStableBorrowRate(asset, user);
+  }
+
+  function setUserUseReserveAsCollateral(address asset, bool useAsCollateral) external override {
+    originalPool.setUserUseReserveAsCollateral(asset, useAsCollateral);
+  }
+
+  function liquidationCall(
+    address collateral,
+    address asset,
+    address user,
+    uint256 purchaseAmount,
+    bool receiveAToken
+  ) external override {
+    originalPool.liquidationCall(collateral, asset, user, purchaseAmount, receiveAToken);
+  }
+
+  function getReservesList() external override view returns (address[] memory) {
+    return originalPool.getReservesList();
+  }
+
+  function getReserveData(address asset) external override view returns (ReserveLogic.ReserveData memory) {
+    return originalPool.getReserveData(asset);
+  }
+
+  function getUserConfiguration(address user) external override view returns (UserConfiguration.Map memory) {
+    return originalPool.getUserConfiguration(user);
+  }
+
+  function getUserAccountData(address user)
+  external
+  override
+  view
+  returns (
+    uint256 totalCollateralETH,
+    uint256 totalBorrowsETH,
+    uint256 availableBorrowsETH,
+    uint256 currentLiquidationThreshold,
+    uint256 ltv,
+    uint256 healthFactor
+  )
+  {
+    return originalPool.getUserAccountData(user);
+  }
+
+  function initReserve(
+    address asset,
+    address aTokenAddress,
+    address stableDebtAddress,
+    address variableDebtAddress,
+    address interestRateStrategyAddress
+  ) external override {
+    originalPool.initReserve(asset, aTokenAddress, stableDebtAddress, variableDebtAddress, interestRateStrategyAddress);
+  }
+
+  function setReserveInterestRateStrategyAddress(address asset, address rateStrategyAddress)
+  external
+  override
+  {
+    originalPool.setReserveInterestRateStrategyAddress(asset, rateStrategyAddress);
+  }
+
+  function setConfiguration(address asset, uint256 configuration) external override {
+    originalPool.setConfiguration(asset, configuration);
+  }
+
+  function getConfiguration(address asset)
+  external
+  override
+  view
+  returns (ReserveConfiguration.Map memory)
+  {
+    return originalPool.getConfiguration(asset);
+  }
+
+  mapping(uint256 => uint256) private reserveNormalizedIncome;
+
+  function getReserveNormalizedIncome(address asset) external override view returns (uint256) {
+    require(reserveNormalizedIncome[block.timestamp] == 1e27);
+    return reserveNormalizedIncome[block.timestamp];
+  }
+
+  mapping(uint256 => uint256) private reserveNormalizedVariableDebt;
+
+  function getReserveNormalizedVariableDebt(address asset)
+  external
+  override
+  view
+  returns (uint256)
+  {
+    require(reserveNormalizedVariableDebt[block.timestamp] == 1e27);
+    return reserveNormalizedVariableDebt[block.timestamp];
+  }
+
+  function setPause(bool val) external override {
+    originalPool.setPause(val);
+  }
+
+  function paused() external override view returns (bool) {
+    return originalPool.paused();
+  }
+
+  function flashLoan(
+    address receiver,
+    address[] calldata assets,
+    uint256[] calldata amounts,
+    uint256 mode,
+    address onBehalfOf,
+    bytes calldata params,
+    uint16 referralCode
+  ) external override {
+    originalPool.flashLoan(receiver, assets, amounts, mode, onBehalfOf, params, referralCode);
+  }
+
+  function finalizeTransfer(
+    address asset,
+    address from,
+    address to,
+    uint256 amount,
+    uint256 balanceFromAfter,
+    uint256 balanceToBefore
+  ) external override {
+    originalPool.finalizeTransfer(asset, from, to, amount, balanceFromAfter, balanceToBefore);
+  }
+
+}
diff --git a/specs/harness/StableDebtTokenHarness.sol b/specs/harness/StableDebtTokenHarness.sol
new file mode 100644
index 00000000..d314f8f0
--- /dev/null
+++ b/specs/harness/StableDebtTokenHarness.sol
@@ -0,0 +1,28 @@
+pragma solidity ^0.6.8;
+
+import {StableDebtToken} from '../../contracts/tokenization/StableDebtToken.sol';
+import {IncentivizedERC20} from '../../contracts/tokenization/IncentivizedERC20.sol';
+
+contract StableDebtTokenHarness is StableDebtToken {
+
+    constructor(
+        address pool,
+        address underlyingAsset,
+        string memory name,
+        string memory symbol,
+        address incentivesController
+    ) public StableDebtToken(pool, underlyingAsset, name, symbol, incentivesController) {}
+
+    function balanceOf(address account) public override view returns (uint256) {
+        return IncentivizedERC20.balanceOf(account);
+    }
+
+    function _calcTotalSupply(uint256 avgRate) internal override view returns (uint256) {
+        return IncentivizedERC20.totalSupply();
+    }
+
+    function getIncentivesController() public view returns (address) {
+        return address(_incentivesController);
+    }
+
+}
\ No newline at end of file
diff --git a/specs/harness/UserConfigurationHarness.sol b/specs/harness/UserConfigurationHarness.sol
new file mode 100644
index 00000000..81b2444e
--- /dev/null
+++ b/specs/harness/UserConfigurationHarness.sol
@@ -0,0 +1,77 @@
+pragma solidity ^0.6.8;
+pragma experimental ABIEncoderV2;
+
+import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
+
+/*
+A wrapper contract for calling functions from the library UserConfiguration.
+*/
+contract UserConfigurationHarness {
+
+  	UserConfiguration.Map internal usersConfig;
+
+	function setBorrowing(
+		address user, 
+		uint256 reserveIndex,
+    	bool borrowing
+	) public {
+		UserConfiguration.setBorrowing(usersConfig, reserveIndex, borrowing);
+	}
+
+	function setUsingAsCollateral(
+		address user, 
+		uint256 reserveIndex,
+    	bool _usingAsCollateral
+	) public {
+		UserConfiguration.setUsingAsCollateral(usersConfig, reserveIndex, _usingAsCollateral);
+	}
+
+	function isUsingAsCollateralOrBorrowing(
+		address user, 
+		uint256 reserveIndex)
+    public 
+    view
+    returns (bool) {	
+    	return UserConfiguration.isUsingAsCollateralOrBorrowing(usersConfig, reserveIndex);
+  	}
+
+	function isBorrowing(
+		address user, 
+		uint256 reserveIndex)
+    public 
+    view
+    returns (bool) {	
+    	return UserConfiguration.isBorrowing(usersConfig, reserveIndex);
+  	}
+
+	function isUsingAsCollateral(
+		address user, 
+		uint256 reserveIndex)
+    public 
+    view
+    returns (bool) {	
+    	return UserConfiguration.isUsingAsCollateral(usersConfig, reserveIndex);
+  	}
+
+	function isBorrowingAny(
+		address user)
+    public 
+    view
+    returns (bool) {	
+    	return UserConfiguration.isBorrowingAny(usersConfig);
+  	}
+
+	function isEmpty(
+		address user)
+    public 
+    view
+    returns (bool) {	
+    	return UserConfiguration.isEmpty(usersConfig);
+  	}
+	
+	/*
+		Mimics the original constructor of the contract.
+	*/
+	function init_state() public { }
+}
+