3.3. Reward Challenge : Missing Spec bounty#


Find a buggy version of Borda that is not caught by the given rules. The buggy version must implement the IBorda interface and the bug must be a high severity bug so that there is an effect on the outcome of the voting.

Challenge rules#

To submit a Missing Spec you will need the following:

  1. An original buggy implementation of IBorda, named BordaNewBug.sol such that:

    • The bug in BordaNewBug.sol is not caught by the current set of rules

    • The bug is not caught by previously reported missing rules

    • The bug has an impact on the voting

    • The buggy BordaNewBug.sol is a full implementation of the IBorda interface and is implemented with the _points and _voted mappings as in the original Borda.sol

    • The buggy BordaNewBug.sol may contain additional functions and fields

  2. A rule or invariant named BordaMissingRule, placed in a file called BordaMissingRule.spec, that:

    • Catches the bug by showing a violation on the new buggy version BordaNewBug.sol

    • Passes on the original Borda.sol implementation, demonstrating that it is a property of a correct implementation of Borda

  3. The following reports:

    • A run of the new BordaMissingRule.spec on the original Borda.sol that is verified

    • A run of Borda.spec on BordaNewBug.sol showing the existing spec misses the bug

    • Reports of all previously acknowledged bounty specs on BordaNewBug.sol, these specs will be found in the bounty_specs folder

    • A run of BordaMissingRule.spec on BordaNewBug.sol showing your rule catches the bug


First, prepare a PR for the Certora Tutorials Code repository containing the two new files BordaNewBug.sol and BordaMissingRule.spec. Second, in create an Issue in Certora Tutorials Code repository containing links to the PR and to all the report runs mentioned above.


  • Per original missing spec: 200 USDC

  • Total Reward: 1000 USDC (for the first five acknowledged instances)


This challenge has finished on Oct 2nd, 2023.

There are more than five missing rules, check your solution against bounty_specs folder