Scaling Smart Contract Security: Why We Invested in Certora

Smart contracts are one of the primary drivers of innovation in the crypto ecosystem. These self-executing instruments act as building blocks for trustless, interconnected applications and power novel constructs like DeFi, NFTs, and DAOs. Having said that, smart contract security remains one of the biggest barriers to the mass adoption of these applications.

Though the industry is maturing, smart contract development is still a relatively new field that requires a distinct engineering mindset, and the cost of failure can be very high. Breaches in popular protocols such as Poly Network, Ronin, Venus, etc. have exposed structural vulnerabilities of these open-source, immutable contracts. While security audits are an important step in identifying vulnerabilities in a pre-deployment phase, it is clear that current tooling and auditing services are neither scalable nor comprehensive enough. In fact, 30% of code exploits and 73% of flash loan attacks in 2021 occurred on platforms that were audited within the prior year (1). We need a scalable and generalized approach to Web3 security and hence, Jump Crypto is excited to lead Series B for Certora.

Certora is a leader in smart contract security that leverages formal verification to verify smart contract code at the bytecode level. As a short introduction, formal verification is a system design technique that involves constructing an abstract representation of software (“I want the code to do this”) and then automatically finding scenarios in the code which violates the specification. For example, the Certora Prover identified a rare scenario in Balancer V2 leading to bankruptcy. This bug was found after excellent audits by Trail of Bits and OpenZeppelin which shows that even the best auditors are prone to errors. Formal verification has historically been an important element of the process for chip design, embedded system control software, and autonomous system security.

Certora implements technology which is unique not just in Web3. This technology automatically searches for behaviors in the code which violate the specification. Certora leverages two techniques in computer science which have been developed in academia:

1. Symbolic constraints solving - The Certora Prover encodes the smart contract  spec into a set of constraints. It then leverages Open source tools like Z3 by Microsoft and CVC5 by the University of Stanford and Iowa University to solve these constraints and thereby demonstrate the absence of bugs in the program.
2. Solving mathematical constraints is computationally very intensive. The computer might fail even when verifying tiny programs. This is where Certora develops sophisticated static analysis techniques which help work around the hardness of constraint solving.
   

In Certora, we found a trifecta of a world-class team, a scalable and productized approach to smart contract security, and validation from a blue-chip customer roster.

Certora CEO Mooly Sagiv is a world-renowned leader in formal verification and Chair of Software Systems at Tel Aviv University and has assembled one of the premier teams in formal verification and smart contract security, including co-founder Shelly Grossman (CTO, Ph.D. TAU), Nurit Dor (VP Product, Ph.D. TAU), John Toman (VP R&D, Ph.D University of Washngton) and many others.

Unlike traditional testing methods such as interactive theorem proving or fuzzing, Certora provides continuous verification by employing a suite of scalable and robust software testing products, including the Certora Prover that checks specs at compile-time, the Static Asset Scanner monitoring layer that ensures up-to-the-minute bytecode security, and a CI / CD platform for smart contract development. It finds rare bugs which are hard to find by testing by essentially enumerating all behaviors of the code.  We believe that Certora’s focus on provable security based on formal methods offers higher reusability and more granular testing, resulting in safer code with fewer exploits.

While the company is still in its early days, we are particularly excited about the enormous inbound interest from leading blue-chip protocols evidenced by the most recent Aave grant for their proposal, supplemented by an impressive customer list that includes Compound, MakerDAO, Balancer, Sushiswap, Coinbase, Benqi, Synthetix, Celo, etc.

In an increasingly complex design space, Certora is building a critical infrastructure needed to move the crypto ecosystem forward. Leveraging Jump Crypto’s R&D efforts and our internal security initiatives, we look forward to partnering with Certora and accelerating its growth curve.

1. The Chainalysis 2022 Crypto Crime Report