Ilya Sergey

I am Co-Founder and Chief Science Officer of &Truth, where I lead the company’s innovation and technical work. I am also an Associate Professor at the School of Computing of National University of Singapore, where I direct the VERSE lab.

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. 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 on leave from NUS at &Truth and am not looking for new PhD students, postdocs, or research interns for the 2027/28 Academic Year.

news

Oct 29, 2026	&Truth, the company I co-founded, is out of stealth! Together with a team I’m immensely proud to be part of, our ambition is to specify and prove all the world’s software correct and secure. Join us!
Oct 18, 2026	New post on Proofs and Intuitions: The Vermilion Experiment: Implementing a Lean Backend for Verus.
Sep 28, 2026	A two-weekend fun project: Vermilion, an experimental Lean 4 backend for the Verus verifier for Rust. Verification conditions are readable Lean theorems, provable with an SMT solver, Lean’s `grind`, Mathlib lemmas, by hand, or by your favourite AI system.
Sep 18, 2026	We have released a new version of Velvet, our foundational multi-modal verifier for imperative programs in Lean, with a number of new features. It now has a new web site!
Aug 15, 2026	Four papers from VERSE lab will appear at OOPSLA 2026: Infinitary Relational Logic Tracking Borrows with Regular Expressions Semi-declarative Language for Combinatorial Search Grammar Repair with Examples and Tree Automata
Aug 14, 2026	New post on Proofs and Intuitions: When the Hard Part Stops Being Hard, on how AI-assisted formal verification is reshaping programming-language research, letting individual researchers do in weeks what used to take months.
Aug 4, 2026	Our paper Certified Program Synthesis with a Multi-modal Verifier has been accepted to ASE 2026. See you in Munich in October!
Jul 28, 2026	Our paper Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean has received a Distinguished Paper Award at CAV 2026!

selected publications

Certified Program Synthesis with a Multi-Modal Verifier

Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey

ASE 2026. ACM.

PDF Artifact
Tracking Borrows with Regular Expressions

Todd Nowacki, Sam Blackshear, John Mitchell, Shaz Qadeer, and Ilya Sergey

Proc. ACM Program. Lang. 2026. (OOPSLA), ACM.

PDF Code Artifact Slides
Infinitary Relational Logic

Vladimir Gladshtein, Qiyuan Zhao, Yuxi Ling, Sean Wang, and Ilya Sergey

Proc. ACM Program. Lang. 2026. (OOPSLA), ACM.

PDF Code Artifact
Semi-declarative Language for Combinatorial Search

Ziyi Yang, and Ilya Sergey

Proc. ACM Program. Lang. 2026. (OOPSLA), ACM.

PDF Artifact
Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean

Vladimir Gladshtein, Vitaly Kurin, Yueyang Feng, Dipesh Kafle, George Pîrlea, Qiyuan Zhao, and Ilya Sergey

CAV 2026. Springer.

Distinguished Paper Award

PDF Code Artifact
Lazy Proof Automation for Separation Logic

Valentin Mikhalchuk, Vladimir Gladshtein, and Ilya Sergey

ITP 2026. LIPIcs, Schloss Dagstuhl.

PDF Code Artifact
Foundational Multi-Modal Program Verifiers

Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey

Proc. ACM Program. Lang. 2026. (POPL), ACM.

PDF Code Artifact
Veil: A Framework for Automated and Interactive Verification of Transition Systems

George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey

CAV 2025. Springer.

PDF Code Artifact
Accelerating Automated Program Verifiers by Automatic Proof Localization

Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Müller, Markus Püschel, and Ilya Sergey

CAV 2025. Springer.

PDF Artifact
Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis

Yuxi Ling, Gokul Rajiv, Kiran Gopinathan, and Ilya Sergey

USENIX Security Symposium 2025. USENIX Association.

PDF Artifact

lecture notes

Programs and Proofs: Mechanizing Mathematics with Dependent Types

Ilya Sergey

Lecture notes with exercises.

PDF Webpage GitHub

miscellanea

I am married to an artist Lilia Anisimova.

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.