  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.
