Gradual Verification for Smart Contracts
summary
Gradual verification combines static separation-logic proofs with imprecise specifications (written as question marks) and automatically emits dynamic checks where the static verifier is optimistic, preserving soundness, a gradual guarantee, and conservative extension. Prototype GradualP targets Algorand by translating pyTEAL-like Python to a Gradon/Viper backend, producing runtime assertions (an example reduces five brute-force asserts when some properties are proved statically) and inserting reentrancy state-invariance checks before external calls.
AI-written summary · about
chapters (8)
- 0:00Gradual verification intro
- 3:31Verifying smart contracts
- 7:05Core concepts of gradual verification
- 8:30Benefits of gradual verification
- 11:01Gradual P framework for Algor
- 13:47Incremental verification example
- 15:10Future directions and challenges
- 15:56Q&A on gas fees
related talks
07mV for Verification
14mRich Specifications for Ethereum Smart Contract Verification
49mAlgorand Smart Contract Architecture
19mGradually Typed Languages Should Be Vigilant!
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
15mCompositional Verification of Smart Contracts Through Communication Abstraction
27mProofs of proofs: incremental verifiability from recursion and accumulation
25mBehavioral simulation for smart contracts