Certora

Mission & Key Concepts

Certora ensures correctness of Smart Contracts by applying modular formal verification.

Certora is a leading provider of technology and services for eliminating vulnerabilities in smart contracts. Certora offers a suite of tools for auditing smart contracts, including both the detection of vulnerabilities and the generation of assurances that essential properties always hold.

The core of the tool suite is the Certora Prover, a verification tool that takes a low-level EVM bytecode program and a specification written in CVL (Certora Verification Language). The prover analyzes the code and the spec together to identify scenarios where the code deviates from the specification. The technology automatically locates critical vulnerabilities that even the best auditor may miss and increases confidence in code security by proving that certain key properties are satisfied.

Additionally, Certora also has tools for analyzing the complexity of contracts, specification checking using mutations and vacuity detection, and a fuzzer for light-weight verification.

Certora’s approach is guided by a number of design principles:

• Verify What You Execute

The tool suite is built on the EVM bytecode instead of the Solidity code. This decision significantly increases security as we verify the code that is actually executed.

• Trust But Verify

The EVM provides a rich interface. Moreover, the compilers that generate EVM bytecode from the source code utilize dynamic loading, making general-purpose verification nearly impossible. Therefore, we place certain restrictions on the analyzed EVM bytecode to make verification scalable. 

• Separate The Specification From The Code

The CVL specification is written in a separate file, making it usable across different code versions of the same contract. Having a separate specification language also makes it easier to use the properties across different smart contract languages like Vyper, and other blockchains like Solana.

Culture & Values

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

History & Achievements

• Founded: 2018
• Team: 80+
• HQ: Israel

Milestones:

• 100 DeFi Hacks Prevented
• 15000 Runs/Month
• 2M+ Solidity Lines Verified
• $32B Protected TVL

Core Team

• Mooly Sagiv - CEO
• Nurit Dor - VP of Products

Benefits

• Competitive Package