Code security with the
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.
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.
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.
CVL by Example
Practice writing CVL rules with a series of progressively challenging code examples.
View CVL Examples
Dive into the docs to get familiar with all of the details of using Prover, writing CVL, and learning about other related products.
Start using Prover
Our team of security experts will analyze your code
- Manual review
- Formal verification
- Custom audit report
- Reusable rules
Run our formal verification tool for free
- Up to 2,000 min/month runtime
- Write your own rules
- Limited support
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