# A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification

arXiv: https://arxiv.org/abs/2305.14752 · HTML: https://mlsanity.com/paper/2305.14752/

## Key facts

- Cited by 42 papers in the map (data through 14 Oct 2026).
- Builds on 52 of its 132 references that are in the map.
- First posted on arXiv 24 May 2023.

## Builds on (most cited first, 30 of 52)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Sequence to Sequence Learning with Neural Networks](https://mlsanity.com/paper/1409.3215/) (2014)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [Measuring Coding Challenge Competence With APPS](https://mlsanity.com/paper/2105.09938/) (2021)
- [CodeXGLUE: A Machine Learning Benchmark Dataset for Code Understanding and Generation](https://mlsanity.com/paper/2102.04664/) (2021)
- [CodeSearchNet Challenge: Evaluating the State of Semantic Code Search](https://mlsanity.com/paper/1909.09436/) (2019)
- [A Prompt Pattern Catalog to Enhance Prompt Engineering with ChatGPT](https://mlsanity.com/paper/2302.11382/) (2023)
- [Prompt Programming for Large Language Models: Beyond the Few-Shot Paradigm](https://mlsanity.com/paper/2102.07350/) (2021)
- [Devign: Effective Vulnerability Identification by Learning Comprehensive Program Semantics via Graph Neural Networks](https://mlsanity.com/paper/1909.03496/) (2019)
- [Can language models learn from explanations in context?](https://mlsanity.com/paper/2204.02329/) (2022)
- [MathPrompter: Mathematical Reasoning using Large Language Models](https://mlsanity.com/paper/2303.05398/) (2023)
- [OpenAGI: When LLM Meets Domain Experts](https://mlsanity.com/paper/2304.04370/) (2023)
- [GitHub Copilot AI pair programmer: Asset or Liability?](https://mlsanity.com/paper/2206.15331/) (2022)
- [SequenceR: Sequence-to-Sequence Learning for End-to-End Program Repair](https://mlsanity.com/paper/1901.01808/) (2018)
- [Deep Learning based Vulnerability Detection: Are We There Yet?](https://mlsanity.com/paper/2009.07235/) (2020)
- [Practical Program Repair in the Era of Large Pre-trained Language Models](https://mlsanity.com/paper/2210.14179/) (2022)
- [Keep the Conversation Going: Fixing 162 out of 337 bugs for 0.42 each using ChatGPT](https://mlsanity.com/paper/2304.00385/) (2023)
- [InferFix: End-to-End Program Repair with LLMs](https://mlsanity.com/paper/2303.07263/) (2023)
- [Self-Edit: Fault-Aware Code Editor for Code Generation](https://mlsanity.com/paper/2305.04087/) (2023)
- [An Analysis of the Automatic Bug Fixing Performance of ChatGPT](https://mlsanity.com/paper/2301.08653/) (2023)
- [Examining Zero-Shot Vulnerability Repair with Large Language Models](https://mlsanity.com/paper/2112.02125/) (2021)
- [Jigsaw: Large Language Models meet Program Synthesis](https://mlsanity.com/paper/2112.02969/) (2021)
- [Large Language Models are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models](https://mlsanity.com/paper/2212.14834/) (2022)
- [CURE: Code-Aware Neural Machine Translation for Automatic Program Repair](https://mlsanity.com/paper/2103.00073/) (2021)
- [Less Training, More Repairing Please: Revisiting Automated Program Repair via Zero-shot Learning](https://mlsanity.com/paper/2207.08281/) (2022)
- [Is ChatGPT the Ultimate Programming Assistant -- How far is it?](https://mlsanity.com/paper/2304.11938/) (2023)

## Built on by (most cited first, 30 of 42)

- [Large Language Models for Software Engineering: A Systematic Literature Review](https://mlsanity.com/paper/2308.10620/) (2023)
- [When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs](https://mlsanity.com/paper/2406.01297/) (2024)
- [Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategies](https://mlsanity.com/paper/2308.03188/) (2023)
- [Recursive Introspection: Teaching Language Model Agents How to Self-Improve](https://mlsanity.com/paper/2407.18219/) (2024)
- [Large Language Models for Cyber Security: A Systematic Literature Review](https://mlsanity.com/paper/2405.04760/) (2024)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [CyberMetric: A Benchmark Dataset based on Retrieval-Augmented Generation for Evaluating LLMs in Cybersecurity Knowledge](https://mlsanity.com/paper/2402.07688/) (2024)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification](https://mlsanity.com/paper/2307.02192/) (2023)
- [Large Language Models in Cybersecurity: State-of-the-Art](https://mlsanity.com/paper/2402.00891/) (2024)
- [LLMs in Web Development: Evaluating LLM-Generated PHP Code Unveiling Vulnerabilities and Limitations](https://mlsanity.com/paper/2404.14459/) (2024)
- [PromSec: Prompt Optimization for Secure Generation of Functional Source Code with Large Language Models (LLMs)](https://mlsanity.com/paper/2409.12699/) (2024)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection](https://mlsanity.com/paper/2503.09433/) (2025)
- [Think Thrice Before You Act: Progressive Thought Refinement in Large Language Models](https://mlsanity.com/paper/2410.13413/) (2024)
- [Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview](https://mlsanity.com/paper/2503.10784/) (2025)
- [Self-Refining Vision Language Model for Robotic Failure Detection and Reasoning](https://mlsanity.com/paper/2602.12405/) (2026)
- [ZeroLeak: Using LLMs for Scalable and Cost Effective Side-Channel Patching](https://mlsanity.com/paper/2308.13062/) (2023)
- [Helping LLMs Improve Code Generation Using Feedback from Testing and Static Analysis](https://mlsanity.com/paper/2412.14841/) (2024)
- [LUNA: A Model-Based Universal Analysis Framework for Large Language Models](https://mlsanity.com/paper/2310.14211/) (2023)
- [Enhancing Source Code Security with LLMs: Demystifying The Challenges and Generating Reliable Repairs](https://mlsanity.com/paper/2409.00571/) (2024)
- [Automated Repair of AI Code with Large Language Models and Formal Verification](https://mlsanity.com/paper/2405.08848/) (2024)
- [Towards Large Language Model Aided Program Refinement](https://mlsanity.com/paper/2406.18616/) (2024)
- [Do AI models help produce verified bug fixes?](https://mlsanity.com/paper/2507.15822/) (2025)
- [Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach](https://mlsanity.com/paper/2312.17353/) (2023)
- [Using ML filters to help automated vulnerability repairs: when it helps and when it doesn't](https://mlsanity.com/paper/2504.07027/) (2025)
- [A Blueprint for AI-Driven Software Quality: Integrating LLMs with Established Standards](https://mlsanity.com/paper/2505.13766/) (2025)
- [Leveraging Large Language Models for Command Injection Vulnerability Analysis in Python: An Empirical Study on Popular Open-Source Projects](https://mlsanity.com/paper/2505.15088/) (2025)
- [Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models](https://mlsanity.com/paper/2506.08171/) (2025)
- [Towards Automated Formal Verification of Backend Systems with LLMs](https://mlsanity.com/paper/2506.10998/) (2025)

## Abstract (arXiv)

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.