Formal Verification with the Certora Prover
summary
A formal verifier that translates contracts plus specs in CVL domain-specific language into logical formulas and uses multiple SMT solvers to produce either a proof or a concrete example transaction counterexample. Timeouts are common but typically around two hours. Supports quantified checks over storage and arbitrary method calls, explicit invariants, revert-path reasoning and state rewind. Demonstrated finding an ERC‑20 transfer issue where sender==recipient leaves balances unchanged, then verifies successfully after adding the missing precondition.
AI-written summary · about
chapters (5)
- 0:00Start
- 0:21Formal Verification with the Certora Prover
- 1:14Formal Verification vs. Fuzzing
- 2:41Certora Verficiation Language (CVL) Features
- 4:04Example / demo
related talks
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
14mRich Specifications for Ethereum Smart Contract Verification
25mVerifying LLM powered Code Transformations with Equivalence Checking
01h 25mIntroduction to Verifiable Computing
32mVerifying Constant-Time Implementations
21mPractical Verification Of Smart Contracts Using Memory Splitting
27mProofs of proofs: incremental verifiability from recursion and accumulation