Using EquiVM, LLM agents produced Lean-checked refinement proofs for 23 real-world EVM contracts, certifying bytecode against a Sol− specification at token cost.
Foundational Verification of Smart Contracts through Verified Compilation
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
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.
fields
cs.PL 1years
2026 1verdicts
CONDITIONAL 1representative citing papers
citing papers explorer
-
Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens
Using EquiVM, LLM agents produced Lean-checked refinement proofs for 23 real-world EVM contracts, certifying bytecode against a Sol− specification at token cost.