Good news for researchers in formal verification: smart contracts regularly suffer exploits such as the DAO bug, which lost the equivalent of 60 million USD on Ethereum. This makes a strong case for applying formal methods to guarantee essential properties.
Which properties would we like to prove? Most previous studies focus on contract-specific properties that do not generalize to a wide class of smart contracts. There is currently no commonly agreed upon list of properties to use as a starting point in writing a formal specification.
We propose three properties that we believe are relevant to all smart contracts: Validity, Liquidity, and Fidelity. Focusing on the concrete case of the Cardano platform, we show how these properties stop exploits similar to the DAO bug, as well as preventing other common issues such as the locking of funds and double satisfaction.
We model an account simulation, a multi-signature wallet, and an order book decentralized exchange, as example smart contract specifications using state transition systems in the Agda proof assistant. We formalize the above properties and prove they hold for the models. The models are then separately proven to be functionally equivalent to a validator implementation in Agda, which is translated to Haskell using agda2hs. The Haskell code can then be compiled and put on the Cardano blockchain directly. We use the Cardano Node Emulator to run property-based tests and confirm that our validator works correctly.
# Available in: doi.Lambda calculi are often used as intermediate representations for compilers. However, they require extensions to handle higherlevel features of programming languages. In this paper we show how to construct an IR based on System Fμω which supports recursive functions and datatypes, and describe how to compile it to System Fμω. Our IR was developed for commercial use at the IOHK company, where it is used as part of a compilation pipeline for smart contracts running on a blockchain.
# Available in: pdf, doi.System F, also known as the polymorphic λ-calculus, is a typed λ-calculus independently discovered by the logician Jean-Yves Girard and the computer scientist John Reynolds. We consider Fωμ, which adds higher-order kinds and iso-recursive types. We present the first complete, intrinsically typed, executable, formalisation of System Fωμ that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System Fωμ. The paper is a literate Agda script.
# Available in: pdf, doi.