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.

Short bio in plain text and 3rd person

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

  1. Lazy Proof Automation for Separation Logic
    ITP 2026. LIPIcs, Schloss Dagstuhl.
  2. Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean
    CAV 2026. Springer.
  3. Foundational Multi-Modal Program Verifiers
    Proc. ACM Program. Lang. 2026. (POPL), ACM.
  4. Veil: A Framework for Automated and Interactive Verification of Transition Systems
    CAV 2025. Springer.
  5. Accelerating Automated Program Verifiers by Automatic Proof Localization
    CAV 2025. Springer.
  6. Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis
    USENIX Security Symposium 2025. USENIX Association.
  7. Compositional Verification of Composite Byzantine Protocols
    31st ACM Conference on Computer and Communications Security (CCS’24) 2024. ACM.

lecture notes

  1. Programs and Proofs: Mechanizing Mathematics with Dependent Types
    Ilya Sergey
    Lecture notes with exercises.

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.