Ensuring smart contract security

Request Early Access

Technology

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

About Certora

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. Certora offers two unique solutions targeted for all participants in the blockchain ecosystem:

Static Asset Scanner (SAS) for businesses that employ Smart Contracts. We currrently check ERC standards. For each scanned contract, we report the security rules that it obeys and provide inputs demonstrating violated rules.

SAS guarantees long-term safety of your digital assets in the blockchain by notifying immediately on any new issues, thus reducing incident response time. This allows your business to avoid the consequences of undesired irreversible transactions.

Quality Development Environment (QDE) for developers is a CI/CD plugin that allows developers to move fast and break nothing. Developers can detect issues during development, assist in QA, and maximize security before contract deployment.

QDE automatically produces a report of existing issues, reporting their severity and the exact manner in which they reproduce, integrating seamlessly into existing CI/CD pipeline.

Contact Us

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

  • Isn't the formal verification problem undecidable?

    Yes. There are actually two difficult problems:
    (1) How does one define what requirement to check
    (2) Given a requirement, how to make sure that all executions of the program fulfill the requirement. The Certora proprietary technology, Certora Prover, addresses the second problem. The second problem is especially interesting for software systems such as Smart Contracts, in which the number of potential states is infinite. This is realized in programs with loops and contracts which call each other. In fact, virtually all contracts have an infinite state since they are reactive.
    Therefore, we develop unique technology which can reason about such programs in an accurate way.

  • How does Certora decide what requirements to check?

    Certora offers two mechanisms:
    (1) A list of predefined requirements based on best practices defined by the Smart Contract community.
    (2) The user defines requirements using a new command called 'ensures' which behaves similarly to Solidity's assert, but is checked at compile-time by the Certora Prover engine.

  • Can Certora handle contracts which rely on other contracts?

    Certora optionally enforces a requirement which ensures that external contracts cannot change the internal state of the checked contract. This automatically prevents bugs like the DAO. It also enables Certora Prover to verify the code without considering the potentially complicated code of the external contract. Thus, Certora verifies one contract at a time. In the formal method community this is called rely-guarantee reasoning. This is similar to the notion of separate compilation in compilers.

  • Do I have to trust Certora?

    Certora facilitates trust by the combination of the following:
    (1) Providing an executable tool where users can review the verification process and reproduce it at any point in time.
    (2) Generating artifacts of the verification, which can be reviewed by non-experts without depending on Certora's tools. These artifacts are test inputs that demonstrate pathes in the code which lead to violations and satisfaction of requirements.
    (3) Developing proprietary technology for automatically generating machine checkable proofs. In Computer Science, this area is called Proof-carrying code.

  • What is the isolation requirement?

    Smart contracts are vulnerable to so called "callback attacks". The attacker contract can exploit the fact that the internal state of the contract is not yet stable. This happened in the DAO attack and the SpankChain bug. One way to avoid the problem is to limit the use of callbacks to occur in the last command in the contract but this can be too restrictive in many cases.
    Effectively Callback Freedom: We are enforcing a requirement which permits liberal usage of callbacks as long as the state of the contract cannot be manipulated in a way which breaks its correctness. For additional documentation, refer to:
    - A short Video by Shelly Grossman
    - A long Video by Noam Rinetzky taken at POPL'18 LA
    - Academic Paper
    - Technical Report
    - Code
    Acknowledgements This is a joint work between Vmware Research Group, Tel Aviv University and Stanford University.

x