CLOVER: Closed-Loop Verifiable Code Generation - Dafny'24

Explore a groundbreaking approach to ensuring correctness in AI-generated code through this 20-minute conference talk presented at ACM SIGPLAN. Dive into the Clover (Closed-Loop Verifiable Code Generation) paradigm, which transforms correctness checking into a more manageable consistency checking problem. Learn about the innovative checker that utilizes formal verification tools and large language models to perform consistency checks among code, docstrings, and formal annotations. Examine the theoretical analysis supporting Clover's effectiveness and review empirical findings from the CloverBench dataset, featuring annotated Dafny programs. Discover how large language models show promise in automatically generating formal specifications and explore the consistency checker's impressive acceptance rate for correct instances while maintaining zero tolerance for incorrect ones.