Foundational Verification of Smart Contracts through Verified Compilation
<|reference_start|>Foundational Verification of Smart Contracts through Verified Compilation: 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.<|reference_end|>
@article{sjöberg2024foundational,
    title={Foundational Verification of Smart Contracts through Verified
  Compilation},
    author={Vilhelm Sj"oberg, Kinnari Dave, Daniel Britten, Maria A Schett,
  Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, Zhong Shao},
    journal={arXiv preprint arXiv:2405.08348},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.08348},
    primaryClass={cs.PL}
}