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