news

news

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