Certora Book
Formal Verification with Certora
Formally verify smart contracts using the Certora Verification Language and Certora Prover.
This tutorial series teaches how to formally verify Solidity smart contracts with Certora's open-source formal verification tool. Readers should have at least an intermediate grasp of Solidity syntax and familiarity with popular ERC standards.
If you need help with CVL, you can ask on Certora's Discord.
1.
Introduction to Formal Verification
2.
Formally Verifying a Counter
3.
Understanding the Spec File in Certora CVL
4.
Certora Require, Assert, and Satisfy
5.
Testing Revert Call In Certora
6.
Overflow and Mathint
7.
Conditional Statements in CVL and Formally Verifying Parts of Solady and Solmate
8.
Implication Operator
9.
Biconditional Operator
10.
Formally verifying Initializable.sol
11.
Testing msg.sender and msg.value in CVL
12.
Formally Verifying Address Balance
13.
Introduction to Parametric Rules
14.
Introduction to Method Properties
15.
Formally Verifying Nonces.Sol in OpenZeppelin
16.
Formally Verifying Ownable.sol
1.
Introduction to Invariants in Certora
2.
Introduction to Storage Hooks and Ghosts
3.
Constraining the Ghost Values in Rules
4.
Constraining Ghosts in Invariants
5.
Using Sstore Hooks with Storage Mappings
6.
Using Sload Hooks with Storage Mappings
7.
Verifying an Invariant Using Ghost and Hook
8.
Preserved Block and Its Role in Invariant Verification
9.
Using “requireInvariant" in Rules and Invariants
10.
Persistent Ghosts
11.
Loops in CVL: Path Explosion and Loop Unrolling
12.
Formally Verify an ERC-20 Token
13.
Formally Verify Solady WETH
14.
Mint and Burn Rules for ERC-721
15.
Invariants for ERC-721
16.
Transfer and Approval Rules for ERC-721
17.
SafeMint and SafeTransfer Rules in ERC-721
18.