iiinova — where your digital self keeps evolving

Ilya Sergey @ilyasergey.bsky.social · 24/09/2026

A two-weekend fun project from 2 months ago: Vermilion, an experimental Lean 4 backend for 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 favorite AI system. github.com/ilyasergey/v...

050

Ilya Sergey @ilyasergey.bsky.social · 06/09/2026

New to the LangLib: JavaGen, a language of nothing but Java interfaces and one subtype query, which is just enough to compute anything by a clever co/contra-variance interplay. Bonus: a Lean proof that Java generics are Turing-complete (Grigore, POPL'17). github.com/ilyasergey/l...

021

Ilya Sergey @ilyasergey.bsky.social · 31/08/2026

As a Programming Language nerd, I have a soft spot for esoteric languages (esolangs), which are built by enthusiasts for fun and to make a point. Over the weekend I started collecting them in Lean, so, please, meet Fantastic Beasts and Where to Find Them, PL edition: github.com/ilyasergey/l... →

$Four dark panels showing the same program in four languages: a Piet painting of coloured pixels, Whitespace rendered as labelled space/tab/linefeed blocks, a FRACTRAN list of 58 fractions, and two lines of Malbolge line noise. A badge in the top-right corner reads "answer := 42".$

162

Ilya Sergey @ilyasergey.bsky.social · 14/08/2026

A new post: "When the Hard Part Stops Being Hard". The gist: the effort that used to be required for a publishable PL result can now be fully automated with AI, and the field's research culture is already changing because of it. proofsandintuitions.net

proofsandintuitions.net

Proofs and Intuitions

A blog about mathematics, computing, formal verification, and the ideas behind them

3295

Ilya Sergey @ilyasergey.bsky.social · 25/06/2026

New blog post on Proofs and Intuitions: "Liveness Proofs in Veil, Part I: The First Step" (by Qiyuan Zhao). proofsandintuitions.net/2026/06/24/l... Safety says nothing bad happens; liveness says something good eventually does. We present a proof mode for verifying liveness deductively in Lean.

proofsandintuitions.net

Liveness Proofs in Veil, Part I: The First Step

Safety property means “nothing bad happens during the run of a program”; liveness property means “the program eventually does something good”. In this post, we walk through a simple proof of a livenes...

020

Ilya Sergey @ilyasergey.bsky.social · 19/05/2026

New blog post: On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications. proofsandintuitions.net/2026/05/18/p... The gist: randomised testing can validate formal specs. It's very cheap and powerful: we found bugs in specs of VERINA and CLEVER benchmarks.

proofsandintuitions.net

On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications

In this post, we show that property-based testing (PBT) is surprisingly effective for validating LLM-synthesised specifications of Lean programs: it is a cheap alternative to symbolic proofs, which he...

1114

Reposted by Ilya Sergey

Lean Focused Research Organization @lean-lang.org · 01/04/2026

1/3 New Lean use case: Veil, a multi-modal verification framework for distributed protocols from George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey at NUS.

2114

Ilya Sergey @ilyasergey.bsky.social · 27/03/2026

Are paper rejections really that bad? My papers get read by ~3 people on average. Each rejection means a resubmission, which means 3 more readers. After 4 rejections, that's double-digit readership.

1131

Ilya Sergey @ilyasergey.bsky.social · 18/03/2026

New on "Proofs and Intuitions": Verifying Move Borrow Checker in Lean: an Experiment in AI-Assisted PL Metatheory. proofsandintuitions.net/2026/03/18/m... The gist: I formalised Move's type system in Lean: 39KLOC, under a month, with Claude. Person-years in PL research just became person-weeks.

proofsandintuitions.net

Verifying Move Borrow Checker in Lean: an Experiment in AI-Assisted PL Metatheory

I formalised and proved the correctness of Move’s new borrow checker in Lean: 39,000 lines of mechanised metatheory, produced in under a month with the help of an AI coding assistant. This post tells ...

060

Ilya Sergey @ilyasergey.bsky.social · 09/02/2026

New post on "Proofs and Intuitions": Verifying Distributed Protocols in Veil. We take a tour of Veil, a Lean-based verification framework that combines TLA+-style model checking with formal proofs and enables AI-powered invariant inference. proofsandintuitions.net/2026/02/09/d...

proofsandintuitions.net

Verifying Distributed Protocols in Veil

In this post, we discuss how to formalise, test, and prove the correctness of a classic distributed protocol by combining model checking, automated deductive verification, and AI-powered invariant inf...

181

Ilya Sergey @ilyasergey.bsky.social · 23/01/2026

Implementing proof systems in Lean in 2026 be like

010

Ilya Sergey @ilyasergey.bsky.social · 21/01/2026

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

Proofs and Intuitions

A blog about mathematics, computing, formal verification, and the ideas behind them

1161

Ilya Sergey @ilyasergey.bsky.social · 05/01/2026

Claude Code and Aristotle are my two new favourite backend solvers for auto-active program verification in Lean. AI is the new SMT.

160

Ilya Sergey @ilyasergey.bsky.social · 22/11/2025

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!

060

Reposted by Ilya Sergey

Dominik Winterer @dominikwinterer.bsky.social · 05/11/2025

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...

findaphd.com

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

043

Ilya Sergey @ilyasergey.bsky.social · 30/10/2025

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.

180

Reposted by Ilya Sergey

Manuel Rigger @mrigger.bsky.social · 18/10/2025

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...

2025.splashcon.org

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...

062

Reposted by Ilya Sergey

ICFP Conference @icfp-conference.bsky.social · 12/10/2025

Lots of folks in the OxCaml tutorial! #icfpsplash25

041

Reposted by Ilya Sergey

Ningke Li @ningkeli.bsky.social · 12/10/2025

@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🥳

162

Reposted by Ilya Sergey

Manuel Rigger @mrigger.bsky.social · 12/10/2025

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.

062

Reposted by Ilya Sergey

ICFP Conference @icfp-conference.bsky.social · 12/10/2025

1st coffee break of the week many many more to come #icfpsplash25

071

Reposted by Ilya Sergey

ICFP Conference @icfp-conference.bsky.social · 12/10/2025

ICFP/SPLASH is starting now!! See you all at NUS today — #icfpsplash25

041

Reposted by Ilya Sergey

Caroline Lemieux @cestlemieux.bsky.social · 10/10/2025

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...

cs.ubc.ca

UBC Computer Science makes waves at programming language conference ICFP/SPLASH

071

Reposted by Ilya Sergey

ICFP Conference @icfp-conference.bsky.social · 11/10/2025

A beautiful day to stop in at the Singapore Botanic Gardens and the National Orchid Garden before ICFP/SPLASH! #icfpsplash25

032

Ilya Sergey @ilyasergey.bsky.social · 10/10/2025

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...

conf.researchr.org

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....

0103

Ilya Sergey @ilyasergey.bsky.social · 09/10/2025

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-...

0144

Reposted by Ilya Sergey

Anil Madhavapeddy @anil.recoil.org · 03/10/2025

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)

