Certora CVL
Certora Verification Language (CVL) is a specification language used with the Certora Prover to formally verify smart contract properties through mathematical proofs.
In Depth
CVL lets you write rules, invariants, and ghost variables that the Certora Prover checks exhaustively against your Solidity code. Unlike fuzzing, which tests with random inputs, CVL verification proves properties hold for all possible inputs within the specified bounds. Rules define expected behavior for individual functions, invariants define properties that must hold across all states, and ghosts track auxiliary state for complex specifications. CVL supports hooks for state tracking, filtered rules for efficiency, and built-in summaries for external calls. See the Certora CVL tutorial for a hands-on guide.
Frequently Asked Questions
What is Certora CVL?
Certora Verification Language (CVL) is a domain-specific language for writing formal specifications of smart contracts. You write rules and invariants in CVL, then the Certora Prover mathematically verifies they hold for all possible inputs and states.
How does Certora compare to fuzzing?
Certora provides mathematical proof that properties hold for all inputs, while fuzzing tests with random inputs and can miss edge cases. However, Certora requires more setup, runs slower, and can struggle with complex multi-contract interactions where fuzzers excel. Most teams benefit from using both. See the fuzzing vs formal verification comparison.