Phoenix, Arizona
March 3-6
More Information & Registration
Back To Schedule
Tuesday, March 3 • 5:05pm - 5:45pm
Towards Formally Verified Smart Contracts with Haskell - Allison Irvin & Nick Waywood, IBM

Sign up or log in to save this to your schedule, view media, leave feedback and see who's attending!

Feedback form is now closed.
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.


Allison Irvin

Software Engineer, IBM
Allison Irvin studied a Bachelor of Science and a Master of Engineering (Mechatronics) at the University of Melbourne and is a software engineer and researcher at IBM. In addition to authoring several scientific research publications, Allison is emerging as a young technical leader... Read More →
avatar for Nick Waywood

Nick Waywood

Software Engineer, IBM Research
Nick Waywood is a full-stack software engineer at IBM Research - Australia. He has led the design and implementation of a number of research prototypes over the past 6 years, ranging from platforms for running scientific workloads to applications in the Healthcare and Blockchain domains... Read More →

Tuesday March 3, 2020 5:05pm - 5:45pm MST
104 A
  Technical Track