conf.researchr.org

ICFP/SPLASH 2025 - Tutorials - ICFP/SPLASH 2025

Latest Announcements Information for presenters at NUS (Sunday) and at MBS (Monday-Saturday) is now available! The registration is now open. Early Registration deadline: 31 August 2025. Activities ...

0103

Ilya Sergey @ilyasergey.bsky.social · 25/09/2025

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.

010

Reposted by Ilya Sergey

Vitaly Bragilevsky @bravit.bsky.social · 25/09/2025

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.

175

Reposted by Ilya Sergey

ICFP Conference @icfp-conference.bsky.social · 22/09/2025

T minus 3 weeks!! I wonder how many ICFP 2025 papers I can read on the plane ride over?

031

Reposted by Ilya Sergey

ICFP Programming Contest 2026 @icfpcontest.bsky.social · 17/09/2025

Now that the competition is over, Adso has penned his reflections. icfpcontest2025.github.io/afterword.pdf We also have many team write-ups here: icfpcontest2025.github.io/writeups.html Please let us know if you have some to add to the list!

icfpcontest2025.github.io

021

Ilya Sergey @ilyasergey.bsky.social · 16/09/2025

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...

050

Ilya Sergey @ilyasergey.bsky.social · 14/09/2025

OlivierFest’25 is taking place on October 14-15 at ICFP/SPLASH'25 in Singapore! A two-day celebration of Olivier Danvy's impact on PL research, with a program packed with talks on algebraic effects, semantics, interpreters, and, of course, continuations. conf.researchr.org/home/icfp-sp...

conf.researchr.org

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 h...

2102

Reposted by Ilya Sergey

Derek Dreyer @herrdreyer.bsky.social · 04/08/2025

It's official: RTFM, the faculty mentoring workshop, is happening again, this time at POPL 2026 in Rennes. The one we had at PLDI 2024 in Copenhagen was well received, so I'm looking forward to the next edition. Stay tuned!

0143

Reposted by Ilya Sergey

Patrick Vallely @pjvphotography.bsky.social · 28/08/2025

"Pat, why do you carry that ridiculous 600mm lens on long hikes?" Buddy, I can see mountains reflected in the eyes of a trailside pika.

Tighter crop of the same pika, focusing on its head.

An even tighter crop, focusing more on the pika's eye.

An extremely tight crop of the pika's eye, emphasizing their reflection of an early morning mountain scene.

6404367310933

Reposted by Ilya Sergey

Manuel Rigger @mrigger.bsky.social · 25/08/2025

I will be organizing two nature walks for ICFP/SPLASH (‪@icfp-conference.bsky.social‬)! I did one of them this weekend and was very lucky to see 11 saltwater crocodiles (including a tiny baby one), countless monitor lizards, otters, macaques, fruit bats, various kinds of birds, and fish.

171

Reposted by Ilya Sergey

ICFP Conference @icfp-conference.bsky.social · 25/08/2025

ICFP/SPLASH goers -- looking to escape into the wild for a moment? Come join one of these two planned hikes (courtesy of @mrigger.bsky.social)! First through the central reserve, and second through the wetlands: 2025.splashcon.org/attending/ou...

2025.splashcon.org

Outdoor Activities - SPLASH 2025

Announcements The registration is now open. Early Registration deadline: 31 August 2025. Read the travel information page for information about visas, accommodation, and travel tips. Check out our Ex...

102

Reposted by Ilya Sergey

Stefan Marr @stefan-marr.de · 24/08/2025

Already registered for SPLASH or @icfp-conference.bsky.social? If not, check out our list of accepted papers: conf.researchr.org/home/icfp-sp... It's language implementation techniques, from debugging and JIT compiling on microcontrollers to visualizing execution patterns between CPU and GPU!

conf.researchr.org

MPLR 2025 - ICFP/SPLASH 2025

The 22nd International Conference on Managed Programming Languages and Runtimes (MPLR 2025, formerly ManLang, originally PPPJ) is a premier forum for presenting and discussing novel results in all asp...

065

Ilya Sergey @ilyasergey.bsky.social · 06/08/2025

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.

060

Reposted by Ilya Sergey

ICFP Conference @icfp-conference.bsky.social · 31/07/2025

ICFP/SPLASH 2025 registration is open! If you register soon, you can catch the early registration discount (by August 31). Register for the whole 7 days and only pay for 6! conf.researchr.org/attending/ic...

conf.researchr.org

Registration - ICFP/SPLASH 2025

The registration is now open. Early Registration deadline: 31 August 2025. Welcome to the website of the joint ICFP/SPLASH 2025 conference! For the first time, the two leading SIGPLAN venues—ICFP and ...

035

Ilya Sergey @ilyasergey.bsky.social · 24/07/2025

Moshe Vardi is Simon Peyton Jones of CAV.

030