Smart contracts are computer programs running on the blockchain. Often, they capture the behaviour of “contracts” from the real world, such as wallets, auctions, ICOs, etc.

Early smart contract languages were important to explore the space, but with bugs in smart contracts leading to huge financial losses, there is now a realization that one needs a clear understanding of the meaning (semantics) of financial contracts. Modern programming languages come with such a precise semantics. Moreover, many of the properties of the language and their tools (compilers, interpreters) are nowadays proved with a computer proof assistant. We will use the Coq proof assistant to build verified tooling for smart contract languages, and build a framework to specify, test and prove properties of smart contracts. In this way we can give a mathematical proof that the smart contract behaves as advertised.

As part of this, we will need a precise specification and reference implementation of the blockchain, including the consensus layer, the transaction layer, and the smart contract language itself. Because of the complexity of this software stack, it is crucial that we model the system in a modular way.