Abstract: Correct system software with formally checked or verified properties has long been considered too costly to own in practice, especially for rapidly evolving cloud and AI stacks. For decades, the correctness of system code has relied primarily on human-centric quality assurance, but the practice of AI-based vibe coding is eroding the efficacy of traditional practices. Stronger correctness guarantees seem to be more important than ever. In this talk, I will discuss our experience of formally checking and verifying cloud systems, motivated by a vision of building truly reliable cloud infrastructures. Specifically, I will present our efforts on model checking and formal verification of distributed systems such as Kubernetes and ZooKeeper, with a focus on recent efforts to scale some of these techniques. I will argue that formally checked and verified system software may no longer be out of reach or prohibitively expensive, with the help of AI. At the same time, achieving correctness requires much more than placing formal methods inside an agentic loop. Scaling formal verification demands system insights alongside AI assistance.
Bio: Tianyin Xu is an Associate Professor of Computer Science in the Siebel School of Computing and Data Science at the University of Illinois Urbana-Champaign (UIUC). His research focuses on building reliable and secure computer systems that empower next-generation computing. He has been in the UIUC List of Teachers Ranked as Excellent for nine times since he joined the CS department in 2018. He is the recipient of two OSDI Jay Lepreau Best Paper Awards, two ASPLOS Best Paper Awards, a SIGCOMM Best Student Paper Award, two SIGSOFT Distinguished Paper Awards, a EuroSys Gilles Muller Best Artifact Award, and a CACM Research Highlight. He is a recipient of a C.W. Gear Outstanding Junior Faculty Award, a Dean's Award for Excellence in Research, NSF CAREER Award, an Intel Rising Star Faculty Award, and a Facebook Distributed Systems Research award. He is an editor of the SIGOPS Blog and is an area chair of the JSys. More details: https://tianyin.github.io.