| Sep 28, 2026 | A two-weekend fun project: Vermilion, an experimental Lean 4 backend for the 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 favourite AI system. |
| Sep 18, 2026 | We have released a new version of Velvet, our foundational multi-modal verifier for imperative programs in Lean, with a number of new features. It now has a new web site! |
| Aug 15, 2026 | Four papers from VERSE lab will appear at OOPSLA 2026: |
| Aug 14, 2026 | New post on Proofs and Intuitions: When the Hard Part Stops Being Hard, on how AI-assisted formal verification is reshaping programming-language research, letting individual researchers do in weeks what used to take months. |
| Aug 4, 2026 | Our paper Certified Program Synthesis with a Multi-modal Verifier has been accepted to ASE 2026. See you in Munich in October! |
| Jul 28, 2026 | Our paper Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean has received a Distinguished Paper Award at CAV 2026! |
| Jul 10, 2026 | I taught verification in Lean (using Velvet and Veil) at the Summer School: LeanLang for Programming, hosted by Emergence Research Lab and IISc in Bengaluru, July 6-10, 2026. |
| May 26, 2026 | Honoured to receive an Amazon Research Award for the project “Linear Types for a Foundational Multi-Modal Program Verifier”! |