diff --git a/contracts/deposit_erc20/certora/always-depletable.spec b/contracts/deposit_erc20/certora/always-depletable.spec
new file mode 100644
index 00000000..3edb4d4f
--- /dev/null
+++ b/contracts/deposit_erc20/certora/always-depletable.spec
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: GPL-3.0-only
+import "helper/erc20.spec";
+
+rule always_depletable {
+    env e;
+    
+    require(e.msg.sender != 0);
+    require(e.msg.sender != currentContract);
+    require(e.msg.value == 0);
+    
+    uint amount = currentContract.token.balanceOf(e, currentContract);
+    require(max_uint >= amount + currentContract.token.balanceOf(e, e.msg.sender));
+    require(currentContract.sent + amount <= max_uint);
+    
+    withdraw@withrevert(e, amount);
+        
+    assert !lastReverted;
+    assert (currentContract.token.balanceOf(e, currentContract) == 0);
+}
diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf
new file mode 100644
index 00000000..4b10cb5f
--- /dev/null
+++ b/contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf
@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/always-depletable.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf
new file mode 100644
index 00000000..d41922de
--- /dev/null
+++ b/contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf
@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/deposit-deposit-revert.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf
new file mode 100644
index 00000000..9751a2cf
--- /dev/null
+++ b/contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf
@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/no-deposit-twice.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf
new file mode 100644
index 00000000..da8059d6
--- /dev/null
+++ b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf
@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/wd-contract-bal.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf
new file mode 100644
index 00000000..351be50a
--- /dev/null
+++ b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf
@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/wd-leq-init-bal.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf
new file mode 100644
index 00000000..c0448798
--- /dev/null
+++ b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf
@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/wd-not-revert.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf
new file mode 100644
index 00000000..e0e36cdc
--- /dev/null
+++ b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf
@@ -0,0 +1,10 @@
+{ 
+    "files": [
+        "versions/lib/ERC20v1.sol:ERC20",
+        "versions/DepositERC20_v1.sol:TokenTransfer"
+    ],
+    "verify": "TokenTransfer:certora/wd-sender-rcv.spec",
+    "link": [
+        "TokenTransfer:token=ERC20"
+    ]
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/certora/deposit-deposit-revert.spec b/contracts/deposit_erc20/certora/deposit-deposit-revert.spec
new file mode 100644
index 00000000..f7381f85
--- /dev/null
+++ b/contracts/deposit_erc20/certora/deposit-deposit-revert.spec
@@ -0,0 +1,15 @@
+import "helper/erc20.spec";
+
+rule deposit_deposit_revert {
+    env e1;
+    env e2;
+
+    method f;
+    calldataarg args;
+
+    deposit(e1);
+    f(e2, args);
+    
+    assert f.selector != sig:deposit().selector;
+}
+
diff --git a/contracts/deposit_erc20/certora/getters.sol b/contracts/deposit_erc20/certora/getters.sol
index 4dfe9d7a..8b137891 100644
--- a/contracts/deposit_erc20/certora/getters.sol
+++ b/contracts/deposit_erc20/certora/getters.sol
@@ -1,15 +1 @@
-function getBalance() public view returns (uint) {
-    return token.balanceOf(address(this));
-}
 
-function getAddressBalance(address addr) public view returns (uint) {
-    return token.balanceOf(addr);
-}
-
-function getSent() public view returns (uint) {
-    return sent;
-}
-
-function getInitialDeposit() public view returns (uint) {
-    return initial_deposit;
-}
diff --git a/contracts/deposit_erc20/certora/helper/erc20.spec b/contracts/deposit_erc20/certora/helper/erc20.spec
new file mode 100644
index 00000000..48ba7180
--- /dev/null
+++ b/contracts/deposit_erc20/certora/helper/erc20.spec
@@ -0,0 +1,20 @@
+/***
+ * This spec file adds `DISPATCHER` summaries for the methods in the ERC20
+ * specification.  It is useful for writing specifications that work with
+ * arbitrary ERC20 contracts; if using it, you should add a variety of ERC20
+ * implementations to the scene.
+ *
+ * See [Using DISPATCHER for ERC20 contracts][guide] in the user guide for more
+ * information.
+ *
+ * [guide]: https://docs.certora.com/en/latest/docs/user-guide/multicontract/index.html#using-dispatcher-for-erc20-contracts
+ */
+
+methods {
+    function _.totalSupply()                         external => DISPATCHER(true);
+    function _.balanceOf(address)                    external => DISPATCHER(true);
+    function _.allowance(address,address)            external => DISPATCHER(true);
+    function _.approve(address,uint256)              external => DISPATCHER(true);
+    function _.transfer(address,uint256)             external => DISPATCHER(true);
+    function _.transferFrom(address,address,uint256) external => DISPATCHER(true);
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/certora/methods.spec b/contracts/deposit_erc20/certora/methods.spec
index 23496455..8b137891 100644
--- a/contracts/deposit_erc20/certora/methods.spec
+++ b/contracts/deposit_erc20/certora/methods.spec
@@ -1,7 +1 @@
-methods {
-    function withdraw(uint) external;
-    function getBalance() external returns (uint) envfree;
-    function getAddressBalance(address) external returns (uint) envfree;
-    function getInitialDeposit() external returns (uint) envfree;
-    function getSent() external returns (uint) envfree;
-}
\ No newline at end of file
+
diff --git a/contracts/deposit_erc20/certora/no-deposit-twice.spec b/contracts/deposit_erc20/certora/no-deposit-twice.spec
index 01322b86..9f8a2767 100644
--- a/contracts/deposit_erc20/certora/no-deposit-twice.spec
+++ b/contracts/deposit_erc20/certora/no-deposit-twice.spec
@@ -1,13 +1,11 @@
-rule no_deposit_twice {
-    env e1;
-    env e2;
-
-    method f;
-    calldataarg args;
+persistent ghost bool multiple_deposit {
+    init_state axiom multiple_deposit == false;
+}
 
-    deposit(e1);
-    f(e2, args);
-    
-    assert f.selector != sig:deposit().selector;
+hook Sstore ever_deposited bool value (bool old_value) { 
+    if(old_value && value)
+        multiple_deposit = true;
 }
 
+invariant no_deposit_twice()
+    !multiple_deposit;
\ No newline at end of file
diff --git a/contracts/deposit_erc20/certora/wd-contract-bal.spec b/contracts/deposit_erc20/certora/wd-contract-bal.spec
index 82234866..d2010276 100644
--- a/contracts/deposit_erc20/certora/wd-contract-bal.spec
+++ b/contracts/deposit_erc20/certora/wd-contract-bal.spec
@@ -1,15 +1,20 @@
 // SPDX-License-Identifier: GPL-3.0-only
+import "./helper/erc20.spec";
 
 rule wd_contract_bal {
     env e;
     uint amount;
     mathint mi_amount = amount;
-
-    mathint before = getBalance();
+    mathint before = currentContract.token.balanceOf(e, currentContract);
     require before >= mi_amount;
     
     withdraw(e, amount);
     
-    mathint after = getBalance();
-    assert before == after + mi_amount;
+    mathint after = currentContract.token.balanceOf(e, currentContract);
+    if(e.msg.sender == currentContract) {
+        assert before == after;
+    }
+    else {
+        assert before == after + mi_amount;
+    }
 }
diff --git a/contracts/deposit_erc20/certora/wd-leq-init-bal.spec b/contracts/deposit_erc20/certora/wd-leq-init-bal.spec
index 68ca22fc..7a1921e9 100644
--- a/contracts/deposit_erc20/certora/wd-leq-init-bal.spec
+++ b/contracts/deposit_erc20/certora/wd-leq-init-bal.spec
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: GPL-3.0-only
+import "helper/erc20.spec";
 
 invariant wd_leq_init_bal()
-    getSent() <= getInitialDeposit();
+    currentContract.sent <= currentContract.initial_deposit;
diff --git a/contracts/deposit_erc20/certora/wd-not-revert.spec b/contracts/deposit_erc20/certora/wd-not-revert.spec
new file mode 100644
index 00000000..fcbe3663
--- /dev/null
+++ b/contracts/deposit_erc20/certora/wd-not-revert.spec
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: GPL-3.0-only
+import "helper/erc20.spec";
+
+rule wd_not_revert {
+    env e;
+    uint amount;
+    uint before = currentContract.token.balanceOf(e, currentContract);
+    
+    require(e.msg.sender != 0);
+    require(e.msg.value == 0);
+
+    require(max_uint >= amount + currentContract.token.balanceOf(e, e.msg.sender));
+    require(currentContract.sent + amount + before <= max_uint);
+    require(amount <= before);
+
+    withdraw@withrevert(e, amount);
+    
+    assert !lastReverted;
+}
diff --git a/contracts/deposit_erc20/certora/wd-sender-rcv.spec b/contracts/deposit_erc20/certora/wd-sender-rcv.spec
new file mode 100644
index 00000000..096d28d3
--- /dev/null
+++ b/contracts/deposit_erc20/certora/wd-sender-rcv.spec
@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: GPL-3.0-only
+import "helper/erc20.spec";
+
+rule wd_sender_rcv {
+    env e;
+    uint amount;
+    address sender = e.msg.sender;
+
+    mathint before = currentContract.token.balanceOf(e, sender);
+    withdraw(e, amount);
+    mathint after = currentContract.token.balanceOf(e, sender);
+
+    if(e.msg.sender != currentContract)
+        assert after == before + amount;
+    else
+        assert after == before;
+}
diff --git a/contracts/deposit_erc20/ground-truth.csv b/contracts/deposit_erc20/ground-truth.csv
index 0c7e695a..9ba73c97 100644
--- a/contracts/deposit_erc20/ground-truth.csv
+++ b/contracts/deposit_erc20/ground-truth.csv
@@ -1,7 +1,8 @@
 property,version,truth,footnote-md
+always-depletable,v1,1,
+deposit-deposit-revert,v1,1,
 no-deposit-twice,v1,1,
-no-deposit-twice,v2,1,
 wd-leq-init-bal,v1,0,"This property should not hold for ERC20 tokens, since one can easily increase the contract balance without the contract being able to notice or prevent it. Since this is also possible with ETH (via coinbase or `selfdestruct` transactions), the behavior is comparable for the purposes of these tests."
-wd-leq-init-bal,v2,0,
 wd-contract-bal,v1,1,
-wd-contract-bal,v2,1,
\ No newline at end of file
+wd-not-revert,v1,1
+wd-sender-rcv,v1,1
\ No newline at end of file
diff --git a/contracts/deposit_erc20/hardhat/DepositERC20.sol b/contracts/deposit_erc20/hardhat/DepositERC20.sol
new file mode 100644
index 00000000..2a5865be
--- /dev/null
+++ b/contracts/deposit_erc20/hardhat/DepositERC20.sol
@@ -0,0 +1,54 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity >= 0.8.2;
+
+import "./ERC20v1.sol";
+
+/// @custom:version conformant to specification.
+contract TokenTransfer {
+    ERC20 token;
+    bool ever_deposited;
+
+    uint private sent;
+    uint initial_deposit;
+
+    // ghost variables
+    uint _count_deposit;
+
+    constructor(ERC20 token_) {
+        token = token_;
+    }
+
+    function deposit() public {
+        require(!ever_deposited);
+
+        ever_deposited = true;
+        uint allowance = token.allowance(msg.sender, address(this));
+        token.transferFrom(msg.sender, address(this), allowance);
+
+        initial_deposit = token.totalSupply();
+
+        _count_deposit += 1;	
+    }
+
+    function withdraw(uint amount) public {
+        sent += amount;
+        token.transfer(msg.sender, amount);
+    }
+    
+    function getBalance() public view returns (uint) {
+        return token.balanceOf(address(this));
+    }
+
+    function getAddressBalance(address addr) public view returns (uint) {
+        return token.balanceOf(addr);
+    }
+
+    function getSent() public view returns (uint) {
+        return sent;
+    }
+
+    function getInitialDeposit() public view returns (uint) {
+        return initial_deposit;
+    }
+
+}
diff --git a/contracts/deposit_erc20/hardhat/ERC20v1.sol b/contracts/deposit_erc20/hardhat/ERC20v1.sol
new file mode 100644
index 00000000..db15e7a2
--- /dev/null
+++ b/contracts/deposit_erc20/hardhat/ERC20v1.sol
@@ -0,0 +1,118 @@
+// SPDX-License-Identifier: MIT
+pragma solidity >= 0.8.2;
+
+import "./IERC20.sol";
+
+/**
+ * @dev Implementation of the {IERC20} interface.
+ *
+ */
+contract ERC20 is IERC20 {
+    mapping(address => uint256) private _balances;
+    uint256 private _totalSupply;
+
+    constructor(uint256 amount) {
+        _totalSupply += amount;
+	    _balances[msg.sender] += amount;
+    }
+
+    function totalSupply() public view returns (uint256) {
+        return _totalSupply;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return _balances[account];
+    }
+
+    /**
+     * Requirements:
+     * - `to` cannot be the zero address.
+     * - the caller must have a balance of at least `amount`.
+     */
+    function transfer(address to, uint256 amount) public returns (bool) {
+        _transfer(msg.sender, to, amount);
+        return true;
+    }
+
+    function allowance(address owner, address spender) public view returns (uint256) {
+        require (owner != address(0));
+	require (spender != address(0));
+	return _balances[owner];
+    }
+
+    /**
+     * NOTE: If `amount` is the maximum `uint256`, the allowance is not updated on
+     * `transferFrom`. This is semantically equivalent to an infinite approval.
+     *
+     * Requirements:
+     * - `spender` cannot be the zero address.
+     */
+    function approve(address spender, uint256 amount) public view returns (bool) {
+        _approve(msg.sender, spender, amount);
+        return true;
+    }
+
+    /**
+     * @dev See {IERC20-transferFrom}.
+     *
+     *
+     * NOTE: Does not update the allowance if the current allowance
+     * is the maximum `uint256`.
+     *
+     * Requirements:
+     *
+     * - `from` and `to` cannot be the zero address.
+     * - `from` must have a balance of at least `amount`.
+     * - the caller must have allowance for ``from``'s tokens of at least
+     * `amount`.
+     */
+    function transferFrom(address from, address to, uint256 amount) public returns (bool) {
+        _spendAllowance(from, msg.sender, amount);
+        _transfer(from, to, amount);
+        return true;
+    }
+
+    function _transfer(address from, address to, uint256 amount) internal {
+        require (from != address(0));
+	require (to != address(0));
+
+	uint256 fromBalance = _balances[from];
+	require (fromBalance >= amount);
+	// unchecked {
+	// Overflow not possible: amount <= fromBalance <= totalSupply.
+	_balances[from] = fromBalance - amount;
+	// Overflow not possible: balance + amount is at most totalSupply, which we know fits into a uint256.
+	_balances[to] += amount;
+	// }
+    }
+
+    /**
+     * @dev Sets `amount` as the allowance of `spender` over the `owner` s tokens.
+     *
+     * This internal function is equivalent to `approve`, and can be used to
+     * e.g. set automatic allowances for certain subsystems, etc.
+     *
+     * Requirements:
+     *
+     * - `owner` cannot be the zero address.
+     * - `spender` cannot be the zero address.
+     */
+    function _approve(address owner, address spender, uint256 amount) internal pure {
+        require (owner != address(0));
+	require (spender != address(0));
+	require (amount >= 0);
+    }
+
+    /**
+     * @dev Updates `owner` s allowance for `spender` based on spent `amount`.
+     *
+     * Does not update the allowance amount in case of infinite allowance.
+     * Revert if not enough allowance is available.
+     *
+     */
+    function _spendAllowance(address owner, address spender, uint256 amount) internal view {
+        uint256 currentAllowance = allowance(owner, spender);
+        require (currentAllowance >= amount);
+	_approve(owner, spender, currentAllowance);
+    }
+}
diff --git a/contracts/deposit_erc20/hardhat/IERC20.sol b/contracts/deposit_erc20/hardhat/IERC20.sol
new file mode 100644
index 00000000..66c4e4d8
--- /dev/null
+++ b/contracts/deposit_erc20/hardhat/IERC20.sol
@@ -0,0 +1,78 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts (last updated v4.6.0) (token/ERC20/IERC20.sol)
+
+pragma solidity ^0.8.0;
+
+/**
+ * @dev Interface of the ERC20 standard as defined in the EIP.
+ */
+interface IERC20 {
+    /**
+     * @dev Emitted when `value` tokens are moved from one account (`from`) to
+     * another (`to`).
+     *
+     * Note that `value` may be zero.
+     */
+    event Transfer(address indexed from, address indexed to, uint256 value);
+
+    /**
+     * @dev Emitted when the allowance of a `spender` for an `owner` is set by
+     * a call to {approve}. `value` is the new allowance.
+     */
+    event Approval(address indexed owner, address indexed spender, uint256 value);
+
+    /**
+     * @dev Returns the amount of tokens in existence.
+     */
+    function totalSupply() external view returns (uint256);
+
+    /**
+     * @dev Returns the amount of tokens owned by `account`.
+     */
+    function balanceOf(address account) external view returns (uint256);
+
+    /**
+     * @dev Moves `amount` tokens from the caller's account to `to`.
+     *
+     * Returns a boolean value indicating whether the operation succeeded.
+     *
+     * Emits a {Transfer} event.
+     */
+    function transfer(address to, uint256 amount) external returns (bool);
+
+    /**
+     * @dev Returns the remaining number of tokens that `spender` will be
+     * allowed to spend on behalf of `owner` through {transferFrom}. This is
+     * zero by default.
+     *
+     * This value changes when {approve} or {transferFrom} are called.
+     */
+    function allowance(address owner, address spender) external view returns (uint256);
+
+    /**
+     * @dev Sets `amount` as the allowance of `spender` over the caller's tokens.
+     *
+     * Returns a boolean value indicating whether the operation succeeded.
+     *
+     * IMPORTANT: Beware that changing an allowance with this method brings the risk
+     * that someone may use both the old and the new allowance by unfortunate
+     * transaction ordering. One possible solution to mitigate this race
+     * condition is to first reduce the spender's allowance to 0 and set the
+     * desired value afterwards:
+     * https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729
+     *
+     * Emits an {Approval} event.
+     */
+    function approve(address spender, uint256 amount) external returns (bool);
+
+    /**
+     * @dev Moves `amount` tokens from `from` to `to` using the
+     * allowance mechanism. `amount` is then deducted from the caller's
+     * allowance.
+     *
+     * Returns a boolean value indicating whether the operation succeeded.
+     *
+     * Emits a {Transfer} event.
+     */
+    function transferFrom(address from, address to, uint256 amount) external returns (bool);
+}
diff --git a/contracts/deposit_erc20/hardhat/test.js b/contracts/deposit_erc20/hardhat/test.js
new file mode 100644
index 00000000..f0c7dddf
--- /dev/null
+++ b/contracts/deposit_erc20/hardhat/test.js
@@ -0,0 +1,29 @@
+const {
+    loadFixture,
+  } = require("@nomicfoundation/hardhat-toolbox/network-helpers");
+  const { expect } = require("chai");
+  
+  describe("DepositERC20_v1", function() {
+    async function deployContractv1() {
+      const [receiver] = await ethers.getSigners();
+  
+      const ERC20Factory = await ethers.getContractFactory("ERC20");
+      const ERC20 = await ERC20Factory.deploy(100);
+      const DepositERC20Factory = await ethers.getContractFactory("TokenTransfer");
+      const DepositERC20 = await DepositERC20Factory.deploy(ERC20.getAddress());
+  
+      return { DepositERC20, ERC20, receiver };
+    }
+      it("wd-leq-init-bal: the overall withdrawn amount exceed the initial deposit", async function(){
+        const { DepositERC20, ERC20, receiver } = await loadFixture(deployContractv1);
+        await DepositERC20.deposit();
+
+        await DepositERC20.connect(receiver).withdraw(100);
+        await ERC20.connect(receiver).transfer(DepositERC20, 100);
+        await DepositERC20.connect(receiver).withdraw(100);
+
+        expect(await DepositERC20.getSent()).to.be.equal(200);  
+
+
+      })
+  })
diff --git a/contracts/deposit_erc20/skeleton.json b/contracts/deposit_erc20/skeleton.json
index 44730c30..9816c696 100644
--- a/contracts/deposit_erc20/skeleton.json
+++ b/contracts/deposit_erc20/skeleton.json
@@ -2,8 +2,12 @@
     "name": "Deposit (ERC20)",
     "specification": "file:spec.md",
     "properties": {
+        "always-depletable": "anyone at any time can fire a transaction to receive the full balance of the contract.",
+        "deposit-deposit-revert": "if `deposit` is called after `deposit` the second call aborts.",
         "no-deposit-twice": "`deposit` can only be called once.",
         "wd-leq-init-bal": "the overall withdrawn amount does not exceed the initial deposit.",
-        "wd-contract-bal": "the contract token balance is decreased by `amount` after a successful `withdraw(amount)`."
-     }
+        "wd-contract-bal": "the contract token balance is decreased by `amount` after a successful `withdraw(amount)`.",
+        "wd-not-revert": "a transaction `withdraw(amount)` is not reverted whenever the `amount` does not exceed the contract balance.",
+        "wd-sender-rcv": "after a successful `withdraw(amount)`, the balance of the transaction sender is increased by `amount`."
+    }
 }
diff --git a/contracts/deposit_erc20/solcmc/Makefile b/contracts/deposit_erc20/solcmc/Makefile
index 1cca6c11..6ed4dd8f 100644
--- a/contracts/deposit_erc20/solcmc/Makefile
+++ b/contracts/deposit_erc20/solcmc/Makefile
@@ -39,7 +39,7 @@ $(CM): $(GROUND_TRUTH) $(OUT)
 
 $(OUT): setup $(PROPERTIES_FILES) $(VERSIONS_FILES)
 	@echo "Running SolCMC ($(solver)) experiments..."
-	@$(PYTHON) ../../../scripts/run_solcmc.py --contracts $(CONTRACTS_DIR) --output $(OUTPUT_DIR) --timeout $(to) --solver $(solver)
+	@$(PYTHON) ../../../scripts/run_solcmc.py --contracts $(CONTRACTS_DIR)/ --output $(OUTPUT_DIR) --timeout $(to) --solver $(solver)
 
 one: setup
 	@$(PYTHON) ../../../scripts/run_solcmc.py --contracts $(contract) --timeout $(to)
@@ -64,4 +64,5 @@ $(LIB_DIR):
 
 #---------------------------- CLEAN ------------------------------#
 clean:
-	rm -rf $(BUILD_DIR)
+	@echo "Deleting \"solcmc/build/\"..."
+	@rm -rf $(BUILD_DIR)
diff --git a/contracts/deposit_erc20/solcmc/no-deposit-twice.sol b/contracts/deposit_erc20/solcmc/no-deposit-twice.sol
index 75b7a90b..1e569b44 100644
--- a/contracts/deposit_erc20/solcmc/no-deposit-twice.sol
+++ b/contracts/deposit_erc20/solcmc/no-deposit-twice.sol
@@ -1,4 +1,4 @@
-    // p1
-    function invariant() public view {
-        assert(_count_deposit <= 1);
-    }
+function invariant() public view {
+    assert(_count_deposit <= 1);
+}
+
diff --git a/contracts/deposit_erc20/solcmc/wd-contract-bal.sol b/contracts/deposit_erc20/solcmc/wd-contract-bal.sol
index 1a16ee30..0772bf6a 100644
--- a/contracts/deposit_erc20/solcmc/wd-contract-bal.sol
+++ b/contracts/deposit_erc20/solcmc/wd-contract-bal.sol
@@ -6,4 +6,4 @@ function invariant(uint amount) public {
     uint new_balance = token.balanceOf(address(this));
 
     assert(new_balance == old_balance - amount);
-}
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/versions/DepositERC20_v1.sol b/contracts/deposit_erc20/versions/DepositERC20_v1.sol
index e748c98d..23c78374 100644
--- a/contracts/deposit_erc20/versions/DepositERC20_v1.sol
+++ b/contracts/deposit_erc20/versions/DepositERC20_v1.sol
@@ -27,11 +27,12 @@ contract TokenTransfer {
 
         initial_deposit = token.totalSupply();
 
-        _count_deposit += 1;	
+        _count_deposit += 1;
     }
 
     function withdraw(uint amount) public {
         sent += amount;
         token.transfer(msg.sender, amount);
     }
-}
+
+}
\ No newline at end of file
diff --git a/contracts/deposit_erc20/versions/DepositERC20_v2.sol b/contracts/deposit_erc20/versions/DepositERC20_v2.sol
deleted file mode 100644
index f3cb563a..00000000
--- a/contracts/deposit_erc20/versions/DepositERC20_v2.sol
+++ /dev/null
@@ -1,40 +0,0 @@
-// SPDX-License-Identifier: UNLICENSED
-pragma solidity >= 0.8.2;
-
-import "./lib/IERC20.sol";
-import "./lib/SafeERC20.sol";
-
-/// @custom:version safe IERC20 interactions by using [SafeERC20.sol](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/v4.8.3/contracts/token/ERC20/utils/SafeERC20.sol) (OpenZeppelin)
-contract TokenTransfer {
-    using SafeERC20 for IERC20;
-
-    IERC20 token;
-    bool ever_deposited;
-    
-    uint private sent;
-    uint initial_deposit;
-
-    // ghost variables
-    uint _count_deposit;
-
-    constructor(IERC20 token_) {
-        token = token_;
-    }
-
-    function deposit() public {
-        require(!ever_deposited);
-
-        ever_deposited = true;
-        uint allowance = token.allowance(msg.sender, address(this));
-        token.safeTransferFrom(msg.sender, address(this), allowance);
-
-        initial_deposit = token.totalSupply();
-    
-        _count_deposit += 1;	
-    }
-
-    function withdraw(uint amount) public {
-        sent += amount;
-        token.safeTransfer(msg.sender, amount);
-    }
-}
diff --git a/contracts/deposit_erc20/versions/lib/ERC20v1.sol b/contracts/deposit_erc20/versions/lib/ERC20v1.sol
new file mode 100644
index 00000000..db15e7a2
--- /dev/null
+++ b/contracts/deposit_erc20/versions/lib/ERC20v1.sol
@@ -0,0 +1,118 @@
+// SPDX-License-Identifier: MIT
+pragma solidity >= 0.8.2;
+
+import "./IERC20.sol";
+
+/**
+ * @dev Implementation of the {IERC20} interface.
+ *
+ */
+contract ERC20 is IERC20 {
+    mapping(address => uint256) private _balances;
+    uint256 private _totalSupply;
+
+    constructor(uint256 amount) {
+        _totalSupply += amount;
+	    _balances[msg.sender] += amount;
+    }
+
+    function totalSupply() public view returns (uint256) {
+        return _totalSupply;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return _balances[account];
+    }
+
+    /**
+     * Requirements:
+     * - `to` cannot be the zero address.
+     * - the caller must have a balance of at least `amount`.
+     */
+    function transfer(address to, uint256 amount) public returns (bool) {
+        _transfer(msg.sender, to, amount);
+        return true;
+    }
+
+    function allowance(address owner, address spender) public view returns (uint256) {
+        require (owner != address(0));
+	require (spender != address(0));
+	return _balances[owner];
+    }
+
+    /**
+     * NOTE: If `amount` is the maximum `uint256`, the allowance is not updated on
+     * `transferFrom`. This is semantically equivalent to an infinite approval.
+     *
+     * Requirements:
+     * - `spender` cannot be the zero address.
+     */
+    function approve(address spender, uint256 amount) public view returns (bool) {
+        _approve(msg.sender, spender, amount);
+        return true;
+    }
+
+    /**
+     * @dev See {IERC20-transferFrom}.
+     *
+     *
+     * NOTE: Does not update the allowance if the current allowance
+     * is the maximum `uint256`.
+     *
+     * Requirements:
+     *
+     * - `from` and `to` cannot be the zero address.
+     * - `from` must have a balance of at least `amount`.
+     * - the caller must have allowance for ``from``'s tokens of at least
+     * `amount`.
+     */
+    function transferFrom(address from, address to, uint256 amount) public returns (bool) {
+        _spendAllowance(from, msg.sender, amount);
+        _transfer(from, to, amount);
+        return true;
+    }
+
+    function _transfer(address from, address to, uint256 amount) internal {
+        require (from != address(0));
+	require (to != address(0));
+
+	uint256 fromBalance = _balances[from];
+	require (fromBalance >= amount);
+	// unchecked {
+	// Overflow not possible: amount <= fromBalance <= totalSupply.
+	_balances[from] = fromBalance - amount;
+	// Overflow not possible: balance + amount is at most totalSupply, which we know fits into a uint256.
+	_balances[to] += amount;
+	// }
+    }
+
+    /**
+     * @dev Sets `amount` as the allowance of `spender` over the `owner` s tokens.
+     *
+     * This internal function is equivalent to `approve`, and can be used to
+     * e.g. set automatic allowances for certain subsystems, etc.
+     *
+     * Requirements:
+     *
+     * - `owner` cannot be the zero address.
+     * - `spender` cannot be the zero address.
+     */
+    function _approve(address owner, address spender, uint256 amount) internal pure {
+        require (owner != address(0));
+	require (spender != address(0));
+	require (amount >= 0);
+    }
+
+    /**
+     * @dev Updates `owner` s allowance for `spender` based on spent `amount`.
+     *
+     * Does not update the allowance amount in case of infinite allowance.
+     * Revert if not enough allowance is available.
+     *
+     */
+    function _spendAllowance(address owner, address spender, uint256 amount) internal view {
+        uint256 currentAllowance = allowance(owner, spender);
+        require (currentAllowance >= amount);
+	_approve(owner, spender, currentAllowance);
+    }
+}
diff --git a/contracts/deposit_erc20/versions/lib/ERC20v2.sol b/contracts/deposit_erc20/versions/lib/ERC20v2.sol
new file mode 100644
index 00000000..a8a5c839
--- /dev/null
+++ b/contracts/deposit_erc20/versions/lib/ERC20v2.sol
@@ -0,0 +1,130 @@
+// SPDX-License-Identifier: MIT
+pragma solidity >= 0.8.2;
+
+import "./IERC20.sol";
+
+/**
+ * @dev Implementation of the {IERC20} interface with bugged transfer.
+ *
+ */
+contract ERC20v2 is IERC20 {
+    mapping(address => uint256) private _balances;
+    mapping(address => mapping(address => bool)) private _allowances;    
+    uint256 private _totalSupply;
+
+    constructor(uint256 amount) {
+        _totalSupply += amount;
+	_balances[msg.sender] += amount;
+    }
+
+    function totalSupply() public view returns (uint256) {
+        return _totalSupply;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return _balances[account];
+    }
+
+    /**
+     * Requirements:
+     * - `to` cannot be the zero address.
+     * - the caller must have a balance of at least `amount`.
+     */
+    function transfer(address to, uint256 amount) public returns (bool) {
+        _transfer(msg.sender, to, amount);
+        return true;
+    }
+
+    function allowance(address owner, address spender) public view returns (uint256) {
+	if (_allowances[owner][spender]) {
+		return type(uint256).max;
+	}
+	else {
+	    return 0;
+	}
+    }
+
+    /**
+     * NOTE: If `amount` is the maximum `uint256`, the allowance is not updated on
+     * `transferFrom`. This is semantically equivalent to an infinite approval.
+     *
+     * Requirements:
+     * - `spender` cannot be the zero address.
+     */
+    function approve(address spender, uint256 amount) public returns (bool) {
+        _approve(msg.sender, spender, amount);
+        return true;
+    }
+
+    /**
+     * @dev See {IERC20-transferFrom}.
+     *
+     *
+     * NOTE: Does not update the allowance if the current allowance
+     * is the maximum `uint256`.
+     *
+     * Requirements:
+     *
+     * - `from` and `to` cannot be the zero address.
+     * - `from` must have a balance of at least `amount`.
+     * - the caller must have allowance for ``from``'s tokens of at least
+     * `amount`.
+     */
+    function transferFrom(address from, address to, uint256 amount) public returns (bool) {
+        _spendAllowance(from, msg.sender, amount);
+        _transfer(from, to, amount);
+        return true;
+    }
+
+    function _transfer(address from, address to, uint256 amount) internal {
+        require (from != address(0));
+	require (to != address(0));
+
+	uint256 fromBalance = _balances[from];
+	require (fromBalance >= amount);
+	// unchecked {
+	// Overflow not possible: amount <= fromBalance <= totalSupply.
+	_balances[from] = fromBalance - amount;
+	// Overflow not possible: balance + amount is at most totalSupply, which we know fits into a uint256.
+	_balances[to] += amount - 1;
+	// }
+    }
+
+    /**
+     * @dev Sets `amount` as the allowance of `spender` over the `owner` s tokens.
+     *
+     * This internal function is equivalent to `approve`, and can be used to
+     * e.g. set automatic allowances for certain subsystems, etc.
+     *
+     * Requirements:
+     *
+     * - `owner` cannot be the zero address.
+     * - `spender` cannot be the zero address.
+     */
+    function _approve(address owner, address spender, uint256 amount) internal {
+        require (owner != address(0));
+	require (spender != address(0));
+	require (amount == type(uint256).max);
+	if (amount > 0) {
+	    _allowances[owner][spender] = true;
+	}
+	else {
+	    _allowances[owner][spender] = false;
+	}
+    }
+
+    /**
+     * @dev Updates `owner` s allowance for `spender` based on spent `amount`.
+     *
+     * Does not update the allowance amount in case of infinite allowance.
+     * Revert if not enough allowance is available.
+     *
+     */
+    function _spendAllowance(address owner, address spender, uint256 amount) internal {
+        uint256 currentAllowance = allowance(owner, spender);
+        require (currentAllowance >= amount);
+	// unchecked {
+	_approve(owner, spender, currentAllowance - amount);
+	// }
+    }
+}
diff --git a/contracts/deposit_erc20/versions/lib/IERC20.sol b/contracts/deposit_erc20/versions/lib/IERC20.sol
new file mode 100644
index 00000000..66c4e4d8
--- /dev/null
+++ b/contracts/deposit_erc20/versions/lib/IERC20.sol
@@ -0,0 +1,78 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts (last updated v4.6.0) (token/ERC20/IERC20.sol)
+
+pragma solidity ^0.8.0;
+
+/**
+ * @dev Interface of the ERC20 standard as defined in the EIP.
+ */
+interface IERC20 {
+    /**
+     * @dev Emitted when `value` tokens are moved from one account (`from`) to
+     * another (`to`).
+     *
+     * Note that `value` may be zero.
+     */
+    event Transfer(address indexed from, address indexed to, uint256 value);
+
+    /**
+     * @dev Emitted when the allowance of a `spender` for an `owner` is set by
+     * a call to {approve}. `value` is the new allowance.
+     */
+    event Approval(address indexed owner, address indexed spender, uint256 value);
+
+    /**
+     * @dev Returns the amount of tokens in existence.
+     */
+    function totalSupply() external view returns (uint256);
+
+    /**
+     * @dev Returns the amount of tokens owned by `account`.
+     */
+    function balanceOf(address account) external view returns (uint256);
+
+    /**
+     * @dev Moves `amount` tokens from the caller's account to `to`.
+     *
+     * Returns a boolean value indicating whether the operation succeeded.
+     *
+     * Emits a {Transfer} event.
+     */
+    function transfer(address to, uint256 amount) external returns (bool);
+
+    /**
+     * @dev Returns the remaining number of tokens that `spender` will be
+     * allowed to spend on behalf of `owner` through {transferFrom}. This is
+     * zero by default.
+     *
+     * This value changes when {approve} or {transferFrom} are called.
+     */
+    function allowance(address owner, address spender) external view returns (uint256);
+
+    /**
+     * @dev Sets `amount` as the allowance of `spender` over the caller's tokens.
+     *
+     * Returns a boolean value indicating whether the operation succeeded.
+     *
+     * IMPORTANT: Beware that changing an allowance with this method brings the risk
+     * that someone may use both the old and the new allowance by unfortunate
+     * transaction ordering. One possible solution to mitigate this race
+     * condition is to first reduce the spender's allowance to 0 and set the
+     * desired value afterwards:
+     * https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729
+     *
+     * Emits an {Approval} event.
+     */
+    function approve(address spender, uint256 amount) external returns (bool);
+
+    /**
+     * @dev Moves `amount` tokens from `from` to `to` using the
+     * allowance mechanism. `amount` is then deducted from the caller's
+     * allowance.
+     *
+     * Returns a boolean value indicating whether the operation succeeded.
+     *
+     * Emits a {Transfer} event.
+     */
+    function transferFrom(address from, address to, uint256 amount) external returns (bool);
+}