Foundational Verification of Smart Contracts through Verified Compilation

TL;DR

This paper introduces the DeepSEA system, a verified compilation framework for Ethereum smart contracts, ensuring correctness based on operational semantics and enabling end-to-end verification for critical financial applications.

Contribution

It presents a verified compiler and programming language for smart contracts, providing a foundational approach to correctness in blockchain applications.

Findings

Verified DeepSEA compiler ensures correctness

Case studies demonstrate practical usability

Supports end-to-end verification of smart contracts

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.