A model of Solidity-style smart contracts in the theorem prover Agda

Abstract

The use of smart contracts is transforming traditional industry and business practices. It enables the automatic enforcement of contractual terms without the need for a trusted third party. Smart contracts can automate a variety of transactions on Blockchain. Despite their numerous benefits, some challenges, such as security vulnerabilities, still need to be addressed before smart contracts can be widely adopted.This paper introduces two models of smart contracts – one simple and one more complex – using the interactive theorem prover Agda. This is a step towards converting the previous work of verifying Bitcoin smart contracts using weakest preconditions [1], [2] to Ethereum’s Solidity-style [3] smart contracts. Since Ethereum’s contracts are object-oriented, this model is substantially more complex than Bitcoin’s. We provide models supporting simple and complex executions, the calling of other contracts, and functions referring to addresses and messages. Furthermore, these models also support transferring money to other contracts and updating specific contracts, and the more complex model includes gas cost and pure functions.