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.

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.

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.

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.

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.

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

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.

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

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!

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

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

findaphd.com

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.

Grokipedia is alright.

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

The tunes of Rocq’n’Roll. #icfpsplash25

Ilya Sergey@ilyasergey.bsky.social · 10mo ago

FARM Performance is about to start! #icfpsplash25

FARM Performance is about to start! #icfpsplash25

Lots of folks in the OxCaml tutorial! #icfpsplash25

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

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.

Ningke Li@ningkeli.bsky.social · 10mo ago

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

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

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

Ilya Sergey@ilyasergey.bsky.social · 10mo ago

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

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

cs.ubc.ca

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

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

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

One week until ICFP/SPLASH’25! conf.researchr.org/home/icfp-sp...

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

conf.researchr.org

@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

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)

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

conf.researchr.org

Yaron Minsky@yminsky.bsky.social · 10mo ago

We're going to be at SPLASH/ICFP in Singapore, so if you're going, come talk to us! Richard Eisenberg is an especially good person to ask, but a lot of us will have useful context on this.

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.