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
My research lab is launching a new blog, where we will share thoughts and tutorials on formal methods, mechanised proofs, PL, and more.
proofsandintuitions.net
First post: verifying imperative programs in Lean 4 with Velvet, using symbolic automation and AI-assisted proving.
proofsandintuitions.net
First post: verifying imperative programs in Lean 4 with Velvet, using symbolic automation and AI-assisted proving.
Proofs and Intuitions
A blog about mathematics, computing, formal verification, and the ideas behind them
proofsandintuitions.net
January 21, 2026 at 3:03 PM
My research lab is launching a new blog, where we will share thoughts and tutorials on formal methods, mechanised proofs, PL, and more.
proofsandintuitions.net
First post: verifying imperative programs in Lean 4 with Velvet, using symbolic automation and AI-assisted proving.
proofsandintuitions.net
First post: verifying imperative programs in Lean 4 with Velvet, using symbolic automation and AI-assisted proving.
Claude Code and Aristotle are my two new favourite backend solvers for auto-active program verification in Lean.
AI is the new SMT.
AI is the new SMT.
January 5, 2026 at 8:01 AM
Claude Code and Aristotle are my two new favourite backend solvers for auto-active program verification in Lean.
AI is the new SMT.
AI is the new SMT.
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!
Reposted by Ilya Sergey
We are hiring!
Suzanne Embury and I are looking for a talented Ph.D. student 👩🎓👨🎓 to join an exciting, high-impact project on automated testing and bug fixing of Formal Methods tools.
www.findaphd.com/phds/project...
Suzanne Embury and I are looking for a talented Ph.D. student 👩🎓👨🎓 to join an exciting, high-impact project on automated testing and bug fixing of Formal Methods tools.
www.findaphd.com/phds/project...
FM-Fuzz: Continuous Fuzzing and AI-based Bug Fixing for Formal Methods at The University of Manchester on FindAPhD.com
PhD Project - FM-Fuzz: Continuous Fuzzing and AI-based Bug Fixing for Formal Methods at The University of Manchester, listed on FindAPhD.com
www.findaphd.com
November 5, 2025 at 10:25 PM
We are hiring!
Suzanne Embury and I are looking for a talented Ph.D. student 👩🎓👨🎓 to join an exciting, high-impact project on automated testing and bug fixing of Formal Methods tools.
www.findaphd.com/phds/project...
Suzanne Embury and I are looking for a talented Ph.D. student 👩🎓👨🎓 to join an exciting, high-impact project on automated testing and bug fixing of Formal Methods tools.
www.findaphd.com/phds/project...
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.
Reposted by Ilya Sergey
A reminder that we will have another @icfp-conference.bsky.social/SPLASH nature walk planned for tomorrow. Consider joining if you are (still) in Singapore! 2025.splashcon.org/attending/ou...
Outdoor Activities - SPLASH 2025
Latest Announcements
Information for presenters at NUS (Sunday) and at MBS (Monday-Saturday) is now available!
Official tag for social media posting about the conference is #icfpsplash25
If you’re pl...
2025.splashcon.org
October 18, 2025 at 3:11 AM
A reminder that we will have another @icfp-conference.bsky.social/SPLASH nature walk planned for tomorrow. Consider joining if you are (still) in Singapore! 2025.splashcon.org/attending/ou...
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
Reposted by Ilya Sergey
Lots of folks in the OxCaml tutorial! #icfpsplash25
October 12, 2025 at 8:19 AM
Lots of folks in the OxCaml tutorial! #icfpsplash25
Reposted by Ilya Sergey
@icfp-conference.bsky.social
Had a nice day co-hosting the first hike of #icfpsplash25 Outdoor Activities track with Yibo🙌
Walking in the forest 🌳
Seeking special animals (monkeys🐒, lizards🦎, colugos🦇, and even a snake🐍!)
Enjoying the networking🥳
Had a nice day co-hosting the first hike of #icfpsplash25 Outdoor Activities track with Yibo🙌
Walking in the forest 🌳
Seeking special animals (monkeys🐒, lizards🦎, colugos🦇, and even a snake🐍!)
Enjoying the networking🥳
October 12, 2025 at 6:57 AM
@icfp-conference.bsky.social
Had a nice day co-hosting the first hike of #icfpsplash25 Outdoor Activities track with Yibo🙌
Walking in the forest 🌳
Seeking special animals (monkeys🐒, lizards🦎, colugos🦇, and even a snake🐍!)
Enjoying the networking🥳
Had a nice day co-hosting the first hike of #icfpsplash25 Outdoor Activities track with Yibo🙌
Walking in the forest 🌳
Seeking special animals (monkeys🐒, lizards🦎, colugos🦇, and even a snake🐍!)
Enjoying the networking🥳
Reposted by Ilya Sergey
It seems the first hike as part of @icfp-conference.bsky.social/SPLASH went well! A shoutout to @ningkeli.bsky.social and Yibo DONG (as well as my wife, Ting), who guided the participants on this walk. I could unfortunately not participate, as I had to travel abroad due to an urgent issue.
@icfp-conference.bsky.social
Had a nice day co-hosting the first hike of #icfpsplash25 Outdoor Activities track with Yibo🙌
Walking in the forest 🌳
Seeking special animals (monkeys🐒, lizards🦎, colugos🦇, and even a snake🐍!)
Enjoying the networking🥳
Had a nice day co-hosting the first hike of #icfpsplash25 Outdoor Activities track with Yibo🙌
Walking in the forest 🌳
Seeking special animals (monkeys🐒, lizards🦎, colugos🦇, and even a snake🐍!)
Enjoying the networking🥳
October 12, 2025 at 7:32 AM
It seems the first hike as part of @icfp-conference.bsky.social/SPLASH went well! A shoutout to @ningkeli.bsky.social and Yibo DONG (as well as my wife, Ting), who guided the participants on this walk. I could unfortunately not participate, as I had to travel abroad due to an urgent issue.
Reposted by Ilya Sergey
October 12, 2025 at 2:27 AM
Reposted by Ilya Sergey
ICFP/SPLASH is starting now!! See you all at NUS today — #icfpsplash25
ICFP/SPLASH'25 is starting tomorrow!
Attending Sunday workshops and FARM Performance at #icfpsplash25? Make sure check out our illustrated guide on getting to NUS Conservatory and dining options on campus:
conf.researchr.org/venue/icfp-s...
Attending Sunday workshops and FARM Performance at #icfpsplash25? Make sure check out our illustrated guide on getting to NUS Conservatory and dining options on campus:
conf.researchr.org/venue/icfp-s...
Venue NUS School of Computing - ICFP/SPLASH 2025
Latest Announcements
If you’re planning to attend FARM Performance and have a dinner on NUS campus, please, check this illustrated guide with directions to YST Conservatory and NUS UTown food courts....
conf.researchr.org
October 12, 2025 at 1:01 AM
ICFP/SPLASH is starting now!! See you all at NUS today — #icfpsplash25
Reposted by Ilya Sergey
The UBC Software Practices Lab is heading to #icfpsplash25! 4 ICFP/OOPSLA talks, 1 SPLASH-E, 5 talks at associated workshops... check it out: www.cs.ubc.ca/news/2025/10...
UBC Computer Science makes waves at programming language conference ICFP/SPLASH
www.cs.ubc.ca
October 10, 2025 at 6:37 PM
The UBC Software Practices Lab is heading to #icfpsplash25! 4 ICFP/OOPSLA talks, 1 SPLASH-E, 5 talks at associated workshops... check it out: www.cs.ubc.ca/news/2025/10...
Reposted by Ilya Sergey
A beautiful day to stop in at the Singapore Botanic Gardens and the National Orchid Garden before ICFP/SPLASH! #icfpsplash25
October 11, 2025 at 2:57 AM
A beautiful day to stop in at the Singapore Botanic Gardens and the National Orchid Garden before ICFP/SPLASH! #icfpsplash25
ICFP/SPLASH'25 is starting tomorrow!
Attending Sunday workshops and FARM Performance at #icfpsplash25? Make sure check out our illustrated guide on getting to NUS Conservatory and dining options on campus:
conf.researchr.org/venue/icfp-s...
Attending Sunday workshops and FARM Performance at #icfpsplash25? Make sure check out our illustrated guide on getting to NUS Conservatory and dining options on campus:
conf.researchr.org/venue/icfp-s...
Venue NUS School of Computing - ICFP/SPLASH 2025
Latest Announcements
If you’re planning to attend FARM Performance and have a dinner on NUS campus, please, check this illustrated guide with directions to YST Conservatory and NUS UTown food courts....
conf.researchr.org
October 10, 2025 at 5:23 PM
ICFP/SPLASH'25 is starting tomorrow!
Attending Sunday workshops and FARM Performance at #icfpsplash25? Make sure check out our illustrated guide on getting to NUS Conservatory and dining options on campus:
conf.researchr.org/venue/icfp-s...
Attending Sunday workshops and FARM Performance at #icfpsplash25? Make sure check out our illustrated guide on getting to NUS Conservatory and dining options on campus:
conf.researchr.org/venue/icfp-s...
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-...
Reposted by Ilya Sergey
@mathieu.social will be presenting a functional pearl "Invertible Syntax without the Tuples", joint work with Arnaud Spiwack, at Olivier Danvy's Festschrift on the Tuesday 14th. conf.researchr.org/details/icfp...
Invertible Syntax without the Tuples (Functional Pearl) (OlivierFest 2025) - ICFP/SPLASH 2025
This two-day event celebrates the career and accomplishments of Olivier Danvy on the occasion of his 64th birthday. Olivier is a visionary in the field of programming languages and is well-known for…
conf.researchr.org
October 2, 2025 at 9:00 AM
@mathieu.social will be presenting a functional pearl "Invertible Syntax without the Tuples", joint work with Arnaud Spiwack, at Olivier Danvy's Festschrift on the Tuesday 14th. conf.researchr.org/details/icfp...
Reposted by Ilya Sergey
And if you’re interested in OxCaml, we have a tutorial on Sunday at ICFP walking through it conf.researchr.org/track/icfp-s... (materials will be online for anyone afterwards. Just the minor detail of finishing writing them first)
October 3, 2025 at 2:32 PM
And if you’re interested in OxCaml, we have a tutorial on Sunday at ICFP walking through it conf.researchr.org/track/icfp-s... (materials will be online for anyone afterwards. Just the minor detail of finishing writing them first)
An opening theme from the Outlaw Star series has just randomly started playing in my head, and now I am fighting the urge to rewatch it.
September 25, 2025 at 6:24 PM
An opening theme from the Outlaw Star series has just randomly started playing in my head, and now I am fighting the urge to rewatch it.
Reposted by Ilya Sergey
I’m looking for an intern to work on Rust/RustRover content creation. If you are a university student in any EU country, the UK, Serbia, or Armenia, and you are passionate about Rust and sharing your knowledge, I’d love to hear from you. Please repost to help spread the word. Links below.
September 25, 2025 at 8:32 AM
I’m looking for an intern to work on Rust/RustRover content creation. If you are a university student in any EU country, the UK, Serbia, or Armenia, and you are passionate about Rust and sharing your knowledge, I’d love to hear from you. Please repost to help spread the word. Links below.