Code security with the
widest coverage

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

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.

Jared Flatow
VP of Engineering, Compound

Fernando Martinelli
Co-founder & CTO, Balancer

Security superpower at your fingertips

Add the most advanced bug-finding technology to your security toolbox. Learning formal verification doesn't require a math degree, but will push you to think differently about how you approach code security.

Getting Started Tutorial

The fastest way to get started. Learn some foundational skills, then dive into writing formal verification rules.

Start Tutorial

CVL by Example

Practice writing CVL rules with a series of progressively challenging code examples.

View CVL Examples

Docs

Dive into the docs to get familiar with all of the details of using Prover, writing CVL, and learning about other related products.

Docs

Start using Prover
today

Audit

Our team of security experts will analyze your code

Manual review
Formal verification
Custom audit report
Reusable rules

Certora Prover

Free

Run our formal verification tool for free

Up to 2,000 min/month runtime
Write your own rules
Limited support

Get Started

Enterprise

Ongoing analysis & verification of your code as you build it

Unlimited audits
Our experts write rules for your code
Unlimited Prover access
Training & dedicated support
Incident response

Code security with the widest coverage