Ilya Sergey
@ilyasergey.bsky.social
Associate Professor at National University of Singapore. I do research in programming languages, software verification, distributed systems, and program synthesis. ilyasergey.net
Implementing proof systems in Lean in 2026 be like
January 23, 2026 at 1:46 PM
Implementing proof systems in Lean in 2026 be like
Revisiting CS101.
November 26, 2025 at 5:11 AM
Revisiting CS101.
Had a fantastic week teaching Programming with Proofs in Lean at Neapolis University Pafos.
It was great to introduce NUP students to program verification with Veil and Velvet, having many insightful discussions along the way. Excited to see what projects they'll develop next!
It was great to introduce NUP students to program verification with Veil and Velvet, having many insightful discussions along the way. Excited to see what projects they'll develop next!
November 22, 2025 at 6:02 PM
Had a fantastic week teaching Programming with Proofs in Lean at Neapolis University Pafos.
It was great to introduce NUP students to program verification with Veil and Velvet, having many insightful discussions along the way. Excited to see what projects they'll develop next!
It was great to introduce NUP students to program verification with Veil and Velvet, having many insightful discussions along the way. Excited to see what projects they'll develop next!
Spent the last couple of days porting my program verification class from Dafny to Lean via Loom/Velvet, and it just works!
Whenever the SMT solver can’t fully prove a program correct, Lean’s aesop and grind take care of the remaining goals.
Whenever the SMT solver can’t fully prove a program correct, Lean’s aesop and grind take care of the remaining goals.
October 30, 2025 at 11:59 AM
Spent the last couple of days porting my program verification class from Dafny to Lean via Loom/Velvet, and it just works!
Whenever the SMT solver can’t fully prove a program correct, Lean’s aesop and grind take care of the remaining goals.
Whenever the SMT solver can’t fully prove a program correct, Lean’s aesop and grind take care of the remaining goals.
Grokipedia is alright.
October 28, 2025 at 11:10 AM
Grokipedia is alright.
The tunes of Rocq’n’Roll. #icfpsplash25
October 12, 2025 at 2:09 PM
The tunes of Rocq’n’Roll. #icfpsplash25
FARM Performance is about to start! #icfpsplash25
October 12, 2025 at 11:17 AM
FARM Performance is about to start! #icfpsplash25
I am thrilled to announce Velvet: a new foundational multi-modal verifier for imperative programs in Lean.
Velvet unifies execution, testing, automated and interactive proofs; and is itself proven sound.
💻 github.com/verse-lab/loom
📄 verse-lab.github.io/papers/loom-...
Velvet unifies execution, testing, automated and interactive proofs; and is itself proven sound.
💻 github.com/verse-lab/loom
📄 verse-lab.github.io/papers/loom-...
October 9, 2025 at 6:03 AM
I am thrilled to announce Velvet: a new foundational multi-modal verifier for imperative programs in Lean.
Velvet unifies execution, testing, automated and interactive proofs; and is itself proven sound.
💻 github.com/verse-lab/loom
📄 verse-lab.github.io/papers/loom-...
Velvet unifies execution, testing, automated and interactive proofs; and is itself proven sound.
💻 github.com/verse-lab/loom
📄 verse-lab.github.io/papers/loom-...
Just visited YST Conservatory of NUS, the venue for the upcoming FARM concert at ICFP/SPLASH'25. Excited about the upcoming performance combining art, music, and creative programming!
2025.splashcon.org/track/splash...
2025.splashcon.org/track/splash...
September 16, 2025 at 10:06 AM
Just visited YST Conservatory of NUS, the venue for the upcoming FARM concert at ICFP/SPLASH'25. Excited about the upcoming performance combining art, music, and creative programming!
2025.splashcon.org/track/splash...
2025.splashcon.org/track/splash...
Do it for science!
August 20, 2025 at 2:32 PM
Do it for science!
It was a pleasure to host @kcsrk.info who visited NUS earlier this week and talked about some cool systems verification projects done by his team.
August 6, 2025 at 11:44 AM
It was a pleasure to host @kcsrk.info who visited NUS earlier this week and talked about some cool systems verification projects done by his team.
It was a great pleasure to host Sebastian Ullrich from Lean FRO at NUS and learn about Lean 4 roadmap and its upcoming module system.
July 8, 2025 at 11:24 AM
It was a great pleasure to host Sebastian Ullrich from Lean FRO at NUS and learn about Lean 4 roadmap and its upcoming module system.
I really like my job.
June 23, 2025 at 11:37 AM
I really like my job.
In Seoul this week. Just got this delicious local treat from a street vendor.
June 16, 2025 at 1:24 PM
In Seoul this week. Just got this delicious local treat from a street vendor.
One of the cutest small traditions we have in my research lab is, when travelling, to put a flag of the current location into the Mattermost status.
June 11, 2025 at 1:55 PM
One of the cutest small traditions we have in my research lab is, when travelling, to put a flag of the current location into the Mattermost status.
One month till POPL deadline.
June 6, 2025 at 9:01 AM
One month till POPL deadline.
The fact that someone made a one hour video about the flight I take every couple of years and it has been watched 90k times is, probably, a sign that my life is a lot more interesting than I think.
(Also, feeling like a jaded survivor in my regular economy class.)
(Also, feeling like a jaded survivor in my regular economy class.)
June 4, 2025 at 10:11 AM
The fact that someone made a one hour video about the flight I take every couple of years and it has been watched 90k times is, probably, a sign that my life is a lot more interesting than I think.
(Also, feeling like a jaded survivor in my regular economy class.)
(Also, feeling like a jaded survivor in my regular economy class.)
When you are asking Cursor to help with a Lean proof, but it is pissed at you.
May 26, 2025 at 1:37 PM
When you are asking Cursor to help with a Lean proof, but it is pissed at you.
Jonathan Ragan-Kelley is visiting NUS today, sharing his exciting work on verified user-schedulable languages.
May 21, 2025 at 3:17 AM
Jonathan Ragan-Kelley is visiting NUS today, sharing his exciting work on verified user-schedulable languages.
I’ve had a ton of fun participating in the Working Group 2.8 meeting on Functional Programming last week. Those lambdas are in good hands.
May 20, 2025 at 2:44 AM
I’ve had a ton of fun participating in the Working Group 2.8 meeting on Functional Programming last week. Those lambdas are in good hands.
Looking forward to visiting MIT CSAIL for the next two days, catching up with the verification folks at PLV and PDOS groups.
May 8, 2025 at 1:57 PM
Looking forward to visiting MIT CSAIL for the next two days, catching up with the verification folks at PLV and PDOS groups.
This is something we've been working on for a while, and now are thrilled to share.
Veil: the first foundational framework that combines SMT-based and interactive proofs about distributed protocols, seamlessly, in Lean!
Tool: github.com/verse-lab/veil
Paper: verse-lab.github.io/papers/veil-...
Veil: the first foundational framework that combines SMT-based and interactive proofs about distributed protocols, seamlessly, in Lean!
Tool: github.com/verse-lab/veil
Paper: verse-lab.github.io/papers/veil-...
April 14, 2025 at 8:52 AM
This is something we've been working on for a while, and now are thrilled to share.
Veil: the first foundational framework that combines SMT-based and interactive proofs about distributed protocols, seamlessly, in Lean!
Tool: github.com/verse-lab/veil
Paper: verse-lab.github.io/papers/veil-...
Veil: the first foundational framework that combines SMT-based and interactive proofs about distributed protocols, seamlessly, in Lean!
Tool: github.com/verse-lab/veil
Paper: verse-lab.github.io/papers/veil-...
I feel that if I published the main paper of my PhD now, it would be received with much more enthusiasm than it has been back in 2012:
March 31, 2025 at 12:24 PM
I feel that if I published the main paper of my PhD now, it would be received with much more enthusiasm than it has been back in 2012: