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

TL;DR

The paper addresses vulnerability detection by contrasting formal verification, LLM-based analysis, and hybrid methods. It analyzes each approach's strengths and limitations, with examples like ESBMC and PropertyGPT illustrating how formal checks guide AI-driven analyses. It demonstrates that hybrid pipelines can achieve broader coverage and better scalability while preserving correctness guarantees. The work highlights a practical path toward robust, adaptive software verification through close collaboration between mathematical rigor and data-driven reasoning.

Abstract

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.

Figures (2)

• Figure 1: High-level categories of Software Testing
• Figure 2: Motivating examples posing challenges for LLMs an FV tools