Getting started with the Certora Prover¶

Simple Voting Contract¶

Simple voting contract with injected bug¶

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

/// @title A simple voting contract
contract Voting {

    // `_hasVoted[user]` is true if the user voted.
    mapping(address => bool) public hasVoted;

    uint256 public votesInFavor;  // How many in favor
    uint256 public votesAgainst;  // How many opposed
    uint256 public totalVotes;  // Total number voted

    function vote(bool isInFavor) external {
        // The prover ignores reverted computation paths
        require(!hasVoted[msg.sender]);
        hasVoted[msg.sender] = true;

        totalVotes = 1;
        if (isInFavor) {
            votesInFavor += 1;
        } else {
            votesAgainst += 1;
        }
    }
}

Running the Certora Prover

The above contract contains a bug. We will try to find it with the help of the Certora Prover. For that we need two things:

a .spec file that contains the specification we want to verify.

a .conf file that contains the configuration we can use to conveniently run the prover.

First spec¶

A spec is written in the Certora Verification Language (CVL).

VotingBug.spec¶

/* A simple rule for the Voting contract */
methods {
    // Declares the getter for the public state variables as `envfree`
    function totalVotes() external returns (uint256) envfree;
}

/// @title Integrity of vote
rule voteIntegrity(env e) {
    uint256 votedBefore = totalVotes();

    bool isInFavor;
    vote(e, isInFavor);

    assert (
        totalVotes() > votedBefore,
        "totalVotes increases after voting"
    );
}

First conf¶

The configuration for the Prover.
Uses the json5 format.
The configuration can be overridden in the command line.

VotingBug.conf¶

{
    "files": ["src/VotingBug.sol:Voting"],
    "verify": "Voting:certora/specs/VotingBug.spec",
    "msg": "A simple rule example",
    "server": "production",
    // To use a specific Solidity compiler:
    // "solc": "<path-to-compiler>
    // Or add to the command line: --solc <path-to-compiler>
    // "solc": "solc" for solc-select,
    "server": "production"
}

Exercises¶

Task 1: Run the spec¶

To run the spec, execute the following command from the root directory of this repo:
```
certoraRun certora/confs/VotingBug.conf
```
You will see the run appear in the Job List.
Results link: rule report.

Tip

You can override the configuration from the command line. For example, the following will use a specific Solidity compiler:

certoraRun certora/confs/VotingBug.conf --solc ~/solc0.8.20

Task 2: Fix the bug¶

You will see two rules appearing on the left side bar:
- envfreeFuncsStaticCheck: this checks whether totalVotes() can be declared as envfree, that is not depending on the environment, like block.timestamp``or ``msgSender.
- voteIntegrity: this is failing, can you find out why?
Fix the bug and rerun the certoraRun command. You should get a report that looks like the fixed rule report.

Task 3: Write a rule to verify the property¶

Property: sum of votes in favor and votes against equals total votes.