News & Updates

Blockchains are Powerful but Vulnerable: Why We’re Investing in Web3 Security Leader Certora

Aaron Fleishman, Partner

Web3 is primarily defined by its open, permissionless, trustless, and decentralized foundation on the blockchain, and is the hot topic these days. The hype is real! This iteration of the web is a major new wave in platform technology, and it’s not just hype. 

Many people have written about Web3 and so rather than writing yet another primer on the state of Web3 or why it’s important (Here’s my favorite. Or another.), I’d like to focus on why Tola is investing in this technology.

*And as a bonus, I’ll touch on why a mid-1900s mathematics technique is uniquely relevant for securing blockchains.

Why Now?

There are many things that make Web3 compelling at this particular moment in time. 

The first is the emergence of real applications and use cases of the underlying blockchain technology. For nearly a decade, blockchain technology felt like Windows without Office – a game-changing new platform seeking tangible applications. And to be clear, this is not a knock on those true believers who were coding during that time; those developers deserve the most credit. They were working on the foundation and the applications simultaneously. It’s just to say that a wide variety of applications hadn’t taken off yet – the ultimate chicken and egg scenario. 

Over the past few years, real-world applications have started to break through on Web3. DeFi had been around of course, but it really accelerated with the DeFi summer of 2020 when we started to see use cases like lending take off. 

Then NFTs and DAOs broke through in 2021. And yes, NFTs get a lot of flak (much of it deserved), but I am as proud of the art that I own in my metaverse house as I am of the art I own in my physical house. 

Side note: If you click that link, you’ll notice a lot of videos and images of a young astronaut. If you’re interested in going down an NFT rabbit hole, check out Aku – a character created by former MLB player turned artist, Micah Johnson, after hearing a young boy ask, “Can astronauts be black?”

As for the second core driver, I’ll reference Microsoft again. (Many of us at Tola worked at Microsoft so we draw on our experiences, in this case the mantra of: developers, developers, developers!) At the most basic level, if a lot of smart, technical people spend every day working on something, usually strong, positive results follow. 

Developers have been flowing into Web3 at an accelerating rate over the past few years. The numbers are still relatively small, but this chart represents the migration toward Web3 and suggests that innovation will follow. 

Chart, line chart

Description automatically generated

Source: Electric Capital, Dec 2021

Why now for Tola?

Tola is investing in the picks and shovels of Web3; in other words, we invest in development. While the front-end of Web3 is roughly the same as Web2, it’s clear that the Web3 tech stack is largely different and as such, requires its own tooling, platforms, and security for developers to build in this new arena. This opportunity plays to our strengths and excites us to our very core. 

Our team has spent many years building organizations that engage and foster developer communities. We know platforms and we love dev tools. (The folks at Microsoft don’t get out of bed for anything other than a platform play.)

One of our top performing Fund I companies is Pulumi, an open source Infrastructure-as-Code platform, that enables developers to program the cloud, and bridge the Dev and Ops divide with cloud engineering. We can see the possibilities when it comes to Web3 to add value through platforms, tools, and community. 

Our Investment in Certora’s Series B

Which brings us to what’s next.

We’re a hypothesis-based firm, which means that we identify areas in need of innovation and we develop the market hypothesis to identify companies in those arenas, ultimately making investments in technologies that make a difference.   

One core hypothesis we’ve been pursuing within Web3 dev tools is QA testing and security. We find this particularly compelling in a blockchain-based environment due to the fact that blockchains are immutable, so deploying smart contracts is arguably more final and more difficult to retract than in traditional Web 2.0 development. As a result, sound and thorough test and security checks are critical for those developing in Web3. 

Most of this market today is manual security auditing which does not scale well and slows development. We met the founders of Certora (based in Israel and Seattle) at ETHDenver and discovered that they are rapidly emerging as leaders in this space with a more automated product-centric approach. 

The co-founders Mooly Sagiv and Shelly Grossman have deep backgrounds in both academia and security software companies, specifically as thought leaders in the realm of formal verification – the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property – using formal methods of mathematics. 

Mooly, Shelly, and the team have leveraged their research and experience in formal verification and security to develop their core SaaS product – Certora Prover. In software, formal verification centers on proving that a program satisfies a formal specification of its behavior. Formal verification as a technique has been around since the 1950s and interestingly, we believe that Mooly and Shelly have found the perfect application for it. 

*Bonus historical reference: The roots of formal verification are traced back to the 1950s in the US and the UK. In 1954, the first computer-generated mathematical proof for a theorem – a decidable fragment of first-order logic called Pressburger arithmetic – was developed by Martin Davis. The theorem being verified at the time was one we all know: that the product of two even numbers is even. Later, in the early 1970s, formal verification made its way into the software realm when Edsger Dijkstra of the Netherlands challenged the software community by claiming that testing wasn’t in itself sufficient since “testing shows the presence, not the absence, of bugs.” 

At a high level, Certora Prover checks the Solidity code, or smart contract, against a pre-defined set of specs to prove that every behavior meets the specs, and if not, identifies bugs or issues. The developer specifies the desired behavior in the spec, and the Certora Prover searches through potentially infinite behaviors to identify bugs. Certora secures  more than 50% of TVL according to

Beyond the incredible talent of these two co-founders and the unique solution they have built, we are thrilled to be supporting a female co-founder in the Web3 space. We’re a diverse team at Tola (and also a female-founded firm) and are committed to investing in founders who have diverse ideas and experiences. 

Certora is growing rapidly and serving many of the top DeFi players today, including Aave and Compound. We couldn’t be more excited to partner with Mooly and Shelly in their $36M Series B round of funding.