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

Approach

• ESBMC-AI uses ESBMC-generated stack traces and counterexamples to guide an LLM in repairing vulnerable C programs.Failed verification passes the original code and property-violation output to the LLM, whose generated code is verified again iteratively.Source: §I · pp. 1–2, Figure 1 · p. 2

Motivation

• Standalone LLM repair is unreliable because code repair requires precise bit-level reasoning, SMT solving, AST parsing, and data-flow analysis.The paper motivates external verification as a guide for locating and repairing vulnerabilities.Source: §I · p. 1

Research questions

• The study asks whether formal-verification feedback improves LLM repair, which vulnerabilities remain difficult, and whether generated patches stay compilable without disrupting program workflows.These questions frame effectiveness, vulnerability-specific difficulty, and patch reliability.Source: §I · p. 2

Evaluation

• The evaluation uses C programs randomly selected from the FormAI dataset to assess ESBMC-AI’s repair effectiveness.The contribution passage describes an assessment on over 1,000 programs.Source: §I · p. 2

Results

• 90.40% accuracy was achieved for buffer overflow on scanf, 86.47% for division by zero, 70.27% for arithmetic overflow on add, and 69.66% for array bounds violations.The reported accuracies were checked by at least one human expert.Source: §I · p. 2

Motivation

• LLMs may generate multiple alternatives without identifying vulnerability roots, whereas BMC detects vulnerabilities through mathematical proofs but requires expertise to translate outputs into repairs.The example motivates combining complementary capabilities rather than relying on either component alone.Source: §II · pp. 2–3

Motivation example

• BMC identifies the arithmetic overflow with a property violation, stack trace, and counterexample that direct LLM questioning misses.GPT-3.5 incorrectly judged the computed value representable within a 32-bit integer range.Source: §II · p. 3

Guided repair

• The LLM repairs the overflow by replacing int with long long int after receiving the BMC-guided diagnosis.The guidance identifies the vulnerable multiplication and the limited range of int.Source: §II · p. 3

Verification

• The updated program receives a “VERIFICATION SUCCESSFUL” result, indicating no integer boundary violations or overflows in the modified code.The example supports the feasibility of counterexample-guided automatic code repair.Source: §II · p. 3

A. Traditional Vulnerability Detection

• Static analysis enables early detection but often has high false-positive rates, while dynamic analysis is input-dependent, incomplete, and expensive.Hybrid methods combine these approaches to balance their strengths and weaknesses.Source: A. Traditional Vulnerability Detection · p. 3
• BMC limits exploration depth to provide reliable results at reduced cost, although related BMC-fuzzing approaches may still scale poorly.The cited discussion contrasts restricted-depth verification with scalability limitations.Source: A. Traditional Vulnerability Detection · pp. 3–4

B. Deep Learning-based Vulnerability Detection

• Deep-learning repair systems generate patches using sequence-to-sequence models, transfer learning, AST differencing, code similarity, or language-model fine-tuning.Examples include DeepFix, SEQUENCER, VRepair, DEAR, DeepRepair, and LLMC-based approaches.Source: B. Deep Learning-based Vulnerability… · p. 4
• LLM-based repair has expanded beyond compile-time errors, but synthesized code and patches can remain incorrect or untrustworthy.Feedback mechanisms include compiler results, tests, bug information, and validation tools, each with stated limitations.Source: B. Deep Learning-based Vulnerability… · p. 4
• ESBMC-AI explores the previously uninvestigated combination of LLMs with formal verification, using symbolic model-checking feedback to improve patch quality and repair speed.The framework seeks a balance between symbolic verification and deep learning.Source: B. Deep Learning-based Vulnerability… · p. 4

IV. BACKGROUND: FORMAL VERIFICATION MEETS LARGE LANGUAGE MODELS

• BMC and LLMs are combined by using BMC diagnostic counterexamples to guide an LLM toward tentative code repairs.BMC verifies programs and provides textual traces; the LLM interprets those traces and proposes fixes.Source: §IV · p. 4, A. Bounded Model Checking (BMC) · p. 5

