Introduction

coq-of-solidity is a tool to formally verify properties about smart contracts written in 🪨 Solidity. Formal verification is about checking properties on a program for every possible input. This contrasts with testing, which only checks a finite number of cases. It is the most powerful way to ensure your code is bug-free! ✅ It was originally developed for critical software in 🧑‍🚀 space systems, nuclear plants, etc. but it is now becoming more and more popular for the blockchain.

In the rest of the documentation, we assume you have some knowledge in formal verification and in particular in the 🐓 Coq proof assistant which we use. On a general note, expect it to be harder to fully formally verify a program than to write it. Still, it must be the simplest way to truly ensure your program is correct.

What you get

Thanks to coq-of-solidity, you can:

• Prove that your smart contract is safe 🛡️ for any possible inputs or successions of calls.
• Prove that your business rules are always respected.
• Run these checks in your CI/CD pipeline to ensure that no bug is introduced in your codebase.

This adds a final layer of security to traditional code audits which are based on human reasoning and testing which only checks a finite amount of cases. This verification even goes beyond other formal verification methods.

Picture from a presentation of Galois

Typical workflow

Formal verification is expensive ⏲️, so you should apply it after every other verification (testing, code review, etc.) is done. Here is a typical workflow:

1. You model your smart contract in the Coq proof system. For this step, you manually rewrite your smart contract in idiomatic Coq code.
2. You start expressing and proving a few properties in Coq about your model. For example, for any possible call the total number of tokens in your contract is constant, if that is a business rule.
3. Once you are confident in the approach, you show that your model is equivalent to the Solidity source code using coq-of-solidity and integrate this check into your CI/CD pipeline. At this step, you will probably discover some differences between your model and the source code, like unaccounted integer overflows, and you will have to refine your model to take them into account.
4. When your code evolves, you can update your model and your proofs to ensure that your new code is still correct. coq-of-solidity will make sure that your model is still equivalent to your source code 🚀.

Example

Here is an example of Solidity function returning the standard addition ➕:

function add(uint256 a, uint256 b) public pure returns (uint256) {
    return a + b;
}

Here is its translation to Coq as generated by coq-of-solidity:

Definition checked_add_t_uint256 (x : U256.t) (y : U256.t) : M.t U256.t :=
  let~ '(_, (sum, x, y)) :=
    let sum := 0 in
    let~ x := [[ cleanup_t_uint256 ~(| x |) ]] in
    let~ y := [[ cleanup_t_uint256 ~(| y |) ]] in
    let~ sum := [[ add ~(| x, y |) ]] in
    let_state~ 'tt := [[
      Shallow.if_ (|
        gt ~(| x, sum |),
        do~ [[ panic_error_0x11 ~(||) ]] in
        M.pure (BlockUnit.Tt, tt),
        tt
      |)
    ]] default~ (sum, x, y) in
    M.pure (BlockUnit.Tt, (sum, x, y))
  in
  M.pure sum.

This translation is a bit more low-level as we rely on the intermediate language Yul of the Solidity compiler. Here is what it does in pseudo-code:

function checked_add_t_uint256(x, y) {
  sum := x + y modulo 2^256
  if x > sum {
    panic
  }
  return sum
}

For security, the addition in Solidity checks the overflows and panics if it happens. Here is the Coq model of the addition:

Definition safe_add (x y : Z) : option Z :=
  (* We use unbounded integers [Z] *)
  let sum := x + y in
  (* We return [None] in case of overflow *)
  if sum <? 2 ^ 256 then
    Some sum
  else
    None.

We can express that it behaves as the translation of the Solidity code in the non-overflown case:

Lemma run_checked_add_t_uint256 codes environment state
    (x y sum : Z)
    (H_x : 0 <= x < 2^256)
    (H_y : 0 <= y < 2^256)
    (H_sum : safe_add x y = Some sum) :
  {{? codes, environment, Some state |
    checked_add_t_uint256 x y ⇓
    Result.Ok sum
  | Some state ?}}.

It says that for any initial chain state and x and y such that they are in the range of uint256, if the addition does not overflow, then the result of the translation is the sum of x and y, and the chain state is unchanged. We could make a similar statement for the overflow case.

Now, we need to prove that this statement is true using the tactic language of Coq and some of the custom tactics provided by coq-of-solidity. We write the proof using the interactive mode of Coq. To give an idea, here is our proof:

Proof.
  unfold safe_add in H_sum.
  destruct (_ <? _) eqn:? in H_sum; inversion_clear H_sum.
  unfold checked_add_t_uint256.
  lu.
  repeat (lu || cu || p).
  s.
  unfold Pure.gt, Pure.add.
  destruct (_ >? _) eqn:?; s.
  { lia. }
  { pe; f_equal.
    lia.
  }
Qed.

How it works

We make a shallow embedding of Yul into Coq. All the code is put into a monad to represent the various side-effects which are mainly:

• Modifying the blockchain state.
• Control-flow operations, such as break or continue in a loop, or revert to prematurely abort a contract.
• Mutating the local variables.

We translate the mutation of variables by doing an effect analysis and building a state that is the tuple of the variables being currently updated. This helps to reason about loops.

We recommend only translating the unoptimized version of Yul. That way you are sure to:

• Keep the same variable names in the Coq translation as in the source Solidity, helping for the proof process.
• Have a diff in the translation that is proportional to the diff in the source code.

The implementation of coq-of-solidity is actually fairly simple and relies on the existing Coq system for the heavy work! 🏋️