Towards Formally Verified Smart Contracts with Haskell

In enterprise DLTs, smart contracts implement security critical and business critical logic. Therefore there is a clear need to have confidence that smart contracts adhere to the intended specificatio …

In enterprise DLTs, smart contracts implement security critical and business critical logic. Therefore there is a clear need to have confidence that smart contracts adhere to the intended specification, without any errors, bugs or malicious code. Events like the DAO attack on the Ethereum blockchain in 2016 is unacceptable in a permissioned, enterprise solution. In order to guarantee the correctness of a smart contract, formal verification is necessary. Because of this, there is a strong research focus in the wider blockchain community on enabling formal verification of smart contracts written in functional programming languages (e.g. DAML, Liquidity, F*, Elle, Verisol, etc.). Functional programming languages lend themselves well to formal verification due to the fact that both formal verification and functional programming have their roots in mathematics. However, to date, little work within the Hyperledger community has been done on bringing formal verification to smart contracts on Hyperledger DLTs.This talk presents support for writing Hyperledger Fabric chaincode with Haskell, a big first step towards having fully verified and secure smart contracts. The work is evaluated by comparing contracts written in Go, Java and Node with Haskell to demonstrate how a functional programming language can help identify flaws in logic, leading to code that is both correct, secure and easier to reason with. The talk finally demonstrates how smart contracts written in Haskell can be formally verified.