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.
Prover tests your code properties mathematically so you know they will hold given any contract state.
Integrate Prover into your development cycle to run every time you change your code.
Share your report with your team in one click using the Prover Dashboard.
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
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.
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
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
Free
Run the leading formal verification tool for free
Integrate the tool trusted by top DeFi protocols to keep their code secure
Ongoing analysis & verification of your code as you build it