| May 26, 2026 | Honoured to receive an Amazon Research Award for the project “Linear Types for a Foundational Multi-Modal Program Verifier”! |
| May 25, 2026 | Our paper on Lazy Proof Automation for Separation Logic will appear at ITP 2026! |
| May 18, 2026 | New post on Proofs and Intuitions: On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications, on how property-based testing surprisingly outperforms symbolic methods at detecting issues in LLM-synthesised Lean specifications. |
| 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. |