1.3. Introduction to formal verification

Formal verification is about proving correctness of algorithms using formal methods. You can read more about this on Wikipedia - Formal verification. Here we will instead show an example.

Example:

Consider the Birth Months riddle (from Braingle), reproduced below, we will use formal verification to find a solution, and also to prove that this solution is unique.

Four sisters, Sara, Ophelia, Nora, and Dawn, were each born in a different one of
the months September, October, November, and December.

"This is terrible," said Ophelia one day. "None of us have an initial that matches
the initial of her birth month."

"I don't mind at all," replied the girl who was born in September.

"That's easy for you to say," said Nora. "It would at least be cool if the initial
of my birth month was a vowel, but no."

In which month was each girl born?

Finding a solution

Step 1

The first step is to translate the riddle into a more formal form. Here is a description of the months as numbers in CVL:

// The months
definition September() returns uint8 = 9;
definition October() returns uint8 = 10;
definition November() returns uint8 = 11;
definition December() returns uint8 = 12;

We use the sisters’ names as parameters (whose value is the birth month of that sister):

rule sistersBirthMonths(
    uint8 Sara,
    uint8 Ophelia,
    uint8 Nora,
    uint8 Dawn
) {

Step 2

We add all the data in the riddle. For example, saying that Sarah was born in either September, October, November or December is:

    require Sara >= September() && Sara <= December();

Each sister was born in one of the four months:

    require Sara >= September() && Sara <= December();
    require Ophelia >= September() && Ophelia <= December();
    require Nora >= September() && Nora <= December();
    require Dawn >= September() && Dawn <= December();

Each sister’s initial is different from the initial of her birth month:

    require (
        Sara != September() &&
        Ophelia != October() &&
        Nora != November() &&
        Dawn != December()
    );

Clues about Ophelia and Nora:

    // Ophelia is not the girl who was born in September
    require Ophelia != September();

    // Nora is not the girl who was born in September
    require Nora != September();

    // Nora's birth month does not start with a vowel
    require Nora != October();

The sisters were born on different months:

    require (
        Sara != Ophelia &&
        Sara != Nora &&
        Sara != Dawn &&
        Ophelia != Nora &&
        Ophelia != Dawn &&
        Nora != Dawn
    );

Step 3

We ask for a solution that satisfies all these requirements, using the CVL statement:

    satisfy true;

Step 4

The entire rule is found in sisters.spec. Running the Certora Prover on this rule would provide a solution (if one exists). You will learn about running the Certora Prover in Lesson 2 Getting Started, in particular in Section Running the Prover. For now we will provide the answer given by the Certora Prover, which looks like this:

*----------------------------------- ... --------------*
|Rule name          |Verified     |        |Local vars |
|-------------------|-------------|- ... --|-----------|
|sistersBirthMonths |Not violated |        |Dawn=9     |
|                   |             |        |Nora=12    |
|                   |             |        |Ophelia=11 |
|                   |             |        |Sara=10    |
|                   |             |        | ...       |
*----------------------------------- ... --------------*

So, Sara was born in October, Ophelia was born in November, Nora was born in December, and Dawn was born in September.

If you want to run the Certora Prover yourself

Go to the folder lesson1_prerequisites/formal_verification/ and enter:

certoraRun Empty.sol --verify Empty:sisters.spec --solc solc8.0 --rule sistersBirthMonths

Proving the solution is unique

To prove the solution is unique, we build another rule, called solutionIsUnique, containing all the requirements above. However, instead of the satisfy true; statement we add the assertion that the only solution is the one we found:

    assert (
        Sara == October() &&
        Ophelia == November() &&
        Nora == December() &&
        Dawn == September()
    );

If the assertion is violated, the Prover will provide a counter-example to the assertion. Such a counter-example would be another solution, showing the previous solution is not unique.

Running the Certora Prover on this new rule simply returns:

*---------------------------------- ...
|Rule name        |Verified     |
|-----------------|-------------|-- ...
|solutionIsUnique |Not violated |

Which proves the solution is unique.

To run the Certora Prover on this rule

Go to the folder lesson1_prerequisites/formal_verification/ and enter:

certoraRun Empty.sol --verify Empty:sisters.spec --solc solc8.0 --rule solutionIsUnique

This rule is also found at sisters.spec. Here is the complete rule:

/// @title Verify that the solution is unique
rule solutionIsUnique(
    uint8 Sara,
    uint8 Ophelia,
    uint8 Nora,
    uint8 Dawn
) {
    // Each sister was born in one of the four months
    require Sara >= September() && Sara <= December();
    require Ophelia >= September() && Ophelia <= December();
    require Nora >= September() && Nora <= December();
    require Dawn >= September() && Dawn <= December();

    // "None of us have an initial that matches the initial of her birth month."
    require (
        Sara != September() &&
        Ophelia != October() &&
        Nora != November() &&
        Dawn != December()
    );

    // Ophelia is not the girl who was born in September
    require Ophelia != September();

    // Nora is not the girl who was born in September
    require Nora != September();

    // Nora's birth month does not start with a vowel
    require Nora != October();

    // The sisters were born on different months
    require (
        Sara != Ophelia &&
        Sara != Nora &&
        Sara != Dawn &&
        Ophelia != Nora &&
        Ophelia != Dawn &&
        Nora != Dawn
    );

    assert (
        Sara == October() &&
        Ophelia == November() &&
        Nora == December() &&
        Dawn == September()
    );
}