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" 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 is one of the players in this field, offering a platform for formal verification using a proprietary spec language, Certora Verification Language 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.

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 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. Rules are structured as Hoare triples:

• 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 (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 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 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. 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. 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, 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, and it's much harder to do in an automated way. Therefore, the Certora prover works by unrolling loops 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 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 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 from Certora's documentation, we are indicating that the asset field in the Pool contract refers to an instance of the ERC20 contract:

import "../ERC20.sol";

contract Pool {
  ERC20 asset;
}

$ 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, 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. 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 in CVL.

For example, view functions can be annotated as returning anything from a constant to a completely non-deterministic value. Here's an example taken from OpenZeppelin contracts:

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

The main challenge is dealing with non-view functions. 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. 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 based on an arbitrary parameter:

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 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, 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. 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). 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 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.

Certora's tutorial on github is also a great starting point for the basic concepts, though the lessons for more advanced ones are still under development. The documentation 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 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 and AAVE being good examples.