news

news

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!
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.