3. Understanding violations

This lesson’s goal is to familiarize you with the Prover’s counter-examples, and to practice bug finding using these counter-examples.

The lesson is composed of two independent examples. The first example, focuses on mistakes in the spec, while the second example focuses on bugs in Solidity. In both cases, the rule report aids in understanding the root cause of the problem.

After each example are hints in case you get stuck. The lesson is concluded with a reward challenge.

1. Fixing ERC20 spec - focuses on mistakes in specs for ERC20

2. Borda count election - focuses on bugs in Solidity code for an election

3. Reward Challenge : Missing Spec bounty - a reward challenge