| 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. |
| May 26, 2025 | Our work on accelerating SMT-based program verifiers (with Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Müller, and Markus Püschel) will appear at CAV’25. |
| Apr 14, 2025 | We are excited to release Veil, a new framework for verifying distributed protocols, automatically and interactively, in Lean! The accompanying paper (with George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, and Qiyuan Zhao) will appear at CAV’25. |
| Feb 21, 2025 | Our paper on synthesising Separation Logic predicates using Answer Set Programming (with Ziyi Yang) is accepted at OOPSLA’25. |