Missing specs ensures that we can have more than one voter
Buggy contract enforce only one voter, the cheater that can vote for himself
Existing oneCanVote did not catch this bug
Missing spec : #18
A run of the new BordaMissingRule.spec on the original Borda.sol that is verified
https://prover.certora.com/output/88083/ee33b030b2f346968a6e75a7ebd389bc/?anonymousKey=832264b21688ea4c31b2c6bcd26e20011b251bb4
A run of Borda.spec on BordaNewBug.sol showing the existing spec misses the bug
https://prover.certora.com/output/88083/1d302e93e9ea43ba8fe8366f86984e71/?anonymousKey=ce8882019f6167ff1ff0243fcd6708ca9654e889
A run of BordaMissingRule.spec on BordaNewBug.sol showing your rule catches the bug
https://prover.certora.com/output/88083/6ee308b0f0c14987aaf5c215e10874e2/?anonymousKey=0f97fbf396b84bd42090d0ad47b2144c341c1d80
Missing specs ensures that we can have more than one voter
Buggy contract enforce only one voter, the cheater that can vote for himself
Existing oneCanVote did not catch this bug
Missing spec : #18
A run of the new BordaMissingRule.spec on the original Borda.sol that is verified
https://prover.certora.com/output/88083/ee33b030b2f346968a6e75a7ebd389bc/?anonymousKey=832264b21688ea4c31b2c6bcd26e20011b251bb4
A run of Borda.spec on BordaNewBug.sol showing the existing spec misses the bug
https://prover.certora.com/output/88083/1d302e93e9ea43ba8fe8366f86984e71/?anonymousKey=ce8882019f6167ff1ff0243fcd6708ca9654e889
A run of BordaMissingRule.spec on BordaNewBug.sol showing your rule catches the bug
https://prover.certora.com/output/88083/6ee308b0f0c14987aaf5c215e10874e2/?anonymousKey=0f97fbf396b84bd42090d0ad47b2144c341c1d80