# 1.3. Introduction to formal verification¶

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()
);
```

```    // 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();

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();

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()
);
}
```