Certora Levels the Playing Field, Open-Sourcing Prover for DeFi Security

Certora, a leading blockchain security platform, has open-sourced its most advanced formal verification engine, Certora Prover, to make smart contract security more accessible for everyone in the crypto sector.

This move from Certora couldn’t have come at a better time as hackers proliferate the digital asset space and steal funds.

“Security remains one of the biggest challenges in Web3. DeFi projects spend millions on audits and often take over a year to launch, yet vulnerabilities continue to put billions of dollars at risk,” remarked Certora CTO Shelly Grossman, adding, “While high-profile exploits have become less frequent, securing smart contracts remains expensive and out of reach for many developers. That changes today.”

Data from blockchain analysis firm Chainalysis reveals that a whopping $2.2 billion was stolen by hackers in 2024, which is an increase of 21% from a year ago. Not only has the dollar amount surged, but so has the number of incidents.

As the crypto adoption rises, gaining traction among both retail and institutions, and the market booms with the total cryptocurrency market cap sitting above $3 trillion, bad actors are certainly multiplying. These cybercriminals are adopting increasingly sophisticated methods and broadening their scope by exploiting weaknesses in smart contracts, which are the backbone of protocols and the DeFi ecosystem. 

Against this backdrop, Certora is offering a powerful solution to DeFi developers, which identifies all possible bugs and then proves their absence. By supporting multiple popular chains, viz. Ethereum (EVM), Solana (sBPF), and Stellar (WASM), Certora ensure that the vast majority of the crypto space is protected against smart contract attacks.

Prover is Certora’s flagship security product, which utilizes formal verification to catch the hardest and rarest bugs. In production for “a long time,” the tool is finally released to the general public.

The Certora Prover essentially acts as an automated mathematical auditor, analyzing smart contract code and developer-defined rules to provide proof of correctness. This way, it goes beyond limited scenarios, evaluating every possible case. Developers have already written over 70,000 verification rules.

It was actually with the help of Certora’s formal verification technology that a fundamental flaw in MakerDAO’s DAI equation, which has been undetected since 2018, was finally caught. Findings like this show that even multiple audits can’t fully remove the vulnerabilities of a smart contract, but a formal verification can help uncover them.

With this tool, Cetora has also been helping the likes of Aave, Uniswap, Lido, EigenLayer, Solana Foundation, and many others protect tens of billions of dollars in TVL. 

However, Certora had its code closed-sourced all this time, which is finally changing in a move to offer all the developers in Web3 a strong tool for absolutely free to make sure that their smart contracts are secure, transparent, and community-driven.

“Smart contract security should not be a privilege reserved for well-funded teams or highly educated people. Open-sourcing the Certora Prover is a step toward making bulletproof smart contracts the norm,” said Certora CEO Mooly Sagiv.

Freely available for all, Certora is currently inviting developers, security researchers, and the Web3 community to employ the solution to verify their smart contracts and help advance its efforts to make DeFi secure.