Mechanising blockchain consensus. - George Pîrlea; Ilya Sergey (CPP, 2018)

Compiling a Higher-Order Smart Contract Language to LLVM. - Vaivaswatha Nagaraj; Jacob Johannsen; Anton Trunov; George Pîrlea; Amrit Kumar 001; Ilya Sergey (CoRR, 2020)

Practical smart contract sharding with ownership and commutativity analysis. - George Pîrlea; Amrit Kumar 001; Ilya Sergey (PLDI, 2021)

Certifying the synthesis of heap-manipulating programs. - Yasunari Watanabe; Kiran Gopinathan; George Pîrlea; Nadia Polikarpova; Ilya Sergey (Proc. ACM Program. Lang., 2021)

Greybox Fuzzing of Distributed Systems. - Ruijie Meng; George Pîrlea; Abhik Roychoudhury; Ilya Sergey (CCS, 2023)

Distributed System Fuzzing. - Ruijie Meng; George Pîrlea; Abhik Roychoudhury; Ilya Sergey (CoRR, 2023)

Compositional Verification of Composite Byzantine Protocols. - Qiyuan Zhao; George Pîrlea; Karolina Grzeszkiewicz; Seth Gilbert; Ilya Sergey (CCS, 2024)

Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. - Qiyuan Zhao; George Pîrlea; Zhendong Ang; Umang Mathur 001; Ilya Sergey (CPP, 2024)

Small Scale Reflection for the Working Lean User. - Vladimir Gladshtein; George Pîrlea; Ilya Sergey (CoRR, 2024)

Bythos: Compositional Verification of Composite Byzantine Protocols. - Qiyuan Zhao; George Pîrlea; Karolina Grzeszkiewicz; Seth Gilbert; Ilya Sergey (Zenodo, 2024)

Veil: A Framework for Automated and Interactive Verification of Transition Systems. - George Pîrlea; Vladimir Gladshtein; Elad Kinsbruner; Qiyuan Zhao; Ilya Sergey (CAV (3), 2025)