Verication-Led Smart Contracts

Abstract

Turing complete smart contract formalisms (e.g. Solidity)<br/>are conceptually appealing, but leave the door open to the problems of<br/>verifying completely arbitrary code, a task which can be of arbitrarily<br/>high complexity or can be undecidable. We argue that a more structured<br/>approach, in which smart contract families are designed ab initio with<br/>efficient veriability in mind, provide a much more practical way for-<br/>ward. We emphasise that the boundary between on-chain and off-chain<br/>information, which must always be determined in an application specic<br/>manner, is crucial in determining the practicability of smart contract<br/>verification. We discuss the role of refinement technologies in breaking<br/>down the complexity of smart contract verification, and illustrate the<br/>argument using the Event-B formal modelling framework and Solidity<br/>as implementation vehicle.