Foundational Verification of Smart Contracts through Verified Compilation

Daniel Britten; Kinnari Dave; Maria A Schett; Qinshi Wang; Sean Noble Anderson; Steve Reeves; Vilhelm Sj\"oberg; Xinyuan Sun; Zhong Shao

Foundational Verification of Smart Contracts through Verified Compilation

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2405.08348 v1 pith:QJURDOOY submitted 2024-05-14 cs.PL

Foundational Verification of Smart Contracts through Verified Compilation

Vilhelm Sj\"oberg , Kinnari Dave , Daniel Britten , Maria A Schett , Xinyuan Sun , Qinshi Wang , Sean Noble Anderson , Steve Reeves

show 1 more author

Zhong Shao

This is my paper

classification cs.PL

keywords deepseasmartcontractcontractscorrectnessfoundationalsystemverification

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

0 comments

read the original 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.

discussion (0)

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens
cs.PL 2026-07 conditional novelty 7.0

Using EquiVM, LLM agents produced Lean-checked refinement proofs for 23 real-world EVM contracts, certifying bytecode against a Sol− specification at token cost.