An Introduction to DeepSEA

DeepSEA is a programming language aimed at enabling scalable formal verification of smart contracts by integrating with the Coq proof assistant. The report outlines DeepSEA's design principles—equational reasoning, layered specification, encapsulation and composition, and built-in abstract refinement—contrasts it with current languages and verification tools, and positions DeepSEA as a solution for producing gas-efficient, formally verified smart-contract code.