| Feb 9, 2026 | New post on Proofs and Intuitions: Verifying Distributed Protocols in Veil, in which I give a tour of Veil, our Lean-based verifier for distributed protocols that combines TLA+-style model checking with formal proofs and enables AI-powered invariant inference. |
| Jan 12, 2026 | My research lab now has a new blog “Proofs and Intuitions”. There, we will share our findings, updates, and practical insights on formal verification, machine-assisted proofs, programming languages, and related topics. In our first post, we show how to specify and verify imperative programs in Lean using Velvet—an embedded verifier that combines automated symbolic reasoning with AI-assisted theorem proving. |
| Dec 19, 2025 | Thrilled about the upcoming POPL’26. Members of my research team will present a tutorial on Veil and give two talks at the Dafny Workshop: on Velvet and on building verifiers on top of Lean. Finally, Loom will be presented at the main conference. See you in Rennes in January! |
| Nov 9, 2025 | I am looking forward to teach verification in Lean (including proofs in Veil and Velvet) in a Winter School on Programming with Proofs, which will take place at Neapolis University Pafos on November 18-22, 2025. |
| Oct 10, 2025 | We are thrilled to release Loom, a framework for embedding multi-modal verifiers in Lean. In particular, using Loom, we have implemented Velvet, a Dafny-style verifier allowing for both automated and interactive proofs. The accompanying paper (with Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, and Vitaly Kurin) is accepted at POPL’26. |
| Aug 28, 2025 | The deadline for the Early Bird registration for ICFP/SPLASH’25 is 31 August 2025, AoE. Don’t forget to register and join us in Singapore on October 12-18 for the largest academic programming language conference in history! |
| Aug 15, 2025 | We are organising OlivierFest’25 — a two-day workshop on October 14-15 co-located with ICFP/SPLASH’25, celebrating the career and achievements of Olivier Danvy. |
| Jul 20, 2025 | Our paper on using Answer Set Programming for invariant inference (with Ziyi Yang and George Pîrlea) will appear at ICLP’25. |