# The Certora Prover Technology: A Gentle Introduction

June 20, 2022

Certora is building a developer tool for smart contracts that supports finding bugs, reasoning about correctness, and producing formally verified proofs. The framework consists of two main components: (1) a specification language for describing intended smart contract behaviors symbolically and (2) an engine for analyzing the smart contracts against the specification. The technology automatically locates critical bugs that even the best auditor can miss and increases confidence in code security by proving that certain rules hold.
On a high level, the Certora prover is essentially a sophisticated compiler translating the bytecode and the properties into a mathematical formula that concisely defines the exact conditions under which the program may violate the properties. This formula is fed into existing open source tools which locate bugs and produce proofs.

This document describes the main techniques implemented in the Certora Prover from a high-level perspective. We assume that the readers are familiar with smart contracts. The examples used in this document are also accessible at Certora's [demo](https://demo.certora.com/) page.

# Design Principles

The Certora prover takes a low-level [EVM bytecode program](https://ethereum.github.io/yellowpaper/paper.pdf) and a specification written in Certora's specification language, [CVL](https://docs.certora.com/en/latest/docs/ref-manual/cvl/index.html).[^1] The prover analyzes the code and the spec together to identify scenarios where the code deviates from the specification.

The design of the prover is guided by the following principles.

**1. Verify what you Execute.**
We decided to implement the verification tool chain on the EVM bytecode instead of the Solidity code. This decision significantly increases security as we verify the code that is actually executed. In particular, it does not trust the compiler (e.g., Solidity compiler) that generates EVM bytecode from the source. However, this decision drastically complicates the verification problem as the compiler often generates sophisticated, optimized code. Certain information is lost in the translation, which adds to the verification complexity, and complicates diagnosability when verification fails. The Certora prover performs static program analysis to reconstruct this information when possible to aid users in diagnosing counterexamples.

**2. Trust but Verify**
The EVM provides a rich interface. Moreover, the compilers generating EVM bytecode from the source utilize dynamic loading, making general-purpose verification nearly impossible. Therefore, we place certain restrictions on the analyzed EVM code to make verification scalable. Our static analysis algorithm enforces these restrictions. When the static analysis algorithm fails, we analyze the failure. In [some](https://medium.com/certora) cases, this reflects a bug in the Solidity compiler, which is reported to the Solidity team. We are constantly working to improve and generalize the static analyses to handle more smart contracts.

**3. Separate the code from the Spec**
The CVL spec is written in a separate file, making the specification usable across different code versions. However, certain features of Solidity are harder to express, e.g., access to private fields, loop invariants, and internal functions. CVL provides several features that can be used to address these challenges.

**4. Rich Spec Language**
Unlike traditional unit tests, which describe the output for a particular input, the Certora Prover considers the _entire_ (potentially infinite) space of possible inputs. CVL supports invariants, parametric functions, uninterpreted functions, "ghosts" functions that can model contract state not explicitly present in the contract, and relational properties. Our spec language allows reasoning about infinite behaviors and checking equivalence between programs.

**5. Powerful Interaction Mechanisms**
Since formal verification is an undecidable problem, there will always be properties that cannot be verified for some programs. CVL provides a rich set of features for approximating difficult-to-verify code, giving users fine-grained tools for trading soundness for completeness. These include: (1) bounding the number of executed loop iterations or providing checked loop invariants, (2) breaking large code into several pieces which are modularly verified.

**6. Vacuity Checking**. One of the hardest questions in formal verification is coming up with the right specification. Errors in a specification can lead users to incorrectly conclude that their contracts are correctly implemented. Therefore, Certora implemements techniques for preventing certain patterns of bad specifications. For example, a tautology invariant of the form `x = 5 ==> x > 0` will be flagged as a potentially incorrect specification by the system.

# Formal Specification

One of the biggest challenges in software development is specifying the intended behavior of the program. Developers often use unit tests to specify the expected outputs for given inputs, but unit tests can only enumerate a finite number of input scenarios to be tested. In contrast to unit tests, specifications in CVL describe the expected output for _every_ possible input. Since this article describes only some of the mechanisms used in CVL specifications; we refer readers to the [reference manual](https://docs.certora.com/) that contains complete details.

## Representation Invariants and Inductive Invariants

Invariants are properties that hold in every reachable state of the program.
In a contract that keeps bank acount balances, an invariant may requires that total is equal to the sum of all balances.

Inductive invariants are invariants that are preserved by arbitrary executions. When a transition is executed in an arbitrary state that satisfies the invariant, the invariant holds after the state. Intuitively, it means that the program is correct even when executed on an arbitrary state. This is a way to guarantee that your program is correct independent of the number of instructions executed. For example, the invariant that every address in an ERC20 is less than or equal to the total balance is correct but _not_ inductive. A counter example to induction is a transition from a state satisfying the invariant into a bad state violating the invariant. Every invariant can be made inductive by strengthening. Notice that this exactly mimics proofs by induction. To learn more about inductive invariants, we refer the reader to https://www.youtube.com/watch?v=30BspXZs7q8.

## Rules

A rule describes properties of possible transitions of the system. It should therefore describe: (1) the state before the transition, (2) the transition, (3) and the state after the transition. By describing a state, we mean setting requirements on the set of possible states, and similarly for transition (i.e. which function is used and what conditions the inputs satisfy). A rule can therefore be defined as the Hoare triple:

{ state before };
f(function inputs);
{ state after };

For example, we might want to track the change in the balance of user _Alice_ when user _Bob_ performs a deposit call to a pool contract. The triple above can take the form:

{ uint256 x = BalanceOf(Alice) };
Deposit(Bob, amount);
{ BalanceOf(Alice) == x };

# Formal Verification via Contraint Solving

The Certora prover compares the behavior of the bytecode and the spec to find bugs and formally prove their absence. Intuitively, the idea is to model both the semantics of the EVM and the specifications as SMT formulas. SMT formulas are constraints over symbolic variables. Symbolic variables are very different from program variables - their value can be arbitrary. For example, the formula `x * x > 4` is satisfiable, e.g., for `x = 3`. However, the formula `x * x + 1 < 0` is not satisfiable. The SMT can generate a formal proof that this formula is not satisfiable for any `x`.

In this section we gradually explain the process.

## Boolean Satisfiability
One of the hardest problems in computer science is boolean satisfiability: given a boolean (0, 1) formula over logical variables: `v1, v2, ..., vk`, is there a value to the logical variables that makes the formula true. For example, `a && !a` is `false` for both `a = 0` and `a = 1`, so it is not satisfiable. The satisfiability problem for `n` variables can be solved by enumerating all the $2^n$ values. However, it is not known how to solve the problem efficiently on arbitrary formulas. Still, there exist tools that can check the satisfiability of huge formulas in a few seconds.

## Formal Verification by Reduction to Satisfiability

Given a loop free program and an assertion, it is possible to formally verify the assertion using Boolean Satisfiablity ([SAT](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem)). For example, Figure 1 shows the control flow of a small program. In order to determine if the assertion at the end of the program holds, we check the SAT query:

(a && x) \/ (!a && !x)
(b && y) \/ (!b && !y)
(x && !y) \/ (!x && y)

Notice how this formula compactly defines 4 paths of the program. The SAT solver identifies that the formula is satisfiable, e.g., for `a = 0` and `b = 1`, then `x = 0` and `y = 1` satisfy the formula.


Figure 1: A program's control flow with an assertion `X == Y` that is not always true.

Modern SAT solvers can also determine that formulas are not satisfiable, often in clever ways without enumerating all values. They enable formally verifying the program on all paths. For example, Figure 2 shows a code fragment with a valid assertion.


Figure 2: An example with a valid assertion.

In this case, the SAT query

(a && x && b) \/ (!a && !x && !b)
(b && y) \/ (!b && !y)
(x && !y) \/ (!x && y)

is not satisfiable for all the values of a, b, x, and y. Therefore, the assertion is valid.

## Beyond Booleans: SMT
We are interested in formally verifying infinite state programs with program variables such as addresses which can take infinite values. In computer science, [SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)(Satisfiability Modulo Theories) refers to the problem of finding if a first-order logical formula over various theories is satisfiable.

# Mitigating Complexity of Constraint Solving via Sound Static Analysis

There exist many open source software for solving SMT constraints, including [Z3](https://github.com/Z3Prover/z3), [CVC5](https://cvc5.github.io/), [Yices](https://yices.csl.sri.com/), and [Vampire](https://vprover.github.io/index.html). The Certora verifier utilizes all of these solvers. These solvers can generate counterexamples and formal proofs in many interesting cases.

Unfortunately, SMT solving is an undecidable problem. Even when all the values are booleans, the complexity is NP-complete. Moreover, the Solidity compiler generates nontrivial instructions that manipulate memory in nontrivial ways and it uses dynamic loading to hide the program's control flow. These strategies make formal reasoning about program correctness even harder. Certora has developed sophisticated static analysis algorithms (also known as abstract interpretation) for automatically inferring nontrivial invariants from the bytecode. For many common programs, Certora's algorithm can mitigate the complexity of SMT solving without sacrificing coverage. When a rule is proved, it is guaranteed to hold.

For example, consider the following EVM code snippet:

l1: mem[index] = “foo()”;
l2: mem[index + 4] = x;
l3: mem[otherIndex] = 44;
l4: send(contract, mem[index .. index + 36])

The Solver needs to assure that the only invoked method in the `send` command on line `l4` is `foo`. This requires proving that the writes to memory on lines `l2` and `l4` do not change the content of `mem[index]`. This is in general an undecidable problem, and a technique that reasons about this is called _pointer analysis_. The Certora prover implements pointer analysis which enforces invariants on the patterns of memory access generated by the compiler in order to solve the problem in many cases.

## Modularity

Automatically verifying that a contract satisfies a specification is an undecidable problem in theory and can have high complexity in practice. To reduce the resources required to complete the proof, a user of the Certora prover can take several approaches to simplify the problem. An important class of techniques is based on modularity, i.e., splitting the verification problem into multiple independent subproblems.

Under modular verification, the user selects some methods from the smart contract to *summarize*. A summary approximates the behavior of the method. By replacing the method with its summary, the user simplifies the overall verification problem for the Certora prover. Many different kinds of summarization are possible. For example, the body of the method could be summarized as returning an arbitrary value, a constant, some ghost state, or some other simplified description of the method's behavior.

With summaries, instead of verifying the entire program in one pass, the problem is broken down into two kinds of subproblems. First, in the entire verification condition of the program instead of using the method's definition, we use its summary. Second, we check that the method's summary is a correct approximation of the actual method definition. In practice, it is sometimes useful to omit the second check to give rule writers maximum flexibility.

# The Certora Prover Architecture

The Certora Prover implements a sophisticated tool chain for verifying low level code. It currently supports EVM bytecode but its tool chain is generic and can be adapted to other bytecodes, e.g., eBPF and Web Assembly.

Figure 1 depicts the Certora prover architecture. It operates on EVM bytecode which is a stack-based language. A decompiler maps each stack location into a symbolic value, called a register, and then converts the bytecode instructions into instructions over registers. A similar technique was implemented in [Soot](http://soot-oss.github.io/soot/). A static analysis algorithm then infers sound invariants about the code, drastically simplifying the verification task. Then, the VC generator outputs a set of mathematical constraints which describes the conditions under which the program can violate the rules. Finally, the Certora prover invokes off-the-shelf SMT solvers that automatically searches for solutions to the mathematical constraints which represent violations of the rules. As described earlier, this is an undecidable problem and these solvers _can_ fail in certain cases by timing out with inconclusive answer. The Certora prover takes the result from the solver, processes it to generate a detailed report, and presents it to the client/user of the prover.

Figure 3: The Certora Prover Architecture

# Related Tools
Smart contract correctness has received a considrable attetion in industry and Academi. Here are some related tools.
## Unit Testing and Fuzzing
Testing and fuzzing of smart contracts can be very effective in tools like [Foundry](https://github.com/foundry-rs/foundry/tree/master/forge), [MythX
(https://mythx.io/), [Manticore](https://github.com/trailofbits/manticore), and [Echidna](https://github.com/crytic/echidna). The Certora prover improves coverage beyond these tools by using the powerful CVL specification and harnessing SMT solvers for identifying potentially rare paths showing cases were violations occur.
## Classical Static Analysis
Static analysis tools such as [Slither](https://github.com/crytic/slither) can also be used to identify potential bugs. The Certora prover provides witnesses for rule violations and guarantees for corrected rules which are beyond the scope of static analysis. Of course, the Certora prover is more computationally expensive.
## Proof Assistants
Proof assistents such as [K](https://kframework.org/), [Coq](https://coq.inria.fr/), and [Isablle/HOL](https://isabelle.in.tum.de/) implement a radically different approach for obtaining provably correct code. The programer writes a mathematical proof about the model and extract code from proofs. Instead, Certora feels more like unit and fuzz testing. We compare the low level code with the high level CVL specifications.
# Conclusions

The Certora prover supports reasoning about *all* executions of an Ethereum bytecode program. The prover takes as input the bytecode program along with a specification written in CVL. The goal of the prover is to check whether all executions of the bytecode satisfy the specification. The prover achieves this by analyzing the bytecode and converting it, together with the specification, into a system of constraints. These constraints are then solved by a suite of underlying SMT solvers. The solvers either report that all executions are correct, or they return a specific input that causes an execution that violates the specification. In either case, the information is translated into a high-level format and shown to the user.

The main challenge with using any formal verification technology is complexity. For practical contracts and specifications, the constraints generated by the prover can be very challenging for the solvers. In these cases, the user can break down the proof by summarizing complex pieces of code. With good summaries, each piece of the proof can be handled by the solver, and the pieces add up to a proof of the original specification.

[^1]: We are actively working on extending the documentation.