Rich Specifications for Ethereum Smart Contract Verification
summary
Defines a specification style that proves concrete guarantees: sound reasoning under arbitrary re-entrancy, modular verification of collaborating contracts, and resource-centric assertions that prevent duplication or unauthorized destruction. Implements the approach in 2vyper, an SMT-based verifier for Vyper built on the Viper infrastructure, and applies it to ERC-20 variants, a callback-heavy token, multi-contract apps and Uniswap, successfully producing concise, machine-checked proofs of strong correctness properties.
AI-written summary · about
chapters (10)
- 0:00Rich Specifications for Ethereum Smart Contract Verification
- 0:14What is a smart contract?
- 1:07Smart contract verification vs. OOP
- 2:37This paper
- 3:32Reasoning about (re-entrant) calls
- 7:24Call-independent properties
- 8:36Tokens are Resources
- 10:00Resource Operations
- 12:31Implementation
- 12:54Evaluation
related talks
07mV for Verification
06mFormal Verification with the Certora Prover
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
21mPractical Verification Of Smart Contracts Using Memory Splitting
23mGradual Verification for Smart Contracts
01h 17mProof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)
25mSuccinct Proofs in Ethereum
25mBehavioral simulation for smart contracts