What's new

13 Dec 2023 Our work on verifying tree clocks in Coq will be presented at CPP'24 in London.
14 Aug 2023 Our paper on fuzzing distributed systems is accepted at CCS'23.


  1. Vladimir Gladshtein, George Pîrlea, Ilya Sergey. Small Scale Reflection for the Working Lean User. Under submission.
  2. Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey. Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024). January 2024. ACM. (Distinguished Paper Award)
  3. Ruijie Meng*, George Pîrlea*, Abhik Roychoudhury, and Ilya Sergey. Greybox Fuzzing of Distributed Systems. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS 2023). November 2023. ACM.
  4. Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, and Ilya Sergey. Certifying the Synthesis of Heap-Manipulating Programs. In Proc. ACM Program. Lang. 5 (ICFP 2021). August 2021. ACM.
  5. George Pîrlea, Amrit Kumar, and Ilya Sergey. Practical Smart Contract Sharding with Ownership and Commutativity Analysis. In 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Virtual, Canada. June 2021. ACM.
  6. 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.
* - joint first author


  1. CS3243 Introduction to Artificial Intelligence (AY 2020/21 Sem 2)
  2. YSC3208 Programming Language Design and Implementation (AY 2020/21 Sem 1)


  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