Toychain: Formally Verified Blockchain Consensus

Abstract

We present Toychain, the first proven-correct implementation of a Nakamoto-style blockchain consensus protocol. We build upon our previous work, the first formalisation of a blockchain-based distributed consensus protocol with a mechanised proof of consistency. Our formalisation includes a reference implementation of the block forest data structure and provably-correct message handlers for the protocol logic. The formal model 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 improve our original model by removing several overly-strong assumptions, notably the assumption that hashing is injective. Then, we instantiate the model with a SHA256-based proof-of-work scheme and extract our proven-correct OCaml implementation of Nakamoto consensus. Finally, we execute our implementation on a local area network to test its effectiveness. All our results are formalised in the Coq interactive theorem prover.

Publication
Master’s thesis
Date
Avatar
George Pîrlea
Undergrad student