A look into formal verification of smart contracts using Certora

This page summarizes the projects mentioned and recommended in the original post on dev.to

Our great sponsors
  • SonarQube - Static code analysis for 29 languages.
  • InfluxDB - Build time-series-based applications quickly and at scale.
  • SaaSHub - Software Alternatives and Reviews
  • Tutorials

    Practical tutorials of Certora Prover (by Certora)

    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.

  • reentrancy-attacks

    A chronological and (hopefully) complete list of reentrancy attacks to date.

    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.

  • SonarQube

    Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.

  • bamboo

    Bamboo see https://github.com/cornellblockchain/bamboo (by pirapira)

    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:

  • openzeppelin-contracts

    OpenZeppelin Contracts is a library for secure smart contract development.

    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.

  • LiquidityPoolExample

    Example Certora verification for a simple multi-contract system

    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.

  • InfluxDB

    Build time-series-based applications quickly and at scale.. InfluxDB is the Time Series Platform where developers build real-time applications for analytics, IoT and cloud-native services. Easy to start, it is available in the cloud or on-premises.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts