Associate Professor at @NUSComputing. Working on programming languages, distributed systems, and proof engineering – all of that in Lean.
Singapore
- Tweets 4,165
- Following 993
- Followers 8,208
- Likes 6,747
A two-weekend fun project: 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/vermil…
6
20
169
7,428
Velvet 2.0 is out: now based on Lean's most recent verification machinery, easier to set up, and 10x faster. New: exception specs, ghost state, named proof goals, lots of case studies from Dijkstra to lazy segment trees. And a new shiny webpage:
velvet-verifier.dev/
3
23
129
7,287
Turns out, it's bad to have a domain with "verifier" in its name, so here we go:
velvetprover.dev/
270
And since, it's apparently, not great to have "verifier" in a domain name, here's an alternative one:
velvetprover.dev/
Velvet 2.0 is out: now based on Lean's most recent verification machinery, easier to set up, and 10x faster. New: exception specs, ghost state, named proof goals, lots of case studies from Dijkstra to lazy segment trees. And a new shiny webpage:
velvet-verifier.dev/
2
12
1,562
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 (@rgrig, POPL'17).
github.com/ilyasergey/langli…
3
33
1,651
As a Programming Language nerd, I have a soft spot for esoteric languages (esolangs), which are built 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/langli… →
6
25
181
12,188
All the listings above come from one source program in Turpentine (a nod to Alan Perlis), a small imperative language, with compilers to twelve of the esolangs. Ten of those are certified: they are derived from the completeness proofs, thus, correct by construction (but useless).
1
3
315
There is more in the collection: Befunge-93, Thue, Ook, Unlambda, SKI, Brainloller, Deadfish, and more on a roadmap. Each has a spec, an interpreter, tests, and a computational-class theorem; most have compilers from Turpentine.
Contributions welcome: github.com/ilyasergey/langli…
6
294
Conjecture: any formal artifact you can name will be vibe-formalized in Lean by some enthusiast by the end of 2026.
9
2
72
13,665
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 full automated with AI, and the field's research culture is already changing because of it.
proofsandintuitions.net/2026…
13
13
106
8,633