Code security with the widest coverage

Catch even the rarest bugs with the leading formal verification tool available.

Get Started for Free

Harness the Power of Formal Verification

Use the same technology that keeps airplane software secure to prove that your contracts will behave exactly as expected, no matter the state of your contract.

Catch hard-to-find bugs

Prover tests your code properties mathematically so you know they will hold given any contract state.

Run on every commit

Integrate Prover into your development cycle to run every time you change your code.

Shareable Bug Report

Share your report with your team in one click using the Prover Dashboard.

How Prover Works

Write a CVL Rule

Similar to how you might write a Foundry fuzz test, you start by writing a rule that defines how you want your contract property to behave. This rule, also known as a specification, is written using the Certora Verification Language (CVL), which has a syntax that is very close to Solidity but with a few added features.

/Specs/Auction.spec

/// auction bid increases contract balance rule bidIncreasesAssets() { env e; // represents global variables like msg.sender require(e.msg.sender != currentContract); require(e.msg.value > currentBid() ); uint256 balanceBefore = nativeBalances[currentContract]; bid(e); assert nativeBalances[currentContract] > balanceBefore; }

Run Prover

Prover compares your rule against your smart contract bytecode to identify scenarios where your code properties could lead to bugs. Additionally, the prover presents a concrete call trace leading to the bug. Unlike fuzzing, Prover compiles your contract down into math to evaluate every possible contract state and contract path.

Analyze results

View results on the Prover Dashboard to see if any of your code properties could be violated under any condition. You will be able to identify even the most hard-to-find bugs that can emerge with complex smart contracts.

Certora Prover helped to cover security on the Aave Protocol, finding vulnerabilities that are usually difficult to find in manual code reviews and audits.

Stani Kulechov

CEO & Founder, Aave

Certora has given us the ability to practically apply formal verification methods to anything we do on-chain.

Jared Flatow

VP of Engineering, Compound

Certora has been a crucial partner along Balancer's journey to ensure excellence in our code quality and security.

Fernando Martinelli

Co-founder & CTO, Balancer

Start using Prover today

Basic

Free

Run the leading formal verification tool for free

  • Up to 2,000 min/month runtime
  • Write your own rules
  • Discord support
Get Started

Premium

Integrate the tool trusted by top DeFi protocols to keep their code secure

  • Unlimited Prover access
  • Setup & onboarding support
  • Up to 10 team members
  • Specification review
Contact Us

Enterprise

Ongoing analysis & verification of your code as you build it

  • Audit + formal verification retainer
  • Our experts write rules for your code
  • Unlimited Prover access
  • Training & dedicated support
  • Incident response
Contact Us
Certora Logo
logologo
Terms of UsePrivacy Policy