A look into formal verification of smart contracts using Certora
Tags: ethereum, formalverification, smartcontracts
Published: 2022-12-02 18:27:40

---
title: A look into formal verification of smart contracts using Certora
published: true
description: A personal overview of how smart contract formal verification works using Certora.
tags: 
- ethereum
- formalverification
- smartcontracts
cover_image: https://dev-to-uploads.s3.amazonaws.com/uploads/articles/yrd5wbcc2y4odd7y8ie6.jpg
# published_at: 2022-12-02 18:00 +0000
---

*This is an overview of how smart contract formal verification works using Certora. It is definitely not an in-depth review of either Certora or formal verification techniques, of which I'm not an expert. Special thanks to Shelly Grossman and Nurit Dor from Certora for reviewing this article.*

In software, we rely on automated tests for checking if our code matches our expectations. Testing helps guide development and uncover bugs, but a green test run only means that our tests haven't stumbled upon any issues for the scenario we chose. It certainly does not mean that our code is correct.

Formal verification is a more powerful method that can mathematically prove that our code adheres to a specification. As described in ["Formal verification of smart contracts"](https://ethereum.org/en/developers/docs/smart-contracts/formal-verification/) on ethereum.org:

> Formal verification refers to the process of evaluating the correctness of a system with respect to a formal specification. In simpler terms, formal verification allows us to check if the behavior of a system satisfies some requirements (i.e., it does what we want).
>
> When implemented in smart contracts, formal verification can prove that a contract's business logic meets a predefined specification. Compared to other methods for assessing the correctness of contract code, such as testing, formal verification gives stronger guarantees that a smart contract is functionally correct.

Given how critical blockchain applications can be, smart contracts are fertile ground for formal verification. The deterministic and bounded execution in the EVM also make formal methods easier to apply. 

[**Certora**](https://certora.com/) is one of the players in this field, offering a platform for formal verification using a proprietary spec language, [Certora Verification Language](https://docs.certora.com) or CVL. These specifications are uploaded, along with the smart contract code, to a proprietary cloud-based platform for verification. Given how resource-intensive formal proofs can be, these are not suited for running locally.

![Example spec run for an ERC20Permit contract](https://i.imgur.com/WCPh7AM.png)

Under the hood, Certora generates a set of constraints out of decompiled EVM bytecode and the CVL specs, which are then passed through an SMT solver. But this is out of scope for this article: refer to their [whitepaper](https://medium.com/certora/certora-technology-white-paper-cae5ab0bdf1) for an in-depth explanation of how it works. So let's jump directly onto the formal specs.

## What does a spec look like in CVL?

The main building block of CVL is a [**rule**](https://docs.certora.com/en/latest/docs/user-guide/bank/index.html#rules-in-the-certora-verification-language). Rules are structured as [Hoare triples](https://en.wikipedia.org/wiki/Hoare_logic):
- A **precondition** defines the current state of the contract
- An **operation** is executed on the contract
- A **postcondition** asserts properties on the resulting state

As an example, taken from [Certora's tutorials](https://github.com/Certora/Tutorials/tree/master/01.Lesson_GettingStarted/BankLesson1) (most examples in this article will be copied or adapted from it), let's say we have a Bank contract that receives and stores deposits from users. We want to verify that, after every deposit, the total funds deposited are greater than every individual user balance.

```
rule totalFundsAfterDeposit(env e, uint256 amount) {
  uint256 userFundsBefore = getFunds(e, e.msg.sender);
  uint256 totalBefore = getTotalFunds(e);
    
  require totalBefore >= userFundsBefore;
	
  deposit(e, amount);
		
  assert getTotalFunds(e) >= getFunds(e, e.msg.sender);
}
```

Note the `require` precondition before the action. Preconditions are not just used to set the stage: they are needed to restrict the space of valid states for a contract. Otherwise, the prover assumes that any state is possible when trying to prove the rule, **even unreacheable ones**.

The power of this spec is that no matter the initial set of balances, the amount deposited, or the user who sends the deposit, we know that this condition will hold. In a unit test, we'd only be testing this for a specific initial state, with a specific deposit from a specific user. A formal spec proves **this property holds for every single input** on **every initial state** covered by the precondition.

CVL also lets us prove that properties hold no matter what function is called. Much like we are proving our property holds for any deposit amount, we can also **prove it over any function call on the contract**:

```
rule totalFundsAfterAnyAction(env e, method f) {
  uint256 userFundsBefore = getFunds(e, e.msg.sender);
  uint256 totalBefore = getTotalFunds(e);
    
  require totalBefore >= userFundsBefore;
	
  calldataargs args;
  f(e, args);
		
  assert getTotalFunds(e) >= getFunds(e, e.msg.sender);
}
```

Note that we are checking that, given any valid initial state and any action executed, the resulting state is still valid. What we are actually doing here is checking that an [**invariant**](https://en.wikipedia.org/wiki/Invariant_(mathematics)#Invariants_in_computer_science) is preserved: a property that should always be true for a given contract. Invariants are a powerful tool when describing a system, and CVL has [a native building block](https://docs.certora.com/en/latest/docs/user-guide/bank/index.html#invariants) for expressing them:

```
invariant totalFundsGreaterThanAnyUser()
    forall address user. getTotalFunds() >= getFunds(user)
```

When presented with an invariant, the prover will use induction to check it, by verifying that:
- The property holds once the contract is constructed
- Assuming that the property holds (precondition), invoking any function (operation), the property still holds (postcondition)

## Pushing the limits

Predicating over all possible values is a powerful primitive, but it has its limitations. For instance, we cannot perform aggregations. Following the previous example, the invariant that _total funds are the sum of each individual user funds_ cannot be expressed in CVL.

Fortunately, CVL introduces another concept that allows us to handle these more complex expressions: [**ghosts**](https://docs.certora.com/en/latest/docs/cvl/ghosts.html). Broadly speaking, a **ghost is a variable or function** defined on CVL that **allows collecting or injecting information into contract "executions"** during verifications.

This is easier to understand [with an example](https://github.com/Certora/Tutorials/blob/2d12eecd3627d220b5f2839aa4d1035345a7ac61/07.Lesson_InductiveReasoning/Invariants/Bank/invariant.spec#L25-L48). To capture the invariant that _total funds are the sum of each individual user funds_, we can declare a ghost that "accumulates" each user deposit **whenever the funds mapping variable is updated** on the contract, and then compares that to the reported value:

```
ghost sumOfAllFunds() returns uint256{
  init_state axiom sumOfAllFunds() == 0;
}

hook Sstore funds[KEY address user] uint256 newBalance (uint256 oldBalance) STORAGE {
  havoc sumOfAllFunds assuming sumOfAllFunds@new() == sumOfAllFunds@old() + newBalance - oldBalance;
}
```

The snippet above is declaring a function `sumOfAllFunds` that returns a number, with an initial state of zero, and **gets updated whenever there's a write to storage** at the `funds` mapping, using both the old and new values of the sum and the entry in the mapping. We can now write an invariant that uses this ghost function and matches it to the returned value from the contract:

```
invariant totalFunds_GE_to_sum_of_all_funds()
  getTotalFunds() >= sumOfAllFunds()
```

In the snippet above, `getTotalFunds` is a call to the contract, which is compared to the ghost `sumOfAllFunds` value that we hold in our spec.

Hooks can also be defined on reads, not just writes. This lets us **inject preconditions upon every value that is read out of storage**, which can be used to further narrow down the state of the contract that we are verifying.

Hooks are an interesting tool for enhancing the expresiveness of proofs, but they come at a disadvantage. While rules and invariants are predicated on the external interface of the contract, hooks **bind a spec to implementation details**. This means a spec that is valid for an implementation may not work on a different one even if they have the same interface.

## Loops and unrolls

Loops are particularly tricky when we have to prove the correctness of an algorithm. The Hoare approach is to devise a [_loop invariant_](https://en.wikipedia.org/wiki/Loop_invariant), a property that holds across each execution of the loop, and that can be used to prove that the loop finishes and that yields a particular end state.

However, coming up with a loop invariant [is not easy](https://www.cs.scranton.edu/~mccloske/courses/cmps144/invariants_lec.html), and it's much harder to do in an automated way. Therefore, the Certora prover works by **[unrolling loops](https://docs.certora.com/en/latest/docs/prover/approx/loops.html) a configurable number of times**. This means that loops get converted into N copies of the body of the loop, and treated as regular non-iterative code.

Since unrolling a loop a fixed number of times can hide bugs, by default the prover will alert if the loop would have run more times than it was unrolled. But since this is usually the case, the prover is typically run in [optimistic-loop](https://docs.certora.com/en/latest/docs/prover/cli/options.html#options-regarding-source-code-loops) mode, which removes these alerts - at the cost of potentially hiding bugs.


## Dealing with multiple contracts

A protocol is rarely composed of a single contract. Even though CVL seems to be geared towards testing individual contract properties, it also has tools for managing multiple contracts.

The simplest option is **[linking](https://docs.certora.com/en/latest/docs/user-guide/multicontract/index.html#working-with-known-contracts) one contract to another**. When running the prover, we can tell it that a field in a contract refers to an instance of another known contract. And CVL lets us refer to all registered contracts when writing our rules.

In [this example](https://docs.certora.com/en/latest/docs/user-guide/multicontract/index.html#working-with-known-contracts) from Certora's documentation, we are indicating that the `asset` field in the `Pool` contract refers to an instance of the `ERC20` contract:

```solidity
import "../ERC20.sol";

contract Pool {
  ERC20 asset;
}
```

```shell
$ certoraRun contracts/Pool.sol contracts/ERC20.sol --link Pool:asset=ERC20 ...
```

In case we have **multiple implementations** for a given contract, we can register them all and have the prover try every known implementation that satisfies the required interface. In [this example](https://docs.certora.com/en/latest/docs/user-guide/multicontract/index.html#erc20-dispatcher), registering the ERC20 interface methods with the `DISPATCHER` keyword instructs the prover to try every ERC20 implementation we have in stock.

```
methods {
  totalSupply()                         returns (uint256) => DISPATCHER(true)
  balanceOf(address)                    returns (uint256) => DISPATCHER(true)
  allowance(address,address)            returns (uint)    => DISPATCHER(true)
  approve(address,uint256)              returns (bool)    => DISPATCHER(true)
  transfer(address,uint256)             returns (bool)    => DISPATCHER(true)
  transferFrom(address,address,uint256) returns (bool)    => DISPATCHER(true)
}
```

This way, whenever our `Pool` contract being verified makes a call to an ERC20 method, the prover will look for every ERC20 implementation we have and try it.

But things get messier when [**working with unknown contracts**](https://docs.certora.com/en/latest/docs/user-guide/multicontract/index.html#working-with-unknown-contracts). What happens if we do not know what will be the instance that our contract will be working with? Following the previous example, what if we want to verify our system will work properly with any ERC20 implementation, even one we did not anticipate or a maliciously crafted one?

As we saw in the example above, the prover works on a method-by-method basis when dealing with external calls. For each method called by the contract being verified, we can **define how we expect that call to behave**. This is referred to as [summaries](https://docs.certora.com/en/latest/docs/cvl/methods.html#summary-types) in CVL.

For example, [view functions](https://docs.certora.com/en/latest/docs/cvl/methods.html#view-summaries-always-constant-per-callee-constant-and-nondet) can be annotated as returning anything from a constant to a completely non-deterministic value. Here's an example [taken from OpenZeppelin contracts](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/2c5194f3f13d3f9ce301d8100b9f5fe0cec6d7d8/certora/specs/GovernorPreventLateQuorum.spec#L43-L76):

```
methods {
  hashProposal(...) returns (uint256) => NONDET
  hashOperationBatch(...) => DISPATCHER(true)
  executeBatch(...) => CONSTANT
}
```

The main challenge is [dealing with non-view functions](https://docs.certora.com/en/latest/docs/cvl/methods.html#havoc-summaries-havoc-all-and-havoc-ecf). The default behavior of the prover is to assume that **an external call can alter all state on every contract _but_ the caller**, noted as `HAVOC_ECF`. This can lead to state changes in external contracts that are unreachable, making verification more difficult. Furthermore, it assumes that the call is non-reentrant, which in reality is [a frequent source of attacks](https://github.com/pcaversaccio/reentrancy-attacks). This last issue can be avoided by indicating that calls _can_ re-enter, noted as `HAVOC_ALL`, but this means that **an external call can mutate any state in any contract, caller included**. This leaves the contract being verified in a state where we don't know anything about it after an external call is made. This severely limits what we can prove.

A more reasonable approach is to assume that the callee _can_ call back into any contract, but restrict it to actual method calls, instead of arbitrary state changes. However, this needs to be handled manually, by **[writing a contract that calls into each method](https://docs.certora.com/en/latest/docs/user-guide/multicontract/index.html#designing-flexible-dispatchees)** based on an arbitrary parameter:

```solidity
contract Receiver is ArbitraryValues {
  ERC20 asset;
  function exec() external {
    uint callback = arbitraryUint();
    if (callback == 0) 
      asset.approve(arbitraryAddress(), arbitraryUint());
    else if (callback == 1) 
      asset.transfer(arbitraryAddress(), arbitraryUint());
    else if (callback == 2) 
      asset.transferFrom(arbitraryAddress(), arbitraryAddress(), arbitraryUint());
  }
}
```

The `ArbitraryValues` base contract provides a set of `arbitraryValue()` methods that return a non-determistic value whenever we need it. These are used to pick both the method to be called and its arguments.

Note that this approach **does not cover all possible interactions**, since we are executing just a single callback, whereas there could be multiple reentrant calls.

One last approach to working with unknown contract implementations is to **map a method to a function in CVL**. Whenever that method is called from the contract being verified, the function will be called instead. This allows us to prove that our contract works as expected _assuming_ that the callee adheres to the spec that has been defined. Note that the callee is not verified here, since there is no implementation to verify it against!

## What are the best use cases for CVL?

After going through scenarios where we push the limits of CVL, let's close with the scenarios where it really shines. The [presentation on categorizing properties](https://github.com/Certora/Tutorials/blob/2d12eecd3627d220b5f2839aa4d1035345a7ac61/06.Lesson_ThinkingProperties/Categorizing_Properties.pdf) from Certora's tutorial gives a good overview of these.

Understanding a smart contract as **a finite-state machine** (obligatory mention to [Yoichi's bamboo](https://github.com/pirapira/bamboo/blob/master/doc/manifest.md), my favorite smart contract programming language that never happened) allows us to define clear rules on:
- what are the **valid states** for the contract, and
- what are the **valid transitions** between those states.

Let's grab some examples from [OpenZeppelin's TimelockController spec](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/2c5194f3f13d3f9ce301d8100b9f5fe0cec6d7d8/certora/specs/TimelockController.spec). In a Timelock, operations can have different states. We can write a rule that checks, for instance, that calling `execute` is the only way for moving an operation from `ready` to `done` state.

```
rule readyDoneTransition(method f, env e){
  bytes32 id;
  require isOperationReady(e, id);

  calldataarg args;
  f(e, args);

  assert isOperationDone(id) => f.selector == execute(...).selector;
}
```

Or that `done` is a final state: no matter what we call on the contract, a `done` proposal will always stay that way:

```
rule doneToNothingTransition(method f, env e){
  bytes32 id;
  require isOperationDone(id);

  calldataarg args;
  f(e, args);

  assert isOperationDone(id);
}
```

And we can rely on invariants to assert the validity of each of these states (see [representation invariants](https://www.cs.cornell.edu/courses/cs3110/2014sp/lectures/10/representation-invariants.html)). For instance, an operation is `ready` to be executed if and only if its associated timestamp is non-zero and in the past:

```
invariant readyCheck(env e, bytes32 id)
  (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) 
  <=> isOperationReady(e, id)
```

Another use case is for writing unit-test-like specs. For instance, in an ERC20, we would write a test that the `transfer` works: it decreases the balance of the sender and increases the balance of the receiver by the sent amount. We would test it with specific addresses with specific balances and a specific amount. But here we can just write that property, and have the prover **verify it for every possible initial state and input**, not just the ones we used in the unit test.

```
rule transfer(env e, address recipient, uint256 amount) {
  address holder = e.msg.sender;
  uint256 holderBalanceBefore = balanceOf(holder);
  uint256 recipientBalanceBefore = balanceOf(recipient);
    
  transfer(e, recipient, amount);

  assert balanceOf(holder)    == holderBalanceBefore    - (holder == recipient ? 0 : amount);
  assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount);
}
```

But we can also test more general properties. Following the previous example, we can just check that a `transfer` always increases the balance of the recipient and decreases that of the sender.

```
rule transfer(env e, address recipient, uint256 amount) {
  address holder = e.msg.sender;
  uint256 holderBalanceBefore = balanceOf(holder);
  uint256 recipientBalanceBefore = balanceOf(recipient);
    
  transfer(e, recipient, amount);

  assert balanceOf(holder) <= holderBalanceBefore;
  assert balanceOf(recipient) >= recipientBalanceBefore;
}
```

Or that `transfer` cannot create new tokens for the sender or recipient, meaning that the sum of their balances must remain constant.

```
rule transfer(env e, address recipient, uint256 amount) {
  uint256 balanceSenderBefore = balanceOf(e, e.msg.sender);
  uint256 balanceRecipientBefore = balanceOf(e, recipient);
  transfer(e, recipient, amount);

  assert balanceRecipientBefore + balanceSenderBefore == balanceOf(e, e.msg.sender) + balanceOf(e, recipient);
}
```

These are examples of **high-level properties** that hold over every execution of a certain operation, like `transfer`, or that hold over the entire contract throughout its lifecycle. The latter are best expressed in the form of invariants, as we saw early on with the Bank example.

```
invariant totalFundsGreaterThanAnyUser()
  forall address user. getTotalFunds() >= getFunds(user)
```

## Learn more

To start playing with CVL, the [demo site](https://demo.certora.com/) has a great interactive online editor, where you can write your contract and spec side-by-side and run the prover on it, or try out a bunch of examples.

![](https://i.imgur.com/WxfGdWF.png)

Certora's [tutorial on github](https://github.com/Certora/Tutorials) is also a great starting point for the basic concepts, though the lessons for more advanced ones are still under development. The [documentation](https://docs.certora.com/en/latest/) provides a good overview and reference for many concepts, though it's also a work in progress, and redirects to an older set of docs for the more advanced ones. A [multi-contract example](https://github.com/Certora/LiquidityPoolExample) repo is a good complement to see the documented concepts in action.

But when you are ready to move on from the tutorial and docs, the best source for learning are the **actual specs for real-life projects**, [OpenZeppelin Contracts](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/formal-verification/certora/specs) and [AAVE](https://www.certora.com/dashboards/aave-dashboard/) being good examples.