Trust but Verify: Scaling Deductive Verification with Abstract Interpretation
summary
Certora Prover verifies EVM and Wasm bytecode by combining abstract interpretation with SMT solving, an internal decompiler to a TP IR, and mutation testing for specs. A bespoke unique pointer analysis for bump-allocation memory recovers high-level structs and enables sound simplifications that speed verification by orders of magnitude and expose real bugs — including multiple compiler-level vulnerabilities (one exploited for ~\$10M). Toolchain focuses on executable-level checks, regression proofs, and spec-driven counterexamples.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 2:10DeFi in one slide
- 8:28Formal verification for DeFi
- 13:23DeFi protocol bugs
- 18:20Tool landscape and Satora
- 23:57Abstract interpretation for low-level code
- 29:20Future of abstract interpretation
- 37:25Formal verification challenges
- 42:39Key takeaways
related talks
06mFormal Verification with the Certora Prover
21mPractical Verification Of Smart Contracts Using Memory Splitting
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
16mAgora: Trust Less and Open More in Verification for Confidential Computing
07mV for Verification
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
28mProving Memory Access Violations in Isabelle/HOL
01h 17mProof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)