Dafny as Verification-Aware Intermediate Language for Code Generation

We will revisit this example later on. Using large language models (LLMs) to generate source code In this paper, we propose to utilise Dafny as an intermediate from natural language prompts is a popular and promising technology within a code-generating chatbot prototype idea with a wide range of applications. One of its limitations on the way to higher quality mainstream-language code. is that the generated code can be faulty at times, often in a Dafny is particularly well-suited for this purpose, because: subtle way, despite being presented to the user as correct. In this paper, we explore ways in which formal methods can assist with increasing the quality of code generated by an LLM. Instead of emitting code in a target language directly, we propose that the user guides the LLM to first generate 1. It allows for a clear distinction between the specification an opaque intermediate representation, in the verificationaware of a program--derived from a natural language language Dafny, that can be automatically validated prompt using an LLM--and its implementation, which for correctness against agreed on specifications. The correct can again be dialogically derived using an LLM with Dafny program is then compiled to the target language and verification feedback in the loop.