TL;DR
This paper introduces a formal, executable model of smart contract execution in Coq that supports inter-contract communication and different blockchain execution models, enabling rigorous reasoning about contract correctness.
Contribution
It provides a novel Coq-based formalization of smart contracts that models various blockchain execution styles and includes a verified example of a complex, communication-heavy contract.
Findings
Successfully modeled both Ethereum and Tezos execution styles.
Developed a verified Congress contract with dynamic communication.
Proved correctness properties related to reentrancy for the Congress contract.
Abstract
We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) and breadth-first execution blockchains (like Tezos). We represent smart contracts programs in Coq's functional language Gallina, enabling easier reasoning about functional correctness of concrete contracts than other approaches. In particular we develop a Congress contract in this style. This contract -- a simplified version of the infamous DAO -- is interesting because of its very dynamic communication pattern with other contracts. We give a high-level partial specification of the Congress's behavior, related to reentrancy, and prove that the Congress satisfies it for all possible smart contract execution orders.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