A. Bounded Model Checking (BMC)

• BMC represents a program as a state-transition system derived from its control-flow graph and translated into SSA expressions for SMT solving.States encode the program counter and variable values, while transitions encode possible control and data changes.Source: A. Bounded Model Checking (BMC) · p. 4
• Table I compares related software bug-detection and repair approaches.The supplied passage identifies the table’s scope but provides no cell values or comparison outcome.Source: Table I · p. 5
• The BMC formulation checks whether an execution within bound k reaches a state violating the safety property ϕ.If satisfiable, the solver provides an assignment from which a counterexample can be extracted.Source: A. Bounded Model Checking (BMC) · p. 5
• A counterexample is a finite state trace showing how execution proceeds from the program entry point to the violated property.The trace informs the LLM about the path reproducing the vulnerability and supports targeted correction.Source: A. Bounded Model Checking (BMC) · p. 5
• When the BMC formula is unsatisfiable, the method concludes that no error state is reachable within the checked bound.This conclusion is bounded by k and does not establish absence of vulnerabilities beyond that exploration depth.Source: A. Bounded Model Checking (BMC) · p. 5
• Counterexamples identify the exact trace, line number, and variable involved, making them actionable inputs for LLM repair.Because they are based on mathematical proofs, they can reduce false positives relative to simple static-analysis results, although implementation errors may remain.Source: A. Bounded Model Checking (BMC) · p. 5

B. Large Language Models (LLMs)

• LLMs transform token sequences into high-dimensional representations and generate likely next tokens through layered nonlinear transformations.They are less efficient than BMC for exact arithmetic and bounded checking but excel at language-processing tasks.Source: B. Large Language Models (LLMs) · pp. 5–6
• The paper frames GPT-3, GPT-4, BERT, and T5 as transformer-based models trained or studied for language understanding and few-shot or contextual learning.These examples motivate using transformer architectures for interpreting BMC counterexamples.Source: B. Large Language Models (LLMs) · p. 6
• Transformer attention helps models focus on different parts of complex BMC inputs when producing human-readable interpretations.The paper identifies scaled dot-product and multi-head attention as mechanisms supporting this translation.Source: B. Large Language Models (LLMs) · p. 6
• In the paper’s example, attention links an overflow, the multiplication expression mul(y,y), and its specific line number.This linkage supports recommending a code fix for the associated vulnerability.Source: B. Large Language Models (LLMs) · p. 6
• Transformer models can relate separated input segments, enabling more context-sensitive recommendations for code debugging and automatic repair.The paper connects this capability to understanding intricate relations within counterexample text.Source: B. Large Language Models (LLMs) · p. 6

V. METHODOOLOGY

• ESBMC-AI runs a BMC tool in the background to detect vulnerabilities using formal-verification techniques.The generated counterexample is then provided to the LLM with a specially crafted prompt.Source: §V · p. 6

A. Why ESBMC?

• ESBMC was selected because SV-COMP 2024 reported that it solves the highest number of reachability-safety tasks within 10 seconds.The 10-second limit is intended to support nearly real-time feedback in IDE and CI pipelines.Source: A. Why ESBMC? · p. 6

B. User Chat Mode (UCM) and Fix Code Mode (FCM)

• UCM explains ESBMC counterexamples for users without automatically changing code, while FCM targets compilable automatic repairs that preserve original behavior.FCM requires vulnerability-specific prompts and expert review because generic prompts reduce repair accuracy.Source: B. User Chat Mode (UCM) and Fix Code… · pp. 6–7

C. The ESBMC-AI Evaluation Dataset

• FormAI contains 112,000 compilable, vulnerability-labeled C programs, and the study prepared 50,000 samples using stronger unbounded classification with a 500-second timeout.Random samples from eight vulnerability categories were manually inspected to verify the approach.Source: C. The ESBMC-AI Evaluation Dataset · p. 7

VI. EXPERIMENTAL RESULTS

