Speaker: Nik Swamy — Partner Researcher, RiSE group, Microsoft Research, Redmond

Date: Tuesday, April 7, 2026, 11:00 AM – 12:00 PM IST

Venue: SSB 334, Department of CSE, IIT Madras

Abstract

Can AI assist in building programs with formal proofs of correctness? My recent experience using Copilot CLI to develop programs with proofs in F* and Pulse has been eye opening. In just the past few weeks, working with agents, I have programmed nearly 200 KLOC of verified code and proofs in a variety of contexts, ranging from concurrent data structures, formalizations of classic algorithms textbooks, porting a verified garbage collector from FP Launchpad, and even some proofs of production C code at Microsoft.

I will speak about my experience and offer some tools and techniques for others to try out similar AI-assisted proof-oriented programming tasks using a fresh consolidated release of F* and related tools, coupled with proof-copilot, agentic tools for proof-oriented programming.

While AI-assistance offers many new opportunities for program proof, I will also offer some thoughts about the many challenges it poses.

Bio

Nik Swamy is a Partner Researcher in the RiSE group at MSR Redmond. His work covers various topics including type systems, functional programming, program proof, and theorem proving. He often thinks about how to use these techniques to build provably correct and secure programs, often in the context of systems software. Most of his work builds on F*, a proof-oriented programming language for higher order, effectful programs.