Dafny as Verification-Aware Intermediate Language for Code Generation

This conference talk explores how formal methods can improve code generation from large language models (LLMs) by using Dafny as an intermediate verification layer. Learn how researchers from MIT and Amazon Web Services developed a system where LLMs generate code in Dafny first, allowing automatic validation against specifications before compiling to target languages—all while keeping the verification process invisible to users. The presentation covers their prototype implementation and its performance on HumanEval Python benchmarks, demonstrating a promising approach to addressing the reliability issues in LLM-generated code. The 15-minute talk was presented at the Dafny 2025 workshop on January 19, 2025, sponsored by ACM SIGPLAN.