• The evaluation classified 31,801 of 50,000 samples as verification failures, indicating that 63.60% of the code was vulnerable.Vulnerabilities were grouped into dereference failures, arithmetic overflows, and buffer overflows; their detailed distribution appears in Table II.Source: §VI · p. 7, Table II · p. 7
• The experiments used GPT-4o with ESBMC configured for overflow, memory-leak, stack-trace, timeout, unwinding, and multi-property checks.In practical use, real-time verification identifies vulnerabilities, transforms counterexamples, and inserts them into expert-designed prompts.Source: §VI · pp. 7–8

Buffer overflow on scanf and fscanf

• 90.40% accuracy was achieved for 175 fscanf() fixes, including 160 successful, 8 failed, and 7 unknown verification results.The reviewed successful patches were correct, compilable, and preserved original program behavior.Source: A. Experimental result on automated… · p. 8

Array bounds violations

• 95.60% success for upper-bound array violations contrasted with 41.03% for lower-bound violations.Lower-bound errors were generally easier to fix, while upper-bound repairs often incorrectly increased a variable by one.Source: A. Experimental result on automated… · p. 8

Buffer overflow on scanf and fscanf

• 91.29% accuracy was achieved across 241 fscanf() programs, with 220 successful fixes and 13 verification failures.Patched programs increased average cyclomatic complexity from 4.61 to 5.62, consistent with adding conditional logic.Source: A. Experimental result on automated… · p. 8

Dereference Failure: forgotten memory

• Dereference-failure repairs achieved a 48.66% success rate across 187 samples.The same issue often reappeared on another line, and formal-verification traces could reveal chains involving functions or files absent from the prompt.Source: A. Experimental result on automated… · p. 8

Division by zero

• 86.47% accuracy was achieved for division-by-zero repairs, based on 133 manually verified samples.Among these samples, 115 fixes succeeded, 8 failed verification, and 10 had unknown results.Source: A. Experimental result on automated… · p. 9

Arithmetic overflow on add

• 70.27% accuracy was achieved for arithmetic-overflow repairs across 73 samples, because fixing one overflow can introduce another.Two iterations addressing addition overflow followed by floating-point multiplication overflow reached 88% accuracy on the same samples.Source: A. Experimental result on automated… · p. 9

LLMs fixation without external help

• LLM fixes reached approximately 80% to 90% accuracy with ESBMC output, compared with 31−37% without exact counterexamples and stack traces.The formal-verification evidence guides the model toward the correct vulnerability and repair direction.Source: B. LLMs fixation without external help · p. 9
• Without formal-verification guidance, the model proposed unrelated issues such as MD5 insecurity instead of recognizing an arithmetic overflow.ESBMC-AI correctly identified and fixed the overflow using the formal counterexample, whereas repeated unguided attempts remained incorrect.Source: B. LLMs fixation without external help · p. 9

Threats to the Validity

• Syntactically valid LLM repairs may fail to address the underlying bug or may introduce new issues.The authors identify hallucination and limited explainability as additional uncertainties requiring stronger interpretability and reliability mechanisms.Source: C. Threats to the Validity · p. 9
• Misleading function names can cause an LLM to overlook the actual vulnerability.This illustrates a failure mode in which surface-level code cues divert the model from the true defect.Source: Figure 2 · p. 10

• ESBMC-AI uses bounded-model-checking feedback to improve automated repair with large language models.Source: §VII · p. 10
• Over 90% accuracy is achieved for scanf/fscanf buffer overflows and lower-bound array violations in a single iteration.More than 80% accuracy is attainable for division by zero and NULL-pointer dereference failures.Source: §VII · p. 10
• Upper-bound array violations and forgotten-memory dereferences are the most challenging cases, often involving other vulnerabilities or external headers and files.Source: §VII · p. 10
• Integrating LLMs with formal verification may require substantial computational resources and risks unintended vulnerabilities or overfitting to specific code patterns.Source: §VII · p. 10
• ESBMC-AI is released as a PyPI module to support use by industrial partners and the research community.Source: §VII · p. 10