Using large language models (LLMs) to generate source code from natural language prompts is a popular and promising idea with a wide range of applications. One of its limitations is that the generated code can be faulty at times, often in a 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 an opaque intermediate representation, in the verification-aware language Dafny, that can be automatically validated for correctness against agreed on specifications. The correct Dafny program is then compiled to the target language and returned to the user. All user-system interactions throughout the procedure occur via natural language; Dafny code is never exposed. We describe our current prototype and report on its performance on the HumanEval Python code generation benchmarks.
Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
Shanghai AI Lab（上海人工智能实验室）；University of Alberta（阿尔伯塔大学）；Tsinghua University（清华大学）；Chinese University of Hong Kong, Shenzhen（香港大学（深圳））；Hong Kong University of Science and Technology（香港科技大学）；Nanyang Technological University（南洋理工大学）；University of Manchester（曼彻斯特大学）；Peking University（北京大学）
From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
Department of Computer Science, The University of Alabama（阿拉巴马大学计算机科学系）；The University of Alabama（阿拉巴马大学）；Alabama Water Institute, The University of Alabama（阿拉巴马水研究院，阿拉巴马大学）
DafnyBench: A Benchmark for Formal Software Verification
Harvard College（哈佛学院）；Massachusetts Institute of Technology（麻省理工学院）；Northeastern University（东北大学）；Stanford University（斯坦福大学）；University of California Irvine（加州大学欧文分校）；Harvard University（哈佛大学）
VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Kempner Institute at Harvard University（哈佛大学肯普纳研究所）；Harvard University（哈佛大学）；TU München（慕尼黑工业大学）；Northeastern University（东北大学）；University of Alabama at Birmingham（阿拉巴马大学伯明翰分校）；University of Oxford（牛津大学）
MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
INESC TEC, Faculdade de Engenharia, Universidade do Porto（波尔图大学工程学院）；Faculdade de Engenharia, Universidade do Porto & LASIGE, Universidade de Lisboa（波尔图大学工程学院）
From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
The Hong Kong University of Science and Technology（香港科学与技术大学）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；Guangzhou Institute of Technology, Xidian University（西安电子科技大学广州研究院）；Chongqing University（重庆大学）；ICTT and ISN Laboratory, Xidian University（西安电子科技大学ICTT和ISN实验室）
RAG-Star: Enhancing Deliberative Reasoning with Retrieval Augmented Verification and Refinement
Gaoling School of Artificial Intelligence, Renmin University of China（中国人民大学高瓴人工智能学院）；Wuhan University of Science and Technology（武汉科技大学）；National University of Singapore（新加坡国立大学）；Northeastern University at Qinhuangdao（东北大学秦皇岛分校）；BOSS Zhipin（BOSS直聘）
Teaching Code LLMs to Reason with Intermediate Formal Specifications
FPT Software AI Center（FPT软件人工智能中心）；University of Texas at Dallas（德克萨斯大学达拉斯分校）；Hanoi Univ. of Science and Tech.（河内科学技术大学）；Texas, USA（得克萨斯州，美国）；Hanoi, Vietnam（河内，越南）
Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
Lancaster University（兰卡斯特大学）；Tsinghua University（清华大学）；Harbin Institute of Technology（哈尔滨工业大学）；Southwest University（西南大学）；Aarhus University（奥胡斯大学）；University of York（约克大学）
Verification of Programs via Intermediate Interpretation
我们探讨了一种方法来验证程序通过程序转换适用于解释器的程序设计语言。一种被称为Turchin超级编译的专门化技术被用来专门化程序模型的一些解释器。我们发现，几个安全属性的功能程序建模一类的缓存一致性协议可以证明由超级编译器和比较结果与我们以前的工作直接验证通过超级编译不使用中间解释。我们的方法部分受到了E. De Angelis等人（2014-2015）在约束逻辑程序专门化的背景下研究了通过程序转换和中间解释进行的验证。
Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover
Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education（教育部高可信软件技术重点实验室；北京大学计算机学院）；School of Computer Science Peking University
