news

news

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