This paper introduces an innovative approach that combines Large Language Models (LLMs) with Formal Verification strategies for automatic software vulnerability repair. Initially, we employ Bounded Model Checking (BMC) to identify vulnerabilities and extract counterexamples. These counterexamples are supported by mathematical proofs and the stack trace of the vulnerabilities. Using a specially designed prompt, we combine the original source code with the identified vulnerability, including its stack trace and counterexample that specifies the line number and error type. This combined information is then fed into an LLM, which is instructed to attempt to fix the code. The new code is subsequently verified again using BMC to ensure the fix succeeded. We present the ESBMC-AI framework as a proof of concept, leveraging the well-recognized and industry-adopted Efficient SMT-based Context-Bounded Model Checker (ESBMC) and a pre-trained transformer model to detect and fix errors in C programs, particularly in critical software components. We evaluated our approach on 50,000 C programs randomly selected from the FormAI dataset with their respective vulnerability classifications. Our results demonstrate ESBMC-AI's capability to automate the detection and repair of issues such as buffer overflow, arithmetic overflow, and pointer dereference failures with high accuracy. ESBMC-AI is a pioneering initiative, integrating LLMs with BMC techniques, offering potential integration into the continuous integration and deployment (CI/CD) process within the software development lifecycle.

翻译：本文提出了一种创新方法，将大语言模型与形式化验证策略相结合，实现软件漏洞的自动修复。首先，我们采用有界模型检验来识别漏洞并提取反例。这些反例由数学证明和漏洞的堆栈轨迹提供支持。通过特别设计的提示模板，我们将原始源代码与已识别的漏洞信息（包括堆栈轨迹及指定行号与错误类型的反例）相结合。该组合信息随后输入大语言模型，指令其尝试修复代码。修复后的新代码将再次通过有界模型检验进行验证以确保修复成功。我们提出ESBMC-AI框架作为概念验证，该框架利用业界公认的高效SMT基上下文有界模型检验器与预训练Transformer模型，专门用于检测和修复C程序（尤其是关键软件组件）中的错误。我们从FormAI数据集中随机选取5万个具有相应漏洞分类的C程序进行评估。实验结果表明，ESBMC-AI能够以高精度自动检测并修复缓冲区溢出、算术溢出及指针解引用失败等问题。作为开创性尝试，ESBMC-AI将大语言模型与有界模型检验技术深度融合，为软件开发生命周期中持续集成与持续部署流程的整合提供了可行路径。