DeepSEA: Advanced Web3 Formal Verification of a Smart Contract Compiler

This report describes DeepSEA, a formally verified compiler for smart contracts built in Coq that translates a minimal DeepSEA surface language through an intermediate MiniC into EVM or eWASM bytecode. It explains the compiler architecture, the methodology for proving correctness of each compilation phase (including match_states relations and transf_step_correct theorems), and how a verified compiler integrates with formal verification to produce trustworthy high-level models for verifying real-world DeFi code like a Uniswap-like swap method.