Ensuring smart contract security

Request Early Access

About Certora

We are the only team which provides
Prover technology for checking security rules with the following features:

Certora for Business

Static Asset Scanner: A monitor layer for smart contracts providing up to the minute security of the bytecode.

Certora for Developers

Quality Development Environment: A CD/CI platform for smart contract development.

Request Early Access

Technology

Certora provides security analysis tools for Smart Contracts. Certora has unique technology called Certora Prover capable of checking at compile-time that all executions of a Smart Contract fulfill a set of security rules.

Certora Prover technology is available as a tool that complements existing compilers and debuggers of Smart Contracts. It checks that the contracts adheres to the interface requirements of other contracts. Certora’s blockchain independent and language-agnostic Prover technology precisely identifies bugs in Smart Contracts and proves their absence.


Contact Us

Blog

Docs

Verification Reports

Customers

Core Team

Certora Prover builds on 30 years of academic research and hundreds of academic publications which pioneeered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise.

Advisory Board

FAQ

  • Can we use the Certora Prover in our CI pipeline?

    This is exactly the intended use case of the Certora prover!

  • What can be tested or proven using the Certora Prover?

    The Certora Prover provides complete path coverage for a set of safety rules provided by the user. For example, a rule might check that only a bounded number of tokens can be minted in an ERC20 contract. The prover either guarantees that the rules hold on all paths and all inputs or produces a test input that demonstrates a violation of the rule.

  • What cannot be tested using the Certora Prover?

    The problem addressed by the Certora Prover is known to be undecidable. This means that there will always be pathological programs and rules for which the Certora prover will time out without a definitive answer. Our experience so far is that realistic customer’s programs are not pathological, and can be successfully analyzed by the Prover. The Certora team is actively working to reduce the number of timeouts when analyzing smart contracts of customers.

  • How does formal verification differ from a traditional security audit?

    A traditional security audit usually involves a manual, holistic review of an entire system. Formal verification, on the other hand, produces a proof that a piece of software satisfies a specification. The Certora team is available for formal verification projects where we will write specifications and verify the code against these specifications. Often, verification projects find bugs in the code, and these bugs can be fixed during the course of the project, with the fixes proved correct. The team also produces a report describing the properties verified and bugs discovered. At the moment, we only analyze and review Ethereum bytecode.

  • Can we program our own rules into the prover into the future?

    Definitely, and we will assist you and review your rules for free.

  • What are the inputs to the Certora Prover?

    The Certora Prover takes as input the smart contract (either as EVM bytecode or Solidity source code) and a set of rules, written in Certora’s specification language. The Prover then automatically determines whether or not the contract satisfies all the rules. Just as good testing sometimes requires code refactoring, verification occasionally requires changes to the code. For example, because the verification happens via the public API to the contract, some pieces of state may need to have getters added so that they are accessible.

  • How do I know that the written rules are correct?

    When the Certora Prover provides a test input which violates the rule, the user can simply check if this violation is due to a bug in the code or in the rule. We also suggest performing a sanity check on the rules e.g., by mutating the contract by adding an artificial bug and checking if any rule is violated. If no rule is violated it indicates a missing rule. The Certora Prover also automatically generates test cases for showing that a point in the program is reachable.

  • What is the technology behind the Certora Prover?
  • How does the Certora Prover differ from existing tools in the market?

    Unlike symbolic execution tools which select specific paths and a fixed set of bad patterns, such as MythX and Slither, the Certora Prover provides complete coverage for a user provided set of rules. Interactive theorem provers such as Coq and K can be used for interactively showing that a specific contract is correct. SMTChecker by the Solidity team and Verisol by Microsoft Research are similar to the Certora Prover in many respects but target Solidity sources with per program user assistance. This makes the tools hard to integrate into the CI pipeline --- the value of the verification is that it allows to move fast and break nothing!

x