George Pîrlea

Bio / Blog / Teaching / CV

I am a final year PhD student at the National University of Singapore, supervised by Ilya Sergey.

My interests include formal methods, programming languages, distributed systems, and cryptography.

Get in touch via email: [email protected]

Follow me on Twitter: @GeorgePirlea

Google Scholar: George Pîrlea

What's new

14 Nov 2025	Check out our Dafny workshop paper on Lessons from Building an Auto-Active Verifier in Lean, detailing our experience building Veil.
14 Apr 2025	We are excited to release Veil, a new framework for verifying distributed protocols both automatically and interactively, in Lean. The paper will appear at CAV'25.
7 Aug 2024	I have been awarded the Dean's Graduate Research Excellence Award.

Publications

1. Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey. Foundational Multi-Modal Program Verifiers. In Proceedings of the 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026). January 2026. ACM.
2. Ziyi Yang, George Pîrlea, Ilya Sergey. Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference. In Proceedings of the 41st International Conference on Logic Programming (ICLP 2025). September 2025.
3. George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, Ilya Sergey. Veil: A Framework for Automated and Interactive Verification of Transition Systems. Computer Aided Verification (CAV 2025). LNCS 15933. July 2025. Springer.
4. Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, Ilya Sergey. Compositional Verification of Composite Byzantine Protocols. In Proceedings of the 31st ACM Conference on Computer and Communications Security (CCS 2024). October 2024. ACM.
5. 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)
6. 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.
7. 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.
8. 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.
9. 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

Manuscripts

1. George Pîrlea, Vladimir Gladshtein, Qiyuan Zhao, Ilya Sergey. Lessons from Building an Auto-Active Verifier in Lean. Workshop paper. Dafny 2026.
2. Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey. Velvet: A Multi-Modal Verifier for Effectful Programs. Workshop paper. Dafny 2026.
3. Vladimir Gladshtein, George Pîrlea, Ilya Sergey. Small Scale Reflection for the Working Lean User. Unpublished draft. arXiv:2403.12733.

Teaching

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

Theses

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

• Practical Smart Contract Sharding with Ownership and Commutativity Analysis
  Given at PLDI (June 2021) and Formal Reasoning about Financial Systems Workshop (September 2022).
• A Formal Model of Rust's Pinning
  Given at Max Planck Institute for Software Systems (September 2019).
• Formally Verified Blockchain Consensus
  Given at National University of Singapore (March 2019), Zilliqa Research (March 2019), and Max Planck Institute for Software Systems (June 2019).
• Formally Verifying Coco
  Given at Microsoft Research Cambridge (August 2018).
• Mechanising Blockchain Consensus
  Given at CPP (January 2018) and Microsoft Research Cambridge (June 2018).