Modelling a Blockchain for Smart Contract Verification using DeepSEA
summary
DeepSEA models the blockchain as a state record plus an inductive action type where each call requires a proof that it will succeed; this successful-call approach forces proofs to focus only on non‑reverting executions and collapses many spurious branches. The paper proves crowdfunding properties: donations are backed by contract balance, donations persist unless claimed, and backers can reclaim after failure, while the DeepSEA pipeline still refines down to Ethereum bytecode. Limitation: actions are dependent on prior states, complicating lists and some proof engineering.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 2:13DeepSEA and crowdfunding
- 5:49Successful call approach
- 8:20Blockchain model implementation
- 12:33Approach in proofs
- 15:01Older proof methods comparison
- 16:29Limitations and summary
- 18:36Q&A
related talks
45mSmart contracts in a blockchain change everything
25mBehavioral simulation for smart contracts
24mAn Introduction to Smart Contracts
51mBlockchain and smart contracts (...)
12mSmart Contract Security
33mSmart Contract-driven AI: A New Era of Decentralization
04mInterview
17mMakerDAO Smart Contract Safety - When Billions are at Stake