# Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 37 of its 58 references that are in the map.
- First posted on arXiv 13 Mar 2025.

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

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Large Language Models for Code: Security Hardening and Adversarial Testing](https://mlsanity.com/paper/2302.05319/) (2023)
- [Vulnerability Detection with Code Language Models: How Far Are We?](https://mlsanity.com/paper/2403.18624/) (2024)
- [Automated Vulnerability Detection in Source Code Using Deep Representation Learning](https://mlsanity.com/paper/1807.04320/) (2018)
- [DiverseVul: A New Vulnerable Source Code Dataset for Deep Learning Based Vulnerability Detection](https://mlsanity.com/paper/2304.00409/) (2023)
- [LLMs Cannot Reliably Identify and Reason About Security Vulnerabilities (Yet?): A Comprehensive Evaluation, Framework, and Benchmarks](https://mlsanity.com/paper/2312.12575/) (2023)
- [SySeVR: A Framework for Using Deep Learning to Detect Software Vulnerabilities](https://mlsanity.com/paper/1807.06756/) (2018)
- [CVEfixes: Automated Collection of Vulnerabilities and Their Fixes from Open-Source Software](https://mlsanity.com/paper/2107.08760/) (2021)
- [VulBERTa: Simplified Source Code Pre-Training for Vulnerability Detection](https://mlsanity.com/paper/2205.12424/) (2022)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [Large Language Model for Vulnerability Detection and Repair: Literature Review and the Road Ahead](https://mlsanity.com/paper/2404.02525/) (2024)
- [VulDeeLocator: A Deep Learning-based Fine-grained Vulnerability Detector](https://mlsanity.com/paper/2001.02350/) (2020)
- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [Automatic Programming: Large Language Models and Beyond](https://mlsanity.com/paper/2405.02213/) (2024)
- [(Security) Assertions by Large Language Models](https://mlsanity.com/paper/2306.14027/) (2023)
- [Uncovering the Limits of Machine Learning for Automatic Vulnerability Detection](https://mlsanity.com/paper/2306.17193/) (2023)
- [Generalization-Enhanced Code Vulnerability Detection via Multi-Task Instruction Fine-Tuning](https://mlsanity.com/paper/2406.03718/) (2024)
- [A Manually-Curated Dataset of Fixes to Vulnerabilities of Open-Source Software](https://mlsanity.com/paper/1902.02595/) (2019)
- [How Far Have We Gone in Vulnerability Detection Using Large Language Models](https://mlsanity.com/paper/2311.12420/) (2023)
- [Toward Secure Code Generation: Bridging Correctness and Security via Task-Adaptive Vulnerability Modeling and Execution-Based Benchmarking](https://mlsanity.com/paper/2407.02395/) (2024)
- [How secure is AI-generated Code: A Large-Scale Comparison of Large Language Models](https://mlsanity.com/paper/2404.18353/) (2024)
- [LLMs in Web Development: Evaluating LLM-Generated PHP Code Unveiling Vulnerabilities and Limitations](https://mlsanity.com/paper/2404.14459/) (2024)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [Agentic AI Software Engineers: Programming with Trust](https://mlsanity.com/paper/2502.13767/) (2025)
- [SmartBugs: A Framework to Analyze Solidity Smart Contracts](https://mlsanity.com/paper/2007.04771/) (2020)
- [To Err is Machine: Vulnerability Detection Challenges LLM Reasoning](https://mlsanity.com/paper/2403.17218/) (2024)
- [Magma: A Ground-Truth Fuzzing Benchmark](https://mlsanity.com/paper/2009.01120/) (2020)
- [SecureFalcon: Are We There Yet in Automated Software Vulnerability Detection with LLMs?](https://mlsanity.com/paper/2307.06616/) (2023)
- [Investigating Large Language Models for Code Vulnerability Detection: An Experimental Study](https://mlsanity.com/paper/2412.18260/) (2024)

## Built on by (most cited first, 7 of 7)

- [Systematization of Knowledge: Security and Safety in the Model Context Protocol Ecosystem](https://mlsanity.com/paper/2512.08290/) (2025)
- [Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification](https://mlsanity.com/paper/2510.03469/) (2025)
- [Towards Automated Formal Verification of Backend Systems with LLMs](https://mlsanity.com/paper/2506.10998/) (2025)
- [From LLMs to Agents: A Comparative Evaluation of LLMs and LLM-based Agents in Security Patch Detection](https://mlsanity.com/paper/2511.08060/) (2025)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)
- [OOM-RL: Out-of-Money Reinforcement Learning Market-Driven Alignment for LLM-Based Multi-Agent Systems](https://mlsanity.com/paper/2604.11477/) (2026)
- [When Passing Tests Hides Vulnerabilities: An Empirical Study of Silent Failures in Agentic Systems](https://mlsanity.com/paper/2609.10548/) (2026)

## Abstract (arXiv)

Software testing and verification are critical for ensuring the reliability and security of modern software systems. Traditionally, formal verification techniques, such as model checking and theorem proving, have provided rigorous frameworks for detecting bugs and vulnerabilities. However, these methods often face scalability challenges when applied to complex, real-world programs. Recently, the advent of Large Language Models (LLMs) has introduced a new paradigm for software analysis, leveraging their ability to understand insecure coding practices. Although LLMs demonstrate promising capabilities in tasks such as bug prediction and invariant generation, they lack the formal guarantees of classical methods. This paper presents a comprehensive study of state-of-the-art software testing and verification, focusing on three key approaches: classical formal methods, LLM-based analysis, and emerging hybrid techniques, which combine their strengths. We explore each approach's strengths, limitations, and practical applications, highlighting the potential of hybrid systems to address the weaknesses of standalone methods. We analyze whether integrating formal rigor with LLM-driven insights can enhance the effectiveness and scalability of software verification, exploring their viability as a pathway toward more robust and adaptive testing frameworks.