1. George Pîrlea and Ilya Sergey. Mechanising Blockchain Consensus. In 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018). Los Angeles, CA,USA, January 2018. ACM.


  1. Toychain: Formally Verified Blockchain Consensus
    MEng Thesis. Advised by Earl Barr and Ilya Sergey.

    Abstract: We present Toychain, the first proven-correct implementation of a Nakamoto-style blockchain consensus protocol. 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.

Selected Talks