LLMs’ capability of quickly generating a large amount of code has been widely recognized, with more than 80% of software developers regularly using coding agents. However, LLMs’ capability of generating semantically correct code remains a concern. In the past three years, many of us at Microsoft Research have explored teaching and using LLMs to write formal specifications and formal correctness proof for Rust programs. We have tried various techniques, such as RAG, agent system building, model fine tuning, and reinforcement learning, and have observed the models getting increasingly better at code reasoning with the support of formal verification tools and agent systems. I will share this journey with the audience in this talk.

Shan Lu is a Professor in the Department of Computer Science at the University of Chicago. She received her Ph.D. at University of Illinois, Urbana-Champaign, in 2008. She was the Clare Boothe Luce Assistant Professor of Computer Sciences at University of Wisconsin, Madison, from 2009 to 2014. Her research focuses on software reliability and efficiency, particularly detecting, diagnosing, and fixing functional and performance bugs in large software systems.

Shan is an ACM Distinguished Member (2019 class), an Alfred P. Sloan Research Fellow (2014), a Distinguished Educator Alumnus from Department of Computer Science at University of Illinois (2013), and NSF Career Award recipient (2010). Her co-authored papers won Google Scholar Classic Paper 2017, Best Paper Awards at ACM-SIGOPS SOSP 2019, USENIX OSDI 2016 and USENIX FAST 2013, 3 ACM-SIGSOFT Distinguished Paper Awards at ICSE 2019, ICSE 2015 and FSE 2014, an ACM-SIGPLAN Research Highlight Award at PLDI 2011, and an IEEE Micro Top Picks in ASPLOS 2006.

Shan currently serves as the Chair of ACM-SIGOPS (2019 –), Member-at-Large of ACM SIG Governing Board Executive Committee (2020 – 2022), and the Associate Editor for IEEE Computer Architecture Letters. She serves/served as the technical program co-chair for USENIX Symposium on Operating Systems Design and Implementation (OSDI) in 2020, USENIX Annual Technical Conference (ATC) in 2015, and ACM Asia-Pacific Systems Workshop (APSys) in 2018.