Ilya Sergey
Associate Professor at National University of Singapore
I am a tenured Associate Professor at the School of Computing of National University of Singapore, where I lead the VERSE lab as a part of PLSE@NUS group. I am also a Research Consultant at Mysten Labs.
I do research in programming languages, software verification, distributed systems, and program synthesis. Nowadays, most of my work involves engineering mechanised proofs in the Lean proof assistant.
I serve as a Program Committee Co-Chair for OOPSLA’27, I was the General Chair for ICFP’25 and the Local Chair for the joint ICFP/SPLASH’25 Conference. I also organised the ICFP Programming Contest 2019. I am the recipient of the AITO Dahl-Nygaard Junior Prize 2019. In the past, I designed and co-developed Scilla programming language. Before joining academia I worked as a software engineer at JetBrains.
coordinates
| Postal Address: | School of Computing, National University of Singapore COM1, 13 Computing Drive, Singapore 117417 |
| Email: | |
| Office: | COM3-02-56 |
| Office Phone: | +65 6601 1466 |
| Availability: | Outlook Calendar |
announcements
- I am not looking for new PhD students, postdocs, or research interns for the 2026/27 Academic Year.
news
| May 26, 2026 | Honoured to receive an Amazon Research Award for the project “Linear Types for a Foundational Multi-Modal Program Verifier”! |
| May 25, 2026 | Our paper on Lazy Proof Automation for Separation Logic will appear at ITP 2026! |
| May 18, 2026 | New post on Proofs and Intuitions: On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications, on how property-based testing surprisingly outperforms symbolic methods at detecting issues in LLM-synthesised Lean specifications. |
| Apr 30, 2026 | Our paper Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean has been accepted to CAV 2026! |
| Apr 13, 2026 | I have given a talk on my experiments in AI-Assisted Metatheory at the FP Launchpad Kickoff at IIT Madras. |
| Apr 2, 2026 | Veil has been featured as one of the verification use cases on the official Lean website! |
| Mar 31, 2026 | Excited to announce that our Dagstuhl Seminar The Next 20 Years of Computer-Assisted Theorem Proving has been accepted! I will be co-organising it with Sandrine Blazy, Jonathan Protzenko, and Sebastian Ullrich. The seminar will take place on February 21–26, 2027. |
| Mar 18, 2026 | New post on Proofs and Intuitions: Verifying Move Borrow Checker in Lean: an Experiment in AI-Assisted PL Metatheory, in which I describe how I mechanised Move’s borrow checker in Lean with AI assistance, producing 39,000 lines of metatheory in about one month. |
selected publications
miscellanea
Last time I checked, my Erdős number was 4.
Here is a high-resolution "official" photo of me, suitable for appropriate occasions. Just in case, here's a more casual picture, couresy of Elena Alhimovich. Yet another old picture of mine by Jorge Cham, for I have contributed to the PHD Movie 2 on Kickstarter.
While living in Madrid, I enjoyed its inimitable atmosphere and delicious food. For the latter, this Maribel's Dining Guide to Madrid (kindly provided by Aleks Nanevski) always came in handy.