Foundational Verification of Smart Contracts through Verified Compilation
Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria A Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, Zhong Shao
TL;DR
The paper presents DeepSEA, a foundational verification framework for Ethereum smart contracts that combines a small, verification-friendly programming language with a fully verified compiler. By outputting both Ethereum bytecode and a Coq model of the contract, DeepSEA enables true end-to-end proofs about contract behavior, including gas-related aspects and data-representation invariants. The authors demonstrate the approach on two realistic case studies—the Uniswap-style AMM and a crowdfunding contract—showing both complex interactive proofs and practical usability. This work advances reliable smart-contract development by enabling high-assurance proofs that are tied directly to the execution semantics of the target platform, promising safer DeFi and decentralized applications at scale.
Abstract
Programs executed on a blockchain - smart contracts - have high financial stakes; their correctness is crucial. We argue, that this correctness needs to be foundational: correctness needs to be based on the operational semantics of their execution environment. In this work we present a foundational system - the DeepSEA system - targeting the Ethereum blockchain as the largest smart contract platform. The DeepSEA system has a small but sufficiently rich programming language amenable for verification, the DeepSEA language, and a verified DeepSEA compiler. Together they enable true end-to-end verification for smart contracts. We demonstrate usability through two case studies: a realistic contract for Decentralized Finance and contract for crowdfunding.