Application Level Verification of Solidity Smart Contracts

Smart contracts running in a blockchain environment (e.g. ones written in Solidity running on an Ethereum blockchain) need to consist of well defined atomic state updates; otherwise, the properties of the on-chain state become meaningless. Essentially, blockchain transactions need to enjoy the well-known ACID properties familiar from the database world. The (D)urability aspect of such transactions implies that it is practically impossible to back out of a running smart contract once it is live on the blockchain.

So, smart contracts need to be right the first time, and for this, formal verification can play a vital role. Event-B is a formalism for modelling and verifying systems whose behaviour consists of well defined atomic state updates, and is supported by the open-source Rodin toolset. This project aims to explore the feasibility of the basic Event-B framework for designing and verifying Solidity smart contracts and, will build a suitable plugin that could be added to the Rodin tool to support the design of such contracts. The project will investigate novel symbolic verification methods based on SAT modulo theories and abstract interpretation techniques in Rodin to check the discharged verification conditions.