diff --git a/contracts/simplified_deflationary_token/Makefile b/contracts/simplified_deflationary_token/Makefile
new file mode 100755
index 00000000..38e75235
--- /dev/null
+++ b/contracts/simplified_deflationary_token/Makefile
@@ -0,0 +1,61 @@
+SOLCMC_DIR = ./solcmc
+SOLCMC_BUILD_DIR = $(SOLCMC_DIR)/build
+SOLCMC_Z3_TABLE = $(SOLCMC_BUILD_DIR)/z3/table.md
+SOLCMC_ELD_TABLE = $(SOLCMC_BUILD_DIR)/eld/table.md
+
+CERTORA_DIR = ./certora
+CERTORA_BUILD_DIR = $(CERTORA_DIR)/build
+CERTORA_TABLE = $(CERTORA_BUILD_DIR)/table.md
+
+VERSIONS_DIR = ./versions
+SKELETON = ./skeleton.json
+GROUND_TRUTH = ./ground-truth.csv
+README = README.md
+
+PYTHON = python
+
+.PHONY: all certora solcmc plain clean cleanr clean-solcmc clean-certora
+
+all: plain solcmc certora
+	@echo "Adding Solcmc table to README..."
+	@echo "### SolCMC" >> $(README)
+	@cat $(SOLCMC_Z3_TABLE) >> $(README)
+	@cat $(SOLCMC_ELD_TABLE) >> $(README)
+	@echo "" >> $(README)
+	@echo "Adding Certora table to README..."
+	@cat $(CERTORA_TABLE) >> $(README)
+
+#---------------------------- CERTORA ----------------------------#
+certora: $(CERTORA_TABLE)
+
+$(CERTORA_TABLE):
+	@cd $(realpath $(CERTORA_DIR)) && make
+
+#---------------------------- SOLCMC -----------------------------#
+solcmc: $(SOLCMC_Z3_TABLE) $(SOLCMC_ELD_TABLE)
+
+$(SOLCMC_Z3_TABLE):
+	@cd $(realpath $(SOLCMC_DIR)) && make solver=z3
+
+$(SOLCMC_ELD_TABLE):
+	@cd $(realpath $(SOLCMC_DIR)) && make solver=eld
+
+#---------------------------- README -----------------------------#
+plain: cleanr $(README)
+	
+$(README): $(VERSIONS_DIR) $(SKELETON) $(GROUND_TRUTH)
+	@echo "Generating plain README..."
+	@$(PYTHON) ../../scripts/readme_gen.py -d . > $(README)
+	@echo "## Experiments" >> $(README)
+
+#---------------------------- CLEAN ------------------------------#
+clean: cleanr clean-solcmc clean-certora
+
+cleanr:
+	rm -f $(README)
+
+clean-solcmc:
+	cd $(realpath $(SOLCMC_DIR)) && make clean
+
+clean-certora:
+	cd $(realpath $(CERTORA_DIR)) && make clean
diff --git a/contracts/simplified_deflationary_token/README.md b/contracts/simplified_deflationary_token/README.md
new file mode 100644
index 00000000..6e39d570
--- /dev/null
+++ b/contracts/simplified_deflationary_token/README.md
@@ -0,0 +1,59 @@
+# Simplified Deflationary Token
+
+## Specification
+This contract implements a simplified version of a deflationary token using `uint256`, where each transaction is charged a fixed fee (10% from the amount of tokens sent).
+The contract deployer will get ownership and total token amount and he’ll be excluded from paying transaction fees moreover can decide whether to exclude or include any user from paying them.
+
+## Properties
+- **liquidity**: Senders with a positive amount of tokens can always send the amount minus the fee.
+- **owner-can-exclude-include-from-fee**: Owner can include or exclude everyone in the fee payment.
+- **owner-fee-after-transfer**: To respect the deflationary token property, after every transfer the owner balance must be increased by fees.
+- **ownership-cannot-change**: The initial owner of the contract defined during the constructor call, cannot change.
+- **total-supply-integrity**: After a transfer, the total amount of tokens is always the same.
+- **user-cannot-exclude-include-from-fee**: A generic user cannot include or exclude someone in fees payment.
+- **validate-transfer-diff-o-s-r**: If owner, sender and receiver have distinct addresses, their balances are updated correctly after the transfer of a positive amount of tokens: Owner balance is incremented by the fee, Sender balance is decremented by the amount and Receiver balance is incremented by the amount minus the fee.
+- **validate-transfer-same-o-r**: If only owner and receiver have the same address, we check that their balances are updated correctly after the transfer of a positive amount of token: Owner balance is incremented by the amount, Sender balance is decremented by the amount and Receiver balance is the same as the owner balance.
+- **validate-transfer-same-o-s**: If only owner and sender have the same address, we check that their balances are updated correctly after the transfer of a positive amount of token: Owner balance is decremented by the amount minus the fee, Sender balance is the same as the owner balance and Receiver balance is incremented by the amount minus the fee.
+- **validate-transfer-same-o-s-r**: If the owner, sender and receiver have the same address, their balances remain unchanged after the transfer of a positive amount of token.
+- **validate-transfer-same-s-r**: If only sender and receiver have the same address, we check that their balances are updated correctly after the transfer of a positive amount of token: Owner balance is incremented by the fee, Sender balance is decremented by the fee and Receiver balance is the same as the sender balance.
+
+## Versions
+- **v1**: the transfer amount and fees are wrongly managed, the fees are not deducted from the sender but at the same time the owner receives the right fee amount (token duplication).
+- **v2**: the deflationary property is not well implemented, when we make a transfer with less than 10 tokens, no fees are charged.
+- **v3**: conforming to specification.
+
+## Ground truth
+|        | liquidity                            | owner-can-exclude-include-from-fee   | owner-fee-after-transfer             | ownership-cannot-change              | total-supply-integrity               | user-cannot-exclude-include-from-fee | validate-transfer-diff-o-s-r         | validate-transfer-same-o-r           | validate-transfer-same-o-s           | validate-transfer-same-o-s-r         | validate-transfer-same-s-r           |
+|--------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|
+| **v1** | 1                                    | 1                                    | 0                                    | 1                                    | 0                                    | 1                                    | 0                                    | 0                                    | 0                                    | 0                                    | 0                                    |
+| **v2** | 1                                    | 1                                    | 0                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    |
+| **v3** | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    |
+ 
+
+## Experiments
+### SolCMC
+#### Z3
+|        | liquidity                            | owner-can-exclude-include-from-fee   | owner-fee-after-transfer             | ownership-cannot-change              | total-supply-integrity               | user-cannot-exclude-include-from-fee | validate-transfer-diff-o-s-r         | validate-transfer-same-o-r           | validate-transfer-same-o-s           | validate-transfer-same-o-s-r         | validate-transfer-same-s-r           |
+|--------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|
+| **v1** | TP!                                  | TP!                                  | TN!                                  | ND                                   | TN                                   | TP!                                  | UNK                                  | UNK                                  | UNK                                  | UNK                                  | UNK                                  |
+| **v2** | TP!                                  | TP!                                  | TN!                                  | ND                                   | UNK                                  | TP!                                  | UNK                                  | TP!                                  | FN                                   | TP!                                  | UNK                                  |
+| **v3** | TP!                                  | TP!                                  | TP!                                  | ND                                   | UNK                                  | TP!                                  | UNK                                  | TP!                                  | UNK                                  | TP!                                  | UNK                                  |
+ 
+
+#### Eldarica
+|        | liquidity                            | owner-can-exclude-include-from-fee   | owner-fee-after-transfer             | ownership-cannot-change              | total-supply-integrity               | user-cannot-exclude-include-from-fee | validate-transfer-diff-o-s-r         | validate-transfer-same-o-r           | validate-transfer-same-o-s           | validate-transfer-same-o-s-r         | validate-transfer-same-s-r           |
+|--------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|
+| **v1** | TP!                                  | TP!                                  | TN!                                  | ND                                   | UNK                                  | TP!                                  | TN                                   | TN                                   | UNK                                  | UNK                                  | TN                                   |
+| **v2** | TP!                                  | TP!                                  | TN!                                  | ND                                   | UNK                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  |
+| **v3** | TP!                                  | TP!                                  | TP!                                  | ND                                   | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  |
+ 
+
+
+### Certora
+|        | liquidity                            | owner-can-exclude-include-from-fee   | owner-fee-after-transfer             | ownership-cannot-change              | total-supply-integrity               | user-cannot-exclude-include-from-fee | validate-transfer-diff-o-s-r         | validate-transfer-same-o-r           | validate-transfer-same-o-s           | validate-transfer-same-o-s-r         | validate-transfer-same-s-r           |
+|--------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|
+| **v1** | TP!                                  | TP!                                  | TN                                   | TP!                                  | TN                                   | TP!                                  | TN                                   | TN                                   | TN                                   | TN                                   | TN                                   |
+| **v2** | TP!                                  | TP!                                  | TN                                   | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  |
+| **v3** | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  |
+ 
+
diff --git a/contracts/simplified_deflationary_token/certora/Makefile b/contracts/simplified_deflationary_token/certora/Makefile
new file mode 100755
index 00000000..60f1b037
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/Makefile
@@ -0,0 +1,85 @@
+# Params 
+contract = ""
+specs = ""
+
+# Input Files
+VERSIONS_DIR = ../versions/
+PROPERTIES_DIR = .
+GROUND_TRUTH = ../ground-truth.csv
+SPEC_FILES = $(wildcard $(PROPERTIES_DIR)/*.spec)
+GETTER_FILE = getters.sol
+METHODS_FILE = methods.spec
+VERSIONS_FILES = $(wildcard $(VERSIONS_DIR)/*.sol)
+
+# Output Files
+BUILD_DIR = build
+OUTPUT_DIR = $(BUILD_DIR)
+CONTRACTS_DIR = $(OUTPUT_DIR)/contracts
+LOGS_DIR = $(OUTPUT_DIR)/logs
+SPEC_DIR = $(OUTPUT_DIR)/specs
+LIB_DIR = $(CONTRACTS_DIR)/lib
+OUT = $(OUTPUT_DIR)/out.csv
+CM = $(OUTPUT_DIR)/cm.csv
+TABLE = $(OUTPUT_DIR)/table.md
+
+PYTHON = python
+
+.PHONY: run one setup contracts specs getters directories clean-specs clean
+
+#---------------------------- RUN --------------------------------#
+run: $(TABLE)
+
+$(TABLE): $(CM)
+	@echo "Generating Certora results table ($(TABLE))..."
+	@echo "### Certora" > $(TABLE)
+	@$(PYTHON) ../../../scripts/mdtable_gen.py --input $(CM) >> $(TABLE)
+
+$(CM): $(GROUND_TRUTH) $(OUT) 
+	@echo "Generating Certora confusion matrix ($(CM))..."
+	@$(PYTHON) ../../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(OUT) > $(CM)
+
+$(OUT): setup $(VERSIONS_FILES) $(SPEC_FILES) $(GETTER_FILE) 
+	@echo "Running Certora experiments..."
+	@$(PYTHON) ../../../scripts/run_certora.py --contracts $(CONTRACTS_DIR) --specs $(SPEC_DIR) --output $(OUTPUT_DIR)
+
+one: clean-specs contracts specs directories 
+	@$(PYTHON) ../../../scripts/run_certora.py --contracts $(contract) --specs $(specs)
+
+#---------------------------- SETUP ------------------------------#
+setup: contracts specs getters directories
+
+contracts: $(CONTRACTS_DIR) getters
+	@$(PYTHON) ../../../scripts/inject_getters.py --contracts $(VERSIONS_DIR) --getters $(GETTER_FILE) --output $(CONTRACTS_DIR)
+
+specs: $(SPEC_DIR) 
+	@for file in $(SPEC_FILES); do \
+		if [ "$$file" != $(PROPERTIES_DIR)/"methods.spec" ]; then \
+			echo "Processing $$file"; \
+			cat $(METHODS_FILE) $$file >> $(SPEC_DIR)/$$file; \
+		fi \
+	done;
+
+getters: 
+	@if ! [ -e $(GETTER_FILE) ]; then touch $(GETTER_FILE); fi;
+
+directories: $(CONTRACTS_DIR) $(LOGS_DIR) $(LIB_DIR) $(SPEC_DIR)
+
+$(CONTRACTS_DIR):
+	@mkdir -p $@
+
+$(SPEC_DIR):
+	@mkdir -p $@
+
+$(LOGS_DIR):
+	@mkdir -p $@
+
+$(LIB_DIR):
+	@cp -r ../../../lib/ $@
+
+#---------------------------- CLEAN ------------------------------#
+clean-specs:
+	rm -rf $(SPEC_DIR)
+
+clean:
+	rm -rf $(BUILD_DIR)
+
diff --git a/contracts/simplified_deflationary_token/certora/getters.sol b/contracts/simplified_deflationary_token/certora/getters.sol
new file mode 100755
index 00000000..8b137891
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/getters.sol
@@ -0,0 +1 @@
+
diff --git a/contracts/simplified_deflationary_token/certora/liquidity.spec b/contracts/simplified_deflationary_token/certora/liquidity.spec
new file mode 100755
index 00000000..9a1a3190
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/liquidity.spec
@@ -0,0 +1,40 @@
+methods {
+    function balanceOf(address account) external returns (uint256) envfree;
+}
+
+function balancesSum(env e, address owner, address receiver) returns mathint {
+    mathint balancesSum;
+    uint ownerBalance = 0;
+    uint receiverBalance = 0;
+
+    if(e.msg.sender != owner) {
+        ownerBalance = balanceOf(owner);
+    }
+    if(e.msg.sender != receiver && owner != receiver) {
+        receiverBalance = balanceOf(receiver);
+    }
+    balancesSum = balanceOf(e.msg.sender) + ownerBalance + receiverBalance;
+    return balancesSum;
+}
+
+rule liquidity {
+    env e;
+    address owner = currentContract.owner;
+    uint amount;
+    address receiver;
+
+    requireInvariant correctTransactionFeePercent();
+    requireInvariant correctTotalSupply();
+    require(balancesSum(e, owner, receiver) <= currentContract.totalSupply);
+    require(e.msg.value == 0);
+    require(amount <= balanceOf(e.msg.sender) && amount > 0);
+
+    bool isMoneyTransferred = transfer@withrevert(e, receiver, amount);
+    assert(!lastReverted);
+}
+
+invariant correctTransactionFeePercent()
+    currentContract.transactionFeePercent == 10;
+
+invariant correctTotalSupply()
+    currentContract.totalSupply == 1000000000000000000000000;
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/methods.spec b/contracts/simplified_deflationary_token/certora/methods.spec
new file mode 100755
index 00000000..8b137891
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/methods.spec
@@ -0,0 +1 @@
+
diff --git a/contracts/simplified_deflationary_token/certora/owner-can-exclude-include-from-fee.spec b/contracts/simplified_deflationary_token/certora/owner-can-exclude-include-from-fee.spec
new file mode 100755
index 00000000..3b08a7a0
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/owner-can-exclude-include-from-fee.spec
@@ -0,0 +1,13 @@
+rule owner_can_exclude_include_from_fee {
+    env e;
+    address owner = currentContract.owner;
+    address account;
+
+    require(owner == e.msg.sender);
+    require(e.msg.value == 0);
+    require(currentContract.isExcludedFromFee[account] == false);
+    excludeFromFee@withrevert(e, account);
+    assert(currentContract.isExcludedFromFee[account] == true);
+    includeInFee@withrevert(e, account);
+    assert(currentContract.isExcludedFromFee[account] == false);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/owner-fee-after-transfer.spec b/contracts/simplified_deflationary_token/certora/owner-fee-after-transfer.spec
new file mode 100755
index 00000000..a1ae799c
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/owner-fee-after-transfer.spec
@@ -0,0 +1,19 @@
+methods {
+    function balanceOf(address account) external returns (uint256) envfree;
+    function calculateFee(uint256 amount) external returns (uint256) envfree;
+}
+
+
+rule owner_fee_after_transfer {
+    env e;
+    address owner = currentContract.owner;
+    address receiver;
+
+    uint256 amount;
+    require(amount > 0);
+    require(currentContract.isExcludedFromFee[e.msg.sender] == false);
+
+    uint256 fee = calculateFee(amount);
+
+    assert(fee > 0);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/ownership-cannot-change.spec b/contracts/simplified_deflationary_token/certora/ownership-cannot-change.spec
new file mode 100755
index 00000000..5e8d071a
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/ownership-cannot-change.spec
@@ -0,0 +1,24 @@
+methods {
+    function balanceOf(address account) external returns (uint256) envfree;
+    function calculateFee(uint256 amount) external returns (uint256) envfree;
+}
+
+hook Sstore SimplifiedDeflationaryToken.owner address hook_owner (address hook_old_owner) {
+    old_owner = hook_old_owner;
+}
+
+ghost address old_owner;
+
+rule ownership_cannot_change {
+    env e;
+    calldataarg args;
+
+    require(old_owner == currentContract.owner);
+
+    transfer@withrevert(e, args);
+    assert(old_owner == currentContract.owner);
+    excludeFromFee@withrevert(e, args);
+    assert(old_owner == currentContract.owner);
+    includeInFee@withrevert(e, args);
+    assert(old_owner == currentContract.owner);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/total-supply-integrity.spec b/contracts/simplified_deflationary_token/certora/total-supply-integrity.spec
new file mode 100755
index 00000000..68cf8830
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/total-supply-integrity.spec
@@ -0,0 +1,42 @@
+methods {
+    function balanceOf(address account) external returns (uint256) envfree;
+}
+
+function balancesSum(env e, address owner, address receiver) returns mathint {
+    mathint balancesSum;
+    uint ownerBalance = 0;
+    uint receiverBalance = 0;
+
+    if(e.msg.sender != owner) {
+        ownerBalance = balanceOf(owner);
+    }
+    if(e.msg.sender != receiver && owner != receiver) {
+        receiverBalance = balanceOf(receiver);
+    }
+    balancesSum = balanceOf(e.msg.sender) + ownerBalance + receiverBalance;
+    return balancesSum;
+}
+rule total_supply_integrity {
+    env e;
+    address owner = currentContract.owner;
+    address receiver;
+    address user;
+    uint256 amount;
+    mathint oldSumBalances = balancesSum(e, owner, receiver);
+    uint256 oldUserBalance = balanceOf(user);
+
+    requireInvariant correctTotalSupply;
+    requireInvariant correctTransactionFeePercent;
+    require(user != owner && user != receiver && user != e.msg.sender);
+    require(oldSumBalances <= currentContract.totalSupply);
+    transfer(e, receiver, amount);
+    assert(balanceOf(user) == oldUserBalance);
+    assert(balancesSum(e, owner, receiver) == oldSumBalances);
+}
+
+
+invariant correctTransactionFeePercent()
+    currentContract.transactionFeePercent == 10;
+
+invariant correctTotalSupply()
+    currentContract.totalSupply == 1000000000000000000000000;
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/user-cannot-exclude-include-from-fee.spec b/contracts/simplified_deflationary_token/certora/user-cannot-exclude-include-from-fee.spec
new file mode 100755
index 00000000..4340dbf4
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/user-cannot-exclude-include-from-fee.spec
@@ -0,0 +1,16 @@
+rule user_cannot_exclude_include_from_fee {
+    env e;
+    address owner = currentContract.owner;
+    address account;
+
+    require(owner != e.msg.sender);
+    require(e.msg.value == 0);
+
+    require(currentContract.isExcludedFromFee[account] == false);
+    excludeFromFee@withrevert(e, account);
+    assert(currentContract.isExcludedFromFee[account] == false);
+
+    require(currentContract.isExcludedFromFee[e.msg.sender] == true);
+    includeInFee@withrevert(e, e.msg.sender);
+    assert(currentContract.isExcludedFromFee[e.msg.sender] == true);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/validate-transfer-diff-o-s-r.spec b/contracts/simplified_deflationary_token/certora/validate-transfer-diff-o-s-r.spec
new file mode 100755
index 00000000..2666ac07
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/validate-transfer-diff-o-s-r.spec
@@ -0,0 +1,36 @@
+methods {
+   function balanceOf(address account) external returns (uint256) envfree;
+   function calculateFee(uint256 amount) external returns (uint256) envfree;
+}
+
+rule validate_transfer_diff_o_s_r {
+   env e;
+   address owner = currentContract.owner;
+   address receiver;
+
+   uint256 amount;
+   uint256 expectedFee = currentContract.isExcludedFromFee[e.msg.sender] ? 0
+                                                   : calculateFee(amount);
+
+   requireInvariant correctTotalSupply;
+   requireInvariant correctTransactionFeePercent;
+
+   require(owner != e.msg.sender && e.msg.sender != receiver && owner != receiver);
+
+   mathint oldOwnerBalance = balanceOf(owner);
+   mathint oldSenderBalance = balanceOf(e.msg.sender);
+   mathint oldReceiverBalance = balanceOf(receiver);
+   require(oldOwnerBalance + oldReceiverBalance + oldSenderBalance <= currentContract.totalSupply);
+
+   transfer(e, receiver, amount);
+
+   assert(balanceOf(owner) == oldOwnerBalance + expectedFee);
+   assert(balanceOf(e.msg.sender) == oldSenderBalance - amount);
+   assert(balanceOf(receiver) == oldReceiverBalance + amount - expectedFee);
+}
+
+invariant correctTransactionFeePercent()
+   currentContract.transactionFeePercent == 10;
+
+invariant correctTotalSupply()
+   currentContract.totalSupply == 1000000000000000000000000;
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/validate-transfer-same-o-r.spec b/contracts/simplified_deflationary_token/certora/validate-transfer-same-o-r.spec
new file mode 100755
index 00000000..da36128c
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/validate-transfer-same-o-r.spec
@@ -0,0 +1,36 @@
+methods {
+   function balanceOf(address account) external returns (uint256) envfree;
+   function calculateFee(uint256 amount) external returns (uint256) envfree;
+}
+
+rule validate_transfer_same_o_r {
+   env e;
+   address owner = currentContract.owner;
+   address receiver;
+
+   uint256 amount;
+   uint256 expectedFee = currentContract.isExcludedFromFee[e.msg.sender] ? 0
+                                                   : calculateFee(amount);
+
+   requireInvariant correctTotalSupply;
+   requireInvariant correctTransactionFeePercent;
+
+   require(owner == receiver && e.msg.sender != receiver);
+
+   mathint oldOwnerBalance = balanceOf(owner);
+   mathint oldSenderBalance = balanceOf(e.msg.sender);
+   mathint oldReceiverBalance = balanceOf(receiver);
+   require(oldOwnerBalance + oldReceiverBalance + oldSenderBalance <= currentContract.totalSupply);
+
+   transfer(e, receiver, amount);
+
+   assert(balanceOf(owner) == oldOwnerBalance + amount);
+   assert(balanceOf(e.msg.sender) == oldSenderBalance - amount);
+   assert(balanceOf(receiver) == oldReceiverBalance + amount);
+}
+
+invariant correctTransactionFeePercent()
+   currentContract.transactionFeePercent == 10;
+
+invariant correctTotalSupply()
+   currentContract.totalSupply == 1000000000000000000000000;
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/validate-transfer-same-o-s-r.spec b/contracts/simplified_deflationary_token/certora/validate-transfer-same-o-s-r.spec
new file mode 100755
index 00000000..09a14f90
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/validate-transfer-same-o-s-r.spec
@@ -0,0 +1,37 @@
+methods {
+   function balanceOf(address account) external returns (uint256) envfree;
+   function calculateFee(uint256 amount) external returns (uint256) envfree;
+}
+
+rule validate_transfer_same_o_s_r {
+   env e;
+   address owner = currentContract.owner;
+   address receiver;
+
+   uint256 amount;
+   uint256 expectedFee = currentContract.isExcludedFromFee[e.msg.sender] ? 0
+                                                   : calculateFee(amount);
+
+   requireInvariant correctTotalSupply;
+   requireInvariant correctTransactionFeePercent;
+
+   require(owner == e.msg.sender && e.msg.sender == receiver);
+
+   mathint oldOwnerBalance = balanceOf(owner);
+   mathint oldSenderBalance = balanceOf(e.msg.sender);
+   mathint oldReceiverBalance = balanceOf(receiver);
+   require(oldOwnerBalance + oldReceiverBalance + oldSenderBalance <= currentContract.totalSupply);
+
+   bool success = transfer(e, receiver, amount);
+
+   require success == true;
+   assert(oldOwnerBalance == balanceOf(owner));
+   assert(oldSenderBalance == balanceOf(receiver));
+   assert(oldReceiverBalance == balanceOf(e.msg.sender));
+}
+
+invariant correctTransactionFeePercent()
+   currentContract.transactionFeePercent == 10;
+
+invariant correctTotalSupply()
+   currentContract.totalSupply == 1000000000000000000000000;
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/validate-transfer-same-o-s.spec b/contracts/simplified_deflationary_token/certora/validate-transfer-same-o-s.spec
new file mode 100755
index 00000000..bf6bdc40
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/validate-transfer-same-o-s.spec
@@ -0,0 +1,36 @@
+methods {
+   function balanceOf(address account) external returns (uint256) envfree;
+   function calculateFee(uint256 amount) external returns (uint256) envfree;
+}
+
+rule validate_transfer_same_o_s {
+   env e;
+   address owner = currentContract.owner;
+   address receiver;
+
+   requireInvariant correctTotalSupply;
+   requireInvariant correctTransactionFeePercent;
+
+   uint256 amount;
+   uint256 expectedFee = currentContract.isExcludedFromFee[e.msg.sender] ? 0
+                                                   : calculateFee(amount);
+  
+   require owner == e.msg.sender && e.msg.sender != receiver;
+
+   mathint oldOwnerBalance = balanceOf(owner);
+   mathint oldSenderBalance = balanceOf(e.msg.sender);
+   mathint oldReceiverBalance = balanceOf(receiver);
+   require (oldOwnerBalance + oldReceiverBalance) == currentContract.totalSupply;
+
+   transfer(e, receiver, amount);
+  
+   assert(balanceOf(owner) == oldOwnerBalance - amount + expectedFee);
+   assert(balanceOf(e.msg.sender) == oldSenderBalance - amount + expectedFee);
+   assert(balanceOf(receiver) == oldReceiverBalance + amount - expectedFee);
+}
+
+invariant correctTransactionFeePercent()
+   currentContract.transactionFeePercent == 10;
+
+invariant correctTotalSupply()
+   currentContract.totalSupply == 1000000000000000000000000;
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/certora/validate-transfer-same-s-r.spec b/contracts/simplified_deflationary_token/certora/validate-transfer-same-s-r.spec
new file mode 100755
index 00000000..7230e257
--- /dev/null
+++ b/contracts/simplified_deflationary_token/certora/validate-transfer-same-s-r.spec
@@ -0,0 +1,37 @@
+methods {
+   function balanceOf(address account) external returns (uint256) envfree;
+   function calculateFee(uint256 amount) external returns (uint256) envfree;
+}
+
+rule validate_transfer_same_s_r {
+   env e;
+   address owner = currentContract.owner;
+   address receiver;
+
+   uint256 amount;
+   uint256 expectedFee = currentContract.isExcludedFromFee[e.msg.sender] ? 0
+                                                   : calculateFee(amount);
+
+   requireInvariant correctTotalSupply;
+   requireInvariant correctTransactionFeePercent;
+
+   require(owner != e.msg.sender && e.msg.sender == receiver);
+
+   mathint oldOwnerBalance = balanceOf(owner);
+   mathint oldSenderBalance = balanceOf(e.msg.sender);
+   mathint oldReceiverBalance = balanceOf(receiver);
+   require(oldOwnerBalance + oldReceiverBalance + oldSenderBalance <= currentContract.totalSupply);
+
+   transfer(e, receiver, amount);
+
+   assert(balanceOf(owner) == oldOwnerBalance + expectedFee);
+   assert(balanceOf(e.msg.sender) == oldSenderBalance - expectedFee);
+   assert(balanceOf(receiver) == oldReceiverBalance - expectedFee);
+}
+
+invariant correctTransactionFeePercent()
+   currentContract.transactionFeePercent == 10;
+
+invariant correctTotalSupply()
+   currentContract.totalSupply == 1000000000000000000000000;
+
diff --git a/contracts/simplified_deflationary_token/ground-truth.csv b/contracts/simplified_deflationary_token/ground-truth.csv
new file mode 100755
index 00000000..b865878a
--- /dev/null
+++ b/contracts/simplified_deflationary_token/ground-truth.csv
@@ -0,0 +1,34 @@
+property,version,truth,footnote-md
+total-supply-integrity,v1,0,""
+validate-transfer-diff-o-s-r,v1,0,""
+validate-transfer-same-o-s-r,v1,0,""
+validate-transfer-same-s-r,v1,0,""
+validate-transfer-same-o-s,v1,0,""
+validate-transfer-same-o-r,v1,0,""
+user-cannot-exclude-include-from-fee,v1,1,
+owner-can-exclude-include-from-fee,v1,1,
+ownership-cannot-change,v1,1,
+owner-fee-after-transfer,v1,0,""
+liquidity,v1,1,
+total-supply-integrity,v2,1,
+validate-transfer-diff-o-s-r,v2,1,
+validate-transfer-same-o-s-r,v2,1,
+validate-transfer-same-s-r,v2,1,
+validate-transfer-same-o-s,v2,1,
+validate-transfer-same-o-r,v2,1,
+user-cannot-exclude-include-from-fee,v2,1,
+owner-can-exclude-include-from-fee,v2,1,
+ownership-cannot-change,v2,1,
+owner-fee-after-transfer,v2,0,""
+liquidity,v2,1,
+total-supply-integrity,v3,1,
+validate-transfer-diff-o-s-r,v3,1,
+validate-transfer-same-o-s-r,v3,1,
+validate-transfer-same-s-r,v3,1,
+validate-transfer-same-o-s,v3,1,
+validate-transfer-same-o-r,v3,1,
+user-cannot-exclude-include-from-fee,v3,1,
+owner-can-exclude-include-from-fee,v3,1,
+ownership-cannot-change,v3,1,
+owner-fee-after-transfer,v3,1,
+liquidity,v3,1,
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/hardhat/SimplifiedDeflationaryTokenV1.sol b/contracts/simplified_deflationary_token/hardhat/SimplifiedDeflationaryTokenV1.sol
new file mode 100755
index 00000000..aabad023
--- /dev/null
+++ b/contracts/simplified_deflationary_token/hardhat/SimplifiedDeflationaryTokenV1.sol
@@ -0,0 +1,57 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+/// @custom:version the transfer amount and fees are wrongly managed, the fees are not deducted from the sender but at the same time the owner receives the right fee amount (token duplication).
+contract SimplifiedDeflationaryTokenV1 {
+    mapping(address => uint256) public balances;
+    mapping(address => bool) public isExcludedFromFee;
+
+    uint256 public totalSupply = 1000000 * (10**18);
+    uint256 public transactionFeePercent = 10;
+
+    address public owner;
+
+    event Transfer(address indexed from, address indexed to, uint256 value);
+
+    constructor() {
+        owner = msg.sender;
+        balances[owner] = totalSupply;
+        isExcludedFromFee[owner] = true;
+    }
+
+    function transfer(address to, uint256 amount) public returns (bool) {
+        require(balances[msg.sender] >= amount, "Insufficient balance");
+
+        uint256 fee = 0;
+        if (!isExcludedFromFee[msg.sender]) {
+            fee = calculateFee(amount);
+            amount = amount - fee; 
+            balances[owner] += fee;
+        }
+
+        balances[msg.sender] -= amount;
+        balances[to] += amount;
+
+        emit Transfer(msg.sender, to, amount);
+
+        return true;
+    }
+
+    function calculateFee(uint256 amount) public view returns (uint256) {
+        return (amount * transactionFeePercent) / 100;
+    }
+
+    function excludeFromFee(address account) public {
+        require(msg.sender == owner, "Only owner can exclude from fee");
+        isExcludedFromFee[account] = true;
+    }
+
+    function includeInFee(address account) public {
+        require(msg.sender == owner, "Only owner can include in fee");
+        isExcludedFromFee[account] = false;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return balances[account];
+    }
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/hardhat/SimplifiedDeflationaryTokenV2.sol b/contracts/simplified_deflationary_token/hardhat/SimplifiedDeflationaryTokenV2.sol
new file mode 100755
index 00000000..9e17cf8d
--- /dev/null
+++ b/contracts/simplified_deflationary_token/hardhat/SimplifiedDeflationaryTokenV2.sol
@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+/// @custom:version the deflationary property is not well implemented, when we make a transfer with less than 10 tokens, no fees are charged.
+contract SimplifiedDeflationaryTokenV2 {
+    mapping(address => uint256) public balances;
+    mapping(address => bool) public isExcludedFromFee;
+
+    uint256 public totalSupply = 1000000 * (10**18);
+    uint256 public transactionFeePercent = 10;
+
+    address public owner;
+
+    event Transfer(address indexed from, address indexed to, uint256 value);
+
+    constructor() {
+        owner = msg.sender;
+        balances[owner] = totalSupply;
+        isExcludedFromFee[owner] = true;
+    }
+
+    function transfer(address to, uint256 amount) public returns (bool) {
+        require(balances[msg.sender] >= amount, "Insufficient balance");
+
+        uint256 fee = 0;
+        if (!isExcludedFromFee[msg.sender]) {
+            fee = calculateFee(amount);
+            balances[owner] += fee;
+        }
+
+        balances[msg.sender] -= amount;
+        balances[to] += (amount - fee);
+
+        emit Transfer(msg.sender, to, amount);
+
+        return true;
+    }
+
+    function calculateFee(uint256 amount) public view returns (uint256) {
+        return (amount * transactionFeePercent) / 100;
+    }
+
+    function excludeFromFee(address account) public {
+        require(msg.sender == owner, "Only owner can exclude from fee");
+        isExcludedFromFee[account] = true;
+    }
+
+    function includeInFee(address account) public {
+        require(msg.sender == owner, "Only owner can include in fee");
+        isExcludedFromFee[account] = false;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return balances[account];
+    }
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/hardhat/test.js b/contracts/simplified_deflationary_token/hardhat/test.js
new file mode 100755
index 00000000..35b8b42e
--- /dev/null
+++ b/contracts/simplified_deflationary_token/hardhat/test.js
@@ -0,0 +1,45 @@
+const {
+    loadFixture,
+  } = require("@nomicfoundation/hardhat-toolbox/network-helpers");
+  const { expect } = require("chai");
+
+  describe("SimplifiedDeflationaryToken", function() {
+    async function deployContractv1() {
+      const [owner, sender, receiver] = await ethers.getSigners();
+
+      const sdtv1 = await ethers.getContractFactory("SimplifiedDeflationaryTokenV1");
+      const SDTv1 = await sdtv1.connect(owner).deploy();
+
+      const sdtv2 = await ethers.getContractFactory("SimplifiedDeflationaryTokenV2");
+      const SDTv2 = await sdtv2.connect(owner).deploy();
+
+      return { SDTv1, SDTv2, owner, sender, receiver };
+    }
+      it("Token duplication", async function(){
+        const { SDTv1, owner, sender, receiver } = await loadFixture(deployContractv1);
+        await SDTv1.connect(owner).transfer(sender.address, 100);
+        
+        await SDTv1.connect(sender).transfer(receiver.address, 100);
+        
+        let balanceOwner = await SDTv1.balanceOf(owner.address);
+        let balanceSender = await SDTv1.balanceOf(sender.address);
+        let balanceReceiver = await SDTv1.balanceOf(receiver.address);
+        
+        expect(
+          balanceReceiver+balanceOwner+balanceSender
+        ).to.be.gt(await SDTv1.totalSupply());
+      })
+      
+      it("Unpaid Fee", async function(){
+        const { SDTv2, owner, sender, receiver } = await loadFixture(deployContractv1);
+        await SDTv2.connect(owner).transfer(sender.address, 100);
+        
+        let balanceBeforeOwner = await SDTv2.balanceOf(owner.address);
+
+        await SDTv2.connect(sender).transfer(receiver.address, 9);
+      
+        expect(
+          await SDTv2.balanceOf(owner.address)
+        ).to.be.equal(balanceBeforeOwner);
+      })
+  })
diff --git a/contracts/simplified_deflationary_token/skeleton.json b/contracts/simplified_deflationary_token/skeleton.json
new file mode 100755
index 00000000..afbb3b27
--- /dev/null
+++ b/contracts/simplified_deflationary_token/skeleton.json
@@ -0,0 +1,17 @@
+{
+    "name": "Simplified Deflationary Token",
+    "specification": "file:spec.md",
+    "properties": {
+        "total-supply-integrity": "After a transfer, the total amount of tokens is always the same.",
+        "validate-transfer-diff-o-s-r": "If owner, sender and receiver have distinct addresses, their balances are updated correctly after the transfer of a positive amount of tokens: Owner balance is incremented by the fee, Sender balance is decremented by the amount and Receiver balance is incremented by the amount minus the fee.",
+        "validate-transfer-same-o-s-r": "If the owner, sender and receiver have the same address, their balances remain unchanged after the transfer of a positive amount of token.",
+        "validate-transfer-same-s-r": "If only sender and receiver have the same address, we check that their balances are updated correctly after the transfer of a positive amount of token: Owner balance is incremented by the fee, Sender balance is decremented by the fee and Receiver balance is the same as the sender balance.",
+        "validate-transfer-same-o-s": "If only owner and sender have the same address, we check that their balances are updated correctly after the transfer of a positive amount of token: Owner balance is decremented by the amount minus the fee, Sender balance is the same as the owner balance and Receiver balance is incremented by the amount minus the fee.",
+        "validate-transfer-same-o-r": "If only owner and receiver have the same address, we check that their balances are updated correctly after the transfer of a positive amount of token: Owner balance is incremented by the amount, Sender balance is decremented by the amount and Receiver balance is the same as the owner balance.",
+        "user-cannot-exclude-include-from-fee": "A generic user cannot include or exclude someone in fees payment.",
+        "owner-can-exclude-include-from-fee": "Owner can include or exclude everyone in the fee payment.",
+        "ownership-cannot-change": "The initial owner of the contract defined during the constructor call, cannot change.",
+        "owner-fee-after-transfer": "To respect the deflationary token property, after every transfer the owner balance must be increased by fees.",
+        "liquidity": "Senders with a positive amount of tokens can always send the amount minus the fee."
+        }
+}
diff --git a/contracts/simplified_deflationary_token/solcmc/Makefile b/contracts/simplified_deflationary_token/solcmc/Makefile
new file mode 100755
index 00000000..6ed4dd8f
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/Makefile
@@ -0,0 +1,68 @@
+# Params
+solver = z3
+to = 10m
+contract = ""
+
+# Input files
+VERSIONS_DIR = ../versions/
+PROPERTIES_DIR = .
+GROUND_TRUTH = ../ground-truth.csv
+PROPERTIES_FILES = $(wildcard $(PROPERTIES_DIR)/*.sol)
+VERSIONS_FILES = $(wildcard $(VERSIONS_DIR)/*.sol)
+
+# Output files
+BUILD_DIR = build
+OUTPUT_DIR = $(BUILD_DIR)/$(solver)
+CONTRACTS_DIR = $(BUILD_DIR)/contracts
+LOGS_DIR = $(OUTPUT_DIR)/logs
+LIB_DIR = $(CONTRACTS_DIR)/lib
+OUT = $(OUTPUT_DIR)/out.csv
+CM = $(OUTPUT_DIR)/cm.csv
+TABLE = $(OUTPUT_DIR)/table.md
+
+PYTHON = python
+
+.PHONY: run one setup contracts directories clean
+
+#---------------------------- RUN --------------------------------#
+run: $(TABLE)
+
+$(TABLE): $(CM)
+	@echo "Generating SolCMC results table ($(TABLE))..."
+	@if [ $(solver) = "z3" ]; then echo "#### Z3" > $(TABLE); \
+	elif [ $(solver) = "eld" ]; then echo "#### Eldarica" > $(TABLE); fi
+	@$(PYTHON) ../../../scripts/mdtable_gen.py --input $(CM) >> $(TABLE)
+
+$(CM): $(GROUND_TRUTH) $(OUT)
+	@echo "Generating Solcmc confusion matrix ($(CM))..."
+	@$(PYTHON) ../../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(OUT) > $(CM)
+
+$(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)
+
+one: setup
+	@$(PYTHON) ../../../scripts/run_solcmc.py --contracts $(contract) --timeout $(to)
+
+#---------------------------- SETUP ------------------------------#
+setup: contracts directories
+
+contracts: $(VERSIONS_FILES) $(PROPERTIES_FILES) $(CONTRACTS_DIR)
+	@echo "Building contracts..."
+	@$(PYTHON) ../../../scripts/builder.py --versions $(VERSIONS_DIR) --properties $(PROPERTIES_DIR) --output $(CONTRACTS_DIR)
+
+directories: $(CONTRACTS_DIR) $(LOGS_DIR) $(LIB_DIR)
+
+$(CONTRACTS_DIR):
+	@mkdir -p $@
+
+$(LOGS_DIR):
+	@mkdir -p $@
+
+$(LIB_DIR):
+	@cp -r ../../../lib/ $@
+
+#---------------------------- CLEAN ------------------------------#
+clean:
+	@echo "Deleting \"solcmc/build/\"..."
+	@rm -rf $(BUILD_DIR)
diff --git a/contracts/simplified_deflationary_token/solcmc/liquidity.sol b/contracts/simplified_deflationary_token/solcmc/liquidity.sol
new file mode 100755
index 00000000..f71240ad
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/liquidity.sol
@@ -0,0 +1,21 @@
+function liquidity(address receiver, uint256 amount) public {
+    require(balancesSum(receiver) <= totalSupply);
+    require(amount <= balanceOf(msg.sender) && amount > 0);
+    bool isMoneyTransferred = transfer(receiver, amount);
+    assert(isMoneyTransferred);
+}
+
+function balancesSum(address receiver) public view returns (uint256) {
+    uint256 balanceSums;
+    uint256 ownerBalance = 0;
+    uint256 receiverBalance = 0;
+
+    if(msg.sender != owner) {
+        ownerBalance = balanceOf(owner);
+    }
+    if(msg.sender != receiver && owner != receiver) {
+        receiverBalance = balanceOf(receiver);
+    }
+    balanceSums = balanceOf(msg.sender) + ownerBalance + receiverBalance;
+    return balanceSums;
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/solcmc/owner-can-exclude-include-from-fee.sol b/contracts/simplified_deflationary_token/solcmc/owner-can-exclude-include-from-fee.sol
new file mode 100755
index 00000000..c98d7d95
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/owner-can-exclude-include-from-fee.sol
@@ -0,0 +1,8 @@
+function ownerCanExcludeIncludeFromFee(address user) public {
+    require(owner == msg.sender);
+    require(isExcludedFromFee[user] == false);
+    excludeFromFee(user);
+    assert(isExcludedFromFee[user] == true);
+    includeInFee(user);
+    assert(isExcludedFromFee[user] == false);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/solcmc/owner-fee-after-transfer.sol b/contracts/simplified_deflationary_token/solcmc/owner-fee-after-transfer.sol
new file mode 100755
index 00000000..38215b49
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/owner-fee-after-transfer.sol
@@ -0,0 +1,6 @@
+function ownerFeeAfterTransfer(uint256 amount) public view {
+   require(amount > 0);
+   require(isExcludedFromFee[msg.sender] == false);
+   uint256 fee = calculateFee(amount);
+   assert(fee > 0);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/solcmc/total-supply-integrity.sol b/contracts/simplified_deflationary_token/solcmc/total-supply-integrity.sol
new file mode 100755
index 00000000..3c1cc600
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/total-supply-integrity.sol
@@ -0,0 +1,24 @@
+function balancesSum(address receiver) public view returns (uint256) {
+   uint256 balanceSums;
+   uint256 ownerBalance = 0;
+   uint256 receiverBalance = 0;
+
+   if(msg.sender != owner) {
+       ownerBalance = balanceOf(owner);
+   }
+   if(msg.sender != receiver && owner != receiver) {
+       receiverBalance = balanceOf(receiver);
+   }
+   balanceSums = balanceOf(msg.sender) + ownerBalance + receiverBalance;
+   return balanceSums;
+}
+
+function totalSupplyIntegrity(address user, address receiver, uint256 amount) public {
+   uint256 oldUserBalance = balanceOf(user);
+   uint256 oldSumBalances = balancesSum(receiver);
+   require(user != owner && user != receiver && user != msg.sender);
+   require(oldSumBalances <= totalSupply);
+   transfer(receiver, amount);
+   assert(balanceOf(user) == oldUserBalance);
+   assert(balancesSum(receiver) == oldSumBalances);
+}
diff --git a/contracts/simplified_deflationary_token/solcmc/user-cannot-exclude-include-from-fee.sol b/contracts/simplified_deflationary_token/solcmc/user-cannot-exclude-include-from-fee.sol
new file mode 100755
index 00000000..30dadb4e
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/user-cannot-exclude-include-from-fee.sol
@@ -0,0 +1,9 @@
+function userCannotExcludeIncludeFromFee(address user) public {
+   require(owner != msg.sender);
+   require(isExcludedFromFee[user] == false);
+   excludeFromFee(user);
+   assert(isExcludedFromFee[user] == false);
+   require(isExcludedFromFee[msg.sender] == true);
+   includeInFee(msg.sender);
+   assert(isExcludedFromFee[msg.sender] == true);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/solcmc/validate-transfer-diff-o-s-r.sol b/contracts/simplified_deflationary_token/solcmc/validate-transfer-diff-o-s-r.sol
new file mode 100755
index 00000000..e4f7a780
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/validate-transfer-diff-o-s-r.sol
@@ -0,0 +1,14 @@
+function validateTransferDiffSR(address receiver, uint256 amount) public {
+   require(owner != msg.sender && msg.sender != receiver && owner != receiver);
+   uint256 oldSenderBalance = balances[msg.sender];
+   uint256 oldReceiverBalance = balances[receiver];
+   uint256 oldOwnerBalance = balances[owner];
+   uint256 expectedFee = isExcludedFromFee[msg.sender] ? 0 : calculateFee(amount);
+   require(oldOwnerBalance + oldReceiverBalance + oldSenderBalance <= totalSupply);
+   transfer(receiver, amount);
+   assert(balances[msg.sender] == oldSenderBalance - amount);
+   assert(balances[receiver] == oldReceiverBalance + amount - expectedFee);
+   assert(balances[owner] == oldOwnerBalance + expectedFee);
+
+}
+
diff --git a/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-o-r.sol b/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-o-r.sol
new file mode 100755
index 00000000..a79c21c8
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-o-r.sol
@@ -0,0 +1,11 @@
+function validateTransferSameOR(address receiver, uint256 amount) public {
+   require(owner != msg.sender && owner == receiver);
+   uint256 oldSenderBalance = balances[msg.sender];
+   uint256 oldReceiverBalance = balances[receiver];
+   uint256 oldOwnerBalance = balances[owner];
+   require(oldOwnerBalance + oldReceiverBalance + oldSenderBalance <= totalSupply);
+   transfer(receiver, amount);
+   assert(balances[msg.sender] == oldSenderBalance - amount);
+   assert(balances[receiver] == oldReceiverBalance + amount);
+   assert(balances[owner] == oldOwnerBalance + amount);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-o-s-r.sol b/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-o-s-r.sol
new file mode 100755
index 00000000..05ce7950
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-o-s-r.sol
@@ -0,0 +1,12 @@
+function validateTransferSameOSR(address receiver, uint256 amount) public {
+   require(owner == msg.sender && msg.sender == receiver);
+   uint256 oldSenderBalance = balances[msg.sender];
+   uint256 oldReceiverBalance = balances[receiver];
+   uint256 oldOwnerBalance = balances[owner];
+  
+   require(oldOwnerBalance + oldReceiverBalance + oldSenderBalance <= totalSupply);
+   transfer(receiver, amount);
+   assert(balances[msg.sender] == oldSenderBalance);
+   assert(balances[receiver] == oldReceiverBalance);
+   assert(balances[owner] == oldOwnerBalance);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-o-s.sol b/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-o-s.sol
new file mode 100755
index 00000000..a1f9cb1c
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-o-s.sol
@@ -0,0 +1,13 @@
+function validateTransferSameOS(address receiver, uint256 amount) public {
+   require(owner == msg.sender && msg.sender != receiver);
+   uint256 oldSenderBalance = balances[msg.sender];
+   uint256 oldReceiverBalance = balances[receiver];
+   uint256 oldOwnerBalance = balances[owner];
+   uint256 expectedFee = isExcludedFromFee[msg.sender] ? 0 : calculateFee(amount);
+
+   require(oldOwnerBalance + oldReceiverBalance + oldSenderBalance <= totalSupply);
+   transfer(receiver, amount);
+   assert(balances[msg.sender] == oldSenderBalance - amount + expectedFee);
+   assert(balances[receiver] == oldReceiverBalance + amount - expectedFee);
+   assert(balances[owner] == oldOwnerBalance - amount + expectedFee);
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-s-r.sol b/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-s-r.sol
new file mode 100755
index 00000000..695bcc3c
--- /dev/null
+++ b/contracts/simplified_deflationary_token/solcmc/validate-transfer-same-s-r.sol
@@ -0,0 +1,14 @@
+function validateTransferSR(address receiver, uint256 amount) public {
+   require(owner != msg.sender && msg.sender == receiver);
+   uint256 oldSenderBalance = balances[msg.sender];
+   uint256 oldReceiverBalance = balances[receiver];
+   uint256 oldOwnerBalance = balances[owner];
+   uint256 expectedFee = isExcludedFromFee[msg.sender] ? 0 : calculateFee(amount);
+
+   require(oldOwnerBalance + oldReceiverBalance + oldSenderBalance <= totalSupply);
+   transfer(receiver, amount);
+   assert(balances[msg.sender] == oldSenderBalance - expectedFee);
+   assert(balances[receiver] == oldReceiverBalance - expectedFee);
+   assert(balances[owner] == oldOwnerBalance + expectedFee);
+}
+
diff --git a/contracts/simplified_deflationary_token/spec.md b/contracts/simplified_deflationary_token/spec.md
new file mode 100755
index 00000000..53dc8ef2
--- /dev/null
+++ b/contracts/simplified_deflationary_token/spec.md
@@ -0,0 +1,2 @@
+This contract implements a simplified version of a deflationary token using `uint256`, where each transaction is charged a fixed fee (10% from the amount of tokens sent).
+The contract deployer will get ownership and total token amount and he’ll be excluded from paying transaction fees moreover can decide whether to exclude or include any user from paying them.
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/versions/SimplifiedDeflationaryToken_v1.sol b/contracts/simplified_deflationary_token/versions/SimplifiedDeflationaryToken_v1.sol
new file mode 100755
index 00000000..89fb2419
--- /dev/null
+++ b/contracts/simplified_deflationary_token/versions/SimplifiedDeflationaryToken_v1.sol
@@ -0,0 +1,57 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+/// @custom:version the transfer amount and fees are wrongly managed, the fees are not deducted from the sender but at the same time the owner receives the right fee amount (token duplication).
+contract SimplifiedDeflationaryToken {
+    mapping(address => uint256) public balances;
+    mapping(address => bool) public isExcludedFromFee;
+
+    uint256 public totalSupply = 1000000 * (10**18);
+    uint256 public transactionFeePercent = 10;
+
+    address public owner;
+
+    event Transfer(address indexed from, address indexed to, uint256 value);
+
+    constructor() {
+        owner = msg.sender;
+        balances[owner] = totalSupply;
+        isExcludedFromFee[owner] = true;
+    }
+
+    function transfer(address to, uint256 amount) public returns (bool) {
+        require(balances[msg.sender] >= amount, "Insufficient balance");
+
+        uint256 fee = 0;
+        if (!isExcludedFromFee[msg.sender]) {
+            fee = calculateFee(amount);
+            amount = amount - fee; 
+            balances[owner] += fee;
+        }
+
+        balances[msg.sender] -= amount;
+        balances[to] += amount;
+
+        emit Transfer(msg.sender, to, amount);
+
+        return true;
+    }
+
+    function calculateFee(uint256 amount) public view returns (uint256) {
+        return (amount * transactionFeePercent) / 100;
+    }
+
+    function excludeFromFee(address account) public {
+        require(msg.sender == owner, "Only owner can exclude from fee");
+        isExcludedFromFee[account] = true;
+    }
+
+    function includeInFee(address account) public {
+        require(msg.sender == owner, "Only owner can include in fee");
+        isExcludedFromFee[account] = false;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return balances[account];
+    }
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/versions/SimplifiedDeflationaryToken_v2.sol b/contracts/simplified_deflationary_token/versions/SimplifiedDeflationaryToken_v2.sol
new file mode 100755
index 00000000..4f2a3a36
--- /dev/null
+++ b/contracts/simplified_deflationary_token/versions/SimplifiedDeflationaryToken_v2.sol
@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+/// @custom:version the deflationary property is not well implemented, when we make a transfer with less than 10 tokens, no fees are charged.
+contract SimplifiedDeflationaryToken {
+    mapping(address => uint256) public balances;
+    mapping(address => bool) public isExcludedFromFee;
+
+    uint256 public totalSupply = 1000000 * (10**18);
+    uint256 public transactionFeePercent = 10;
+
+    address public owner;
+
+    event Transfer(address indexed from, address indexed to, uint256 value);
+
+    constructor() {
+        owner = msg.sender;
+        balances[owner] = totalSupply;
+        isExcludedFromFee[owner] = true;
+    }
+
+    function transfer(address to, uint256 amount) public returns (bool) {
+        require(balances[msg.sender] >= amount, "Insufficient balance");
+
+        uint256 fee = 0;
+        if (!isExcludedFromFee[msg.sender]) {
+            fee = calculateFee(amount);
+            balances[owner] += fee;
+        }
+
+        balances[msg.sender] -= amount;
+        balances[to] += (amount - fee);
+
+        emit Transfer(msg.sender, to, amount);
+
+        return true;
+    }
+
+    function calculateFee(uint256 amount) public view returns (uint256) {
+        return (amount * transactionFeePercent) / 100;
+    }
+
+    function excludeFromFee(address account) public {
+        require(msg.sender == owner, "Only owner can exclude from fee");
+        isExcludedFromFee[account] = true;
+    }
+
+    function includeInFee(address account) public {
+        require(msg.sender == owner, "Only owner can include in fee");
+        isExcludedFromFee[account] = false;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return balances[account];
+    }
+}
\ No newline at end of file
diff --git a/contracts/simplified_deflationary_token/versions/SimplifiedDeflationaryToken_v3.sol b/contracts/simplified_deflationary_token/versions/SimplifiedDeflationaryToken_v3.sol
new file mode 100755
index 00000000..df2d5153
--- /dev/null
+++ b/contracts/simplified_deflationary_token/versions/SimplifiedDeflationaryToken_v3.sol
@@ -0,0 +1,58 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+/// @custom:version conforming to specification.
+contract SimplifiedDeflationaryToken {
+    mapping(address => uint256) public balances;
+    mapping(address => bool) public isExcludedFromFee;
+
+    uint256 public totalSupply = 1000000 * (10**18);
+    uint256 public transactionFeePercent = 10;
+
+    address public owner;
+
+    event Transfer(address indexed from, address indexed to, uint256 value);
+
+    constructor() {
+        owner = msg.sender;
+        balances[owner] = totalSupply;
+        isExcludedFromFee[owner] = true;
+    }
+
+    function transfer(address to, uint256 amount) public returns (bool) {
+        require(balances[msg.sender] >= amount, "Insufficient balance");
+        require(amount > 0, "Cannot send 0 Token");
+
+        uint256 fee = 0;
+        if (!isExcludedFromFee[msg.sender]) {
+            fee = calculateFee(amount);
+            balances[owner] += fee;
+        }
+
+        balances[msg.sender] -= amount;
+        balances[to] += (amount - fee);
+
+        emit Transfer(msg.sender, to, amount);
+
+        return true;
+    }
+
+    function calculateFee(uint256 amount) public view returns (uint256) {
+        uint256 fee = (amount * transactionFeePercent) / 100;
+        return fee == 0 ? 1 : fee;
+    }
+
+    function excludeFromFee(address account) public {
+        require(msg.sender == owner, "Only owner can exclude from fee");
+        isExcludedFromFee[account] = true;
+    }
+
+    function includeInFee(address account) public {
+        require(msg.sender == owner, "Only owner can include in fee");
+        isExcludedFromFee[account] = false;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return balances[account];
+    }
+}
\ No newline at end of file