🪨🐓 coq-of-solidity

A formal verification tool for Solidity using the Coq proof system

The coq-of-solidity project is a tool to automatically translate Solidity smart contracts to the Coq proof system. This allows to formally verify the correctness of the smart contracts.

Formal verification is about verifying code for all possible input, and goes further than traditional testing that only covers a finite amount of cases. Formal verification relies on mathematical methods to analyze the code.

This project provides:

1. More security for code audits: all the combinations of inputs are covered, in contrast to testing.
2. Reusable audits for future code changes: we can re-run the proofs as the code evolves.

The coq-of-solidity tool uses an interactive theorem prover (Coq) to check arbitrarily complex code properties and business rules for your smart contracts.

🙏 Thanks

We thank the AlephZero Foundation for their support and funding of this project.

📬 Contact

If you have smart contracts that you wish to audit with a maximum level of security, or want to know more about this project, do not hesitate to contact us at contact@formal.land. We provide formal verification services for Solidity, Rust, and OCaml, and we already secured thousands of lines of code for the blockchain industry (Tezos, Aleph Zero, Sui).

🚀 Quick start

This project is based on a fork of the solc Solidity compiler. Compile it following the manual of solc to obtain a solc binary.

Then, assuming that you are at the root of this project, run the following commands:

build/solc/solc --ir-coq --optimize my_smart_contract.sol

It will pretty-print on the terminal a Coq version of the code. Examples of contracts that are already translated in Coq are in the CoqOfSolidity/ folder.

We successfully translate and run more than 90% of the Solidity compiler tests in test/libsolidity/semanticTests/. The main missing features are the pre-compiled contracts and error cases in contract calls. The main file to extract the semantic tests with the execution trace to Coq is test/libsolidity/SemanticTest.cpp:

• example source test: test/libsolidity/semanticTests/various/erc20.sol
• Coq output: CoqOfSolidity/test/libsolidity/semanticTests/various/erc20/GeneratedTest.v

Assuming that you have a working installation of the Coq system, you can compile the existing translated code with:

cd CoqOfSolidity
make -j4 -k

The Coq compilation takes a lot of time as there are a lot of generated files.

The translated Coq files can sometimes be a bit too verbose. You can have a better readability by generating the original Yul code that we use to generate the Coq translation with:

build/solc/solc --ir-optimized --optimize my_smart_contract.sol

🏗️ Architecture

This project is built as a fork of the official solc compiler in order to re-use the frontend (parser, type-checker, ...) and stay up-to-date with the Solidity language. The solc compiler is a C++ project that compiles Solidity code to EVM bytecode.

We translate the intermediate language Yul to Coq. Yul is a low-level intermediate language used by the Solidity compiler that is both simpler than Solidity and more high-level than EVM bytecode. The relevant code is in libyul/AsmCoqConverter.cpp.

We then define in Coq the semantics of the Yul language as well as of all the EVM primitives (addition, multiplication, keccak256, contract calls, ...). This is done in the two following files:

• CoqOfSolidity/CoqOfSolidity.v for the semantics of the Yul language
• CoqOfSolidity/simulations/CoqOfSolidity.v for the semantics of the EVM primitives

To prevent mistakes in our Coq definitions, we also translate the semanticTests of the Solidity compiler to Coq and re-run them in Coq. We then check that we get the exact same outputs as the code generated by the official Solidity compiler.

🧪 Build the tests

To build the tests you need to:

1. Translate the test files to Coq with the following commands:

   cd CoqOfSolidity
   python translate_from_tests.py

   This will generate one .v file per contract in the semanticTests and syntaxTests folders.
2. Generate the test files corresponding to the execution traces with the following commands:

   build/test/soltest --run_test=semanticTests

   This will generate one GeneratedTest.v file per semantic test. This command takes several minutes to run, as it also compiles and executes each of the contracts in the semantic tests. This command might require a few dependencies to run, like evmone. You can first try to make this test command work in te upstream repository of Solidity.
3. Then you can compile them with:

   cd CoqOfSolidity
   make -j4 -k

   For the syntax tests it will verify that the translated Coq code type checks. For the semantic tests it will verify that the execution trace of the contract is the same in Coq as with the Solidity compiler, in addition of type checking the translated code.

We do not support yet all the semantic tests but around 90% and are working on the remaining ones.

📚 Example

Here is what the Coq translation looks like for an example of Solidity code:

function _transfer(address from, address to, uint256 value) internal {
    require(to != address(0), "ERC20: transfer to the zero address");

    // The subtraction and addition here will revert on overflow.
    _balances[from] = _balances[from] - value;
    _balances[to] = _balances[to] + value;
    emit Transfer(from, to, value);
}

translates in Coq to:

(* Generated by coq-of-solidity *)

Definition fun_transfer (var_from : U256.t) (var_to : U256.t) (var_value : U256.t) : M.t unit :=
  let~ _1 := [[ and ~(| var_to, (sub ~(| (shl ~(| 160, 1 |)), 1 |)) |) ]] in
  do~ [[
    M.if_unit (| iszero ~(| _1 |),
      let~ memPtr := [[ mload ~(| 64 |) ]] in
      do~ [[ mstore ~(| memPtr, (shl ~(| 229, 4594637 |)) |) ]] in
      do~ [[ mstore ~(| (add ~(| memPtr, 4 |)), 32 |) ]] in
      do~ [[ mstore ~(| (add ~(| memPtr, 36 |)), 35 |) ]] in
      do~ [[ mstore ~(| (add ~(| memPtr, 68 |)), 0x45524332303a207472616e7366657220746f20746865207a65726f2061646472 |) ]] in
      do~ [[ mstore ~(| (add ~(| memPtr, 100 |)), 0x6573730000000000000000000000000000000000000000000000000000000000 |) ]] in
      do~ [[ revert ~(| memPtr, 132 |) ]] in
      M.pure tt
    |)
  ]] in
  let~ _2 := [[ and ~(| var_from, (sub ~(| (shl ~(| 160, 1 |)), 1 |)) |) ]] in
  do~ [[ mstore ~(| 0x00, _2 |) ]] in
  do~ [[ mstore ~(| 0x20, 0x00 |) ]] in
  let~ _3 := [[ checked_sub_uint256 ~(| (sload ~(| (keccak256 ~(| 0x00, 0x40 |)) |)), var_value |) ]] in
  do~ [[ mstore ~(| 0x00, _2 |) ]] in
  do~ [[ mstore ~(| 0x20, 0x00 |) ]] in
  do~ [[ sstore ~(| (keccak256 ~(| 0x00, 0x40 |)), _3 |) ]] in
  do~ [[ mstore ~(| 0x00, _1 |) ]] in
  do~ [[ mstore ~(| 0x20, 0x00 |) ]] in
  let~ _4 := [[ checked_add_uint256 ~(| (sload ~(| (keccak256 ~(| 0x00, 0x40 |)) |)), var_value |) ]] in
  do~ [[ mstore ~(| 0x00, _1 |) ]] in
  do~ [[ mstore ~(| 0x20, 0x00 |) ]] in
  do~ [[ sstore ~(| (keccak256 ~(| 0x00, 0x40 |)), _4 |) ]] in
  let~ _5 := [[ mload ~(| 0x40 |) ]] in
  do~ [[ mstore ~(| _5, var_value |) ]] in
  do~ [[ log3 ~(| _5, 0x20, 0xddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef, _2, _1 |) ]] in
  M.pure tt.

The Coq output is based on the Yul compilation of the above Solidity code. It is a shallow embedding when we can, as in this example, and a deep embedding otherwise.

We have proven the code above to be equivalent to the high-level Coq version:

Definition _transfer (from to : Address.t) (value : U256.t) (s : Storage.t) : Result.t Storage.t :=
  if to =? 0 then
    revert_address_null
  else if balanceOf s from <? value then
    revert_arithmetic
  else
    let s :=
      s <| Storage.balances :=
        Dict.declare_or_assign s.(Storage.balances) from (balanceOf s from - value)
      |> in
    if balanceOf s to + value >=? 2 ^ 256 then
      revert_arithmetic
    else
      Result.Success s <| Storage.balances :=
        Dict.declare_or_assign s.(Storage.balances) to (balanceOf s to + value)
      |>.

In the high-level version we make explicit all the overflow checks and use real maps instead of Keccak-encoded keys.

📝 License

The code of the translation is under the GPL-3.0 license as this is a fork of the Solidity compiler. The code of the Coq semantics is under the MIT license.

👥 Developers

Some scripts or commands that can be useful for the development of this project:

To generate the JSON of the Yul of an example:

./build/solc/solc --ir-optimized-ast-json --optimize test/libsolidity/semanticTests/various/erc20.sol |tail -1 |jq 'walk(if type == "object" then del(.nativeSrc, .src, .type) else . end)' >CoqOfSolidity/test/libsolidity/semanticTests/various/erc20/ERC20.json