| Apr 30, 2026 | Our paper Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean has been accepted to CAV 2026! |
| Apr 13, 2026 | I have given a talk on my experiments in AI-Assisted Metatheory at the FP Launchpad Kickoff at IIT Madras. |
| Apr 2, 2026 | Veil has been featured as one of the verification use cases on the official Lean website! |
| Mar 31, 2026 | Excited to announce that our Dagstuhl Seminar The Next 20 Years of Computer-Assisted Theorem Proving has been accepted! I will be co-organising it with Sandrine Blazy, Jonathan Protzenko, and Sebastian Ullrich. The seminar will take place on February 21–26, 2027. |
| Mar 18, 2026 | New post on Proofs and Intuitions: Verifying Move Borrow Checker in Lean: an Experiment in AI-Assisted PL Metatheory, in which I describe how I mechanised Move’s borrow checker in Lean with AI assistance, producing 39,000 lines of metatheory in about one month. |
| 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! |