Move fast, break nothing.

Secure your smart contracts with industry-leading formal verification tools & smart contract audits.

Get started free Request an audit

Over $100B TVL Protected

Prove your code works with mathematical certainty

Certora Prover is a powerful tool that compares your smart contract bytecode against a rule detailing how you expect your code to behave. This process, known as formal verification, will check every possible contract state and contract path to identify critical vulnerabilities that hackers can exploit.

Solidity

/contracts/ERC20.sol

contract ERC20 is IERC20, IERC20Metadata {
...
    function transferFrom(address sender, address recipient, uint256 value) public virtual returns (bool) {
        _spendAllowance(sender, msg.sender, value);
        _transfer(sender, recipient, value);
        return true;
    }
...

Rule

/specs/ERC20.spec

// Checks that transferFrom() decreases allowance of `e.msg.sender`

rule checkTransferFrom(address sender, address recipient, uint256 amount) {
    env e; // represents global variables like msg.sender
    require sender != recipient && amount > 0;

    uint256 allowanceBefore = allowance(sender, e.msg.sender);
    transferFrom(e, sender, recipient, amount);
    uint256 allowanceAfter = allowance(sender, e.msg.sender);
    
    assert (allowanceBefore > allowanceAfter),
        "allowance must decrease..."; // error message 
}

Learn about Prover

Use the most powerful security tools available

Run on every commit

Secure your code on every commit by integrating Prover into your development pipeline.

Find more bugs

Catch rare and hard-to-find bugs using our formal verification tools that give you the widest coverage.

Hire our experts

Hire our team of formal verification experts to write custom rules that ensure the security of your code.

Code security that
inspires confidence

Find the right solution for you, whether you run our tools yourself or hire our team of experts to secure your code.

Integrate into your process

Certora Prover

Run on every commit
Check every contract state
Check every contract path
Verify your contract properties

Learn About Prover

Dedicated audit team

Security Audits

Dedicated auditors
Formal verification experts
Detailed report
Interactive process with team

Explore Audits

Engage our community

Work with our community to crowdsource custom formal specifications to find vulnerabilities in your code. We run frequent community audit contests together with leading platforms like Code4rena.

Learn More