Thank you, Rachit!
09.02.2026 14:43 — 👍 0 🔁 0 💬 0 📌 0Thank you, Rachit!
09.02.2026 14:43 — 👍 0 🔁 0 💬 0 📌 0
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
23.01.2026 13:46 — 👍 1 🔁 0 💬 0 📌 0
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.
Weird. Let me check with the SIGPLAN AV Team.
05.12.2025 12:22 — 👍 2 🔁 0 💬 0 📌 0
Revisiting CS101.
26.11.2025 05:11 — 👍 1 🔁 0 💬 0 📌 0
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...
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.
28.10.2025 11:10 — 👍 2 🔁 0 💬 0 📌 0
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...
18.10.2025 03:11 — 👍 6 🔁 2 💬 0 📌 1Safe travels!
18.10.2025 02:07 — 👍 2 🔁 0 💬 0 📌 0The tunes of Rocq’n’Roll. #icfpsplash25
12.10.2025 14:09 — 👍 2 🔁 0 💬 0 📌 0
FARM Performance is about to start! #icfpsplash25
12.10.2025 11:17 — 👍 1 🔁 0 💬 0 📌 1
Lots of folks in the OxCaml tutorial! #icfpsplash25
12.10.2025 08:19 — 👍 4 🔁 1 💬 0 📌 0
@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.
12.10.2025 07:32 — 👍 6 🔁 2 💬 0 📌 0
1st coffee break of the week
many many more to come
#icfpsplash25
ICFP/SPLASH is starting now!! See you all at NUS today — #icfpsplash25
12.10.2025 01:01 — 👍 4 🔁 1 💬 0 📌 0
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...
10.10.2025 18:37 — 👍 7 🔁 1 💬 0 📌 0
A beautiful day to stop in at the Singapore Botanic Gardens and the National Orchid Garden before ICFP/SPLASH! #icfpsplash25
11.10.2025 02:57 — 👍 3 🔁 2 💬 0 📌 0
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...
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-...
I might drop by.
07.10.2025 11:46 — 👍 1 🔁 0 💬 1 📌 0
One week until ICFP/SPLASH’25!
conf.researchr.org/home/icfp-sp...
@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...
02.10.2025 09:00 — 👍 1 🔁 1 💬 1 📌 0And 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)
03.10.2025 14:32 — 👍 10 🔁 3 💬 0 📌 0And your point is?
28.09.2025 12:42 — 👍 0 🔁 0 💬 0 📌 0An 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.
25.09.2025 18:24 — 👍 1 🔁 0 💬 0 📌 0