René's URL Explorer Experiment

{"@context":"https://schema.org","@type":"DiscussionForumPosting","headline":"Missing spec","articleBody":"Missing specs ensures that we can have more than one voter\r\nBuggy contract enforce only one voter, the cheater that can vote for himself\r\n_Existing oneCanVote did not catch this bug_\r\n\r\nMissing spec : #18   \r\n\r\nA run of the new BordaMissingRule.spec on the original Borda.sol that is verified\r\nhttps://prover.certora.com/output/88083/ee33b030b2f346968a6e75a7ebd389bc/?anonymousKey=832264b21688ea4c31b2c6bcd26e20011b251bb4\r\n\r\nA run of Borda.spec on BordaNewBug.sol showing the existing spec misses the bug\r\nhttps://prover.certora.com/output/88083/1d302e93e9ea43ba8fe8366f86984e71/?anonymousKey=ce8882019f6167ff1ff0243fcd6708ca9654e889\r\n\r\n\r\nA run of BordaMissingRule.spec on BordaNewBug.sol showing your rule catches the bug\r\nhttps://prover.certora.com/output/88083/6ee308b0f0c14987aaf5c215e10874e2/?anonymousKey=0f97fbf396b84bd42090d0ad47b2144c341c1d80","author":{"url":"https://github.com/zapaz","@type":"Person","name":"zapaz"},"datePublished":"2023-09-28T11:58:29.000Z","interactionStatistic":{"@type":"InteractionCounter","interactionType":"https://schema.org/CommentAction","userInteractionCount":0},"url":"https://github.com/19/tutorials-code/issues/19"}