CS Colloquium: Nikhil Swamy on The ART of Agentic Proof-Oriented Programming: Audits, Rubrics, and Templates

Name: CS Colloquium: Nikhil Swamy on The ART of Agentic Proof-Oriented Programming: Audits, Rubrics, and Templates
Start: 2026-10-29T15:30:00-06:00
End: 2026-10-29T16:30:00-06:00
Location: ECCR 265

Data, AI & ML 29.10.2026 / donderdag / 15:30 - 16:30 ECCR 265 Organisator: Computer Science Hybride evenement Tickets kopen

Please join us in ECCR 265 or on Zoom!

Abstract: AI-based program synthesis is now widespread. While AI agents churn out large amounts of code from informal natural language descriptions, comprehending this code and assessing its correctness is a major challenge.

Having agents code in proof-oriented languages can help, using theorem proving tools to check that the code conforms to a specification, and allowing humans to focus on assessing formal specifications against their informal intent. However, when confronted with reviewing messy agent-generated specifications, one may be no better off than trying to understand the code itself.

This talk draws on my team's experience this year using agents to program & prove in F*, a proof-oriented language developed at Microsoft Research. In just a few months, with agents, we have built several verified libraries and systems, ranging from formalizations of algorithms textbooks, to garbage collectors, cryptographic libraries, a variety of Internet standard networking protocols, and even C code from the Linux kernel, in total exceeding a million lines of code and proof.

I attempt to articulate a few principles that have emerged from this experience. Drawing on classic ideas from programming language design and proof engineering, these principles aim to structure the interaction between humans and agents, simplifying the process of reviewing agent-authored specifications and claims of correctness. Many open questions remain.

You can learn more about this work at the RiSE blog and from this manuscript.

Bio: Nik is a researcher in the RiSE group at Microsoft Research in Redmond. His work covers various topics including type systems, functional programming, program proofs, and theorem proving, and these days the intersection of these topics with AI. He is one of the authors of the F* proof-oriented programming language, which is used to build provably correct & secure code, including cryptographic software and OS components, some of which may well be running on your device. His work has received several awards, including a Most Influential Paper award from POPL 2016. He has a PhD from the University of Maryland from 2008.