Toychain: Formally Verified Blockchain Consensus
COM1 Level 3
MR1, COM1-03-19
Abstract:
We present the first formalisation of a blockchain-based distributed consensus protocol with a proof of its consistency mechanised in an interactive proof assistant. In this work, we focus on global system safety properties and prove a form of eventual consistency.
Our development includes a reference implementation of the block forest data structure and provably-correct message handlers for the protocol logic. The development is parametric wrt. implementations of several security primitives, such as hash-functions, a notion of a proof object, a Validator Acceptance Function, and a Fork Choice Rule. We precisely characterise the assumptions, made about these components for proving the global system consensus, and discuss their adequacy.
Finally, we instantiate Toychain with a SHA256-based proof-of-work scheme and extract a proven-correct OCaml implementation of a blockchain consensus protocol.
All our results are formalised in the Coq interactive theorem prover.
Biodata:
George Pirlea is a researcher at University College London. His recent projects include mechanised verification of consensus protocols (working as a part of Ilya Sergey's group), as well as creating a formal model of Microsoft's Coco framework.