How DeepSEA Works

DeepSEA is a programming language and toolchain designed to compile smart contracts to EVM bytecode and produce formal representations for the Coq proof assistant, enabling interactive proofs of correctness (e.g., token transfer invariants). The document outlines the compilation pipeline, differences between executable and Coq representations, example proofs about overflow and token conservation, and the project’s ongoing development status and planned releases.