Move fast, break nothing.

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

$25B+ 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.



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



// 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
Certora Logo
Terms of UsePrivacy Policy