The Smart Contract Model
Yackolley Amoussou-Guenou, Maurice Herlihy, Sucharita Jayanti, Maria Potop-Butucaru, Sergio Rajsbaum
TL;DR
The paper introduces a formal smart contract model for cross-chain coordination, where contracts on multiple ledgers act as trusted state machines and parties may act irrationally or dishonestly. It defines cross-chain systems, tasks, and protocols using interface automata, and grounds correctness in game-theoretic concepts such as Coalition Nash Equilibrium, along with safety and liveness guarantees under bounded timing $\Delta$. A central case study of a two-party cross-chain swap illustrates how a hashlock-based escrow across ledgers can achieve a secure, atomic-like transfer when both parties comply, and how deviations are handled without sacrificing safety. This framework aims to adapt classical distributed computing insights to blockchain environments and points toward future work on oracles, bridges, and probabilistic or cryptographic enhancements to broaden applicability and robustness.
Abstract
Many of the problems that arise in the context of blockchains and decentralized finance can be seen as variations on classical problems of distributed computing. The smart contract model proposed here is intended to capture both the similarities and the differences between classical and blockchain-based models of distributed computing. The focus is on cross-chain protocols in which a collection of parties, some honest and some perhaps not, interact through trusted smart contracts residing on multiple, independent ledgers. While cross-chain protocols are capable of general computations, they are primarily used to track ownership of assets such as cryptocurrencies or other valuable data. For this reason, the smart contract model differs in some essential ways from familiar models of distributed and concurrent computing. Because parties are potentially Byzantine, tasks to be solved are formulated using elementary game-theoretic notions, taking into account the utility to each party of each possible outcome. As in the classical model, the parties provide task inputs and agree on a desired sequence of proposed asset transfers. Unlike the classical model, the contracts, not the parties, determine task outputs in the form of executed asset transfers, since they alone have the power to control ownership.