diff --git a/lesson3_violations/Borda/Borda.conf b/lesson3_violations/Borda/Borda.conf
index 0a46999..b45a8d2 100644
--- a/lesson3_violations/Borda/Borda.conf
+++ b/lesson3_violations/Borda/Borda.conf
@@ -1,9 +1,11 @@
 {
   "files": [
-    "Borda.sol:Borda"
+    "BordaNewBug.sol:Borda"
   ],
   "verify": "Borda:Borda.spec",
-  "send_only": false,
+  "send_only": true,
+  "optimistic_loop": true,
+  "loop_iter": "101",
   "msg": "Verification of Borda",
-  "rule_sanity" : "advanced"
+  "rule_sanity" : "basic"
 }
diff --git a/lesson3_violations/Borda/Borda.spec b/lesson3_violations/Borda/Borda.spec
index d0c8ace..5b2d9ce 100644
--- a/lesson3_violations/Borda/Borda.spec
+++ b/lesson3_violations/Borda/Borda.spec
@@ -217,6 +217,10 @@ ghost mapping(address => uint256) points_mirror {
  init_state axiom forall address c. points_mirror[c] == 0;
 } 
 
+ghost mapping(address => bool) voted_mirror {
+	init_state axiom forall address c. !voted_mirror[c];
+}
+
 ghost mathint countVoters {
     init_state axiom countVoters == 0;
 }
@@ -235,7 +239,8 @@ hook Sload uint256 curr_point _points[KEY address a]  STORAGE {
 }
 
 hook Sstore _voted[KEY address a] bool val (bool old_val) STORAGE {
-  countVoters = countVoters +1;
+  countVoters = countVoters + 1;
+  voted_mirror[a] = val;
 }
 
 
@@ -253,4 +258,40 @@ rule resolvabilityCriterion(address f, address s, address t, address tie) {
   Each voter contribute a total of 6 points, so the sum of all points is six time the number of voters 
 */
 invariant sumOfPoints() 
-    sumPoints == countVoters * 6; 
\ No newline at end of file
+    sumPoints == countVoters * 6;
+
+
+// ADDED RULES:
+
+invariant votedFunctionIsVotedMapping()
+	forall address a. voted_mirror[a] == voted(a);
+
+rule preferLastVotedHigh(address f, address s, address t) {
+	env e;
+    uint prev_points = points(winner());
+	vote(e, f, s, t);
+	address w = winner();
+	assert (points(w) == points(f) => points(w) == prev_points || w == f);
+	assert (points(w) == points(s) => points(w) == prev_points || w == f || w == s);
+	assert (points(w) == points(t) => points(w) == prev_points || w == f || w == s || w == t);
+}
+
+rule onlyVotingCanChangeTheWinner(env e, method m){
+    address winnerBefore = winner();
+    calldataarg args; 
+    m(e, args);
+    address winnerAfter = winner();
+    assert m.selector != sig:vote(address,address,address).selector => winnerAfter == winnerBefore, "The winner can be changed only after voting";
+}
+
+rule viewNeverRevert() {
+    address _points;
+    address _voted;
+
+    winner@withrevert();
+    assert !lastReverted;
+    points@withrevert(_points);
+    assert !lastReverted;
+    voted@withrevert(_voted);
+    assert !lastReverted;
+}
diff --git a/lesson3_violations/Borda/BordaMissingRule.spec b/lesson3_violations/Borda/BordaMissingRule.spec
new file mode 100644
index 0000000..4a7e242
--- /dev/null
+++ b/lesson3_violations/Borda/BordaMissingRule.spec
@@ -0,0 +1,28 @@
+methods {
+    function points(address) external returns uint256  envfree;
+    function vote(address,address,address) external;
+    function voted(address) external returns bool  envfree;
+    function winner() external returns address  envfree;
+}
+
+ghost mathint countVoters {
+	init_state axiom countVoters == 0;
+}
+
+ghost mathint sumPoints {
+	init_state axiom sumPoints == 0;
+}
+
+hook Sstore _points[KEY address a] uint256 new_points (uint256 old_points) STORAGE {
+	sumPoints = sumPoints + new_points - old_points;
+}
+
+hook Sstore _voted[KEY address a] bool val (bool old_val) STORAGE {
+	countVoters = countVoters + (val ? 1 : 0) - (old_val ? 1 : 0);
+}
+
+invariant sumOfPoints() 
+    sumPoints == countVoters * 6;
+
+
+
diff --git a/lesson3_violations/Borda/BordaNewBug.sol b/lesson3_violations/Borda/BordaNewBug.sol
new file mode 100644
index 0000000..28c8bfc
--- /dev/null
+++ b/lesson3_violations/Borda/BordaNewBug.sol
@@ -0,0 +1,57 @@
+pragma solidity ^0.8.0;
+import "./IBorda.sol";
+
+contract Borda is IBorda{
+
+    // The current winner
+    address public _winner;
+
+    // A map storing whether an address has already voted. Initialized to false.
+    mapping (address => bool)  _voted;
+
+    // Points each candidate has recieved, initialized to zero.
+    mapping (address => uint256) _points;
+
+    // current maximum points of all candidates.
+    uint256 public pointsOfWinner;
+
+    constructor() {
+        // many, many votes there
+        voteTo(address(0xaa), 600);
+
+        // now, make 100 touches to the _voted mapping, clearing it in the end
+        for (int i = 0; i < 99; i++)
+            _voted[address(0xaa)] = true;
+        _voted[address(0xaa)] = false;
+    }
+
+    function vote(address f, address s, address t) public override {
+        require(!_voted[msg.sender], "this voter has already cast its vote");
+        require( f != s && f != t && s != t, "candidates are not different");
+        _voted[msg.sender] = true;
+        voteTo(f, 3);
+        voteTo(s, 2);
+        voteTo(t, 1);
+    }
+
+    function voteTo(address c, uint256 p) private {
+        //update points
+        _points[c] = _points[c]+ p;
+        // update winner if needed
+        if (_points[c] > _points[_winner]) {
+            _winner = c;
+        }
+    }
+
+    function winner() external view override returns (address) {
+        return _winner;
+    }
+
+    function points(address c) public view override returns (uint256) {
+        return _points[c];
+    }
+
+    function voted(address x) public view override returns(bool) {
+        return _voted[x];
+    }
+}