Primary Investigator:
Jamie Davis

Project Members
Elijah Jorgensen, Yu-Wei (Sean) Chang, Gaurav Vermani, Arpan Swaroop, Paschal Amusuo, James C. Davis

High-integrity cyber-physical systems heavily rely on C/C++, making them inherently vulnerable to critical memory safety flaws. While Bounded Model Checking (BMC) provides mathematical assurance against these defects, its industrial adoption is severely hindered by the manual engineering effort required to generate proof harnesses. Recent advancements, such as the LLM-driven AutoUP tool, successfully automate component-level harness generation. However, applying these techniques at a codebase-wide scale remains computationally and operationally intractable without significant user intervention. This research presents the LLM-Augmented Formal Verification Toolchain (LAFVT), an orchestration framework designed to transition automated formal verification into a scalable, industry-ready system. LAFVT addresses the scalability bottleneck through a modular, three-stage pipeline: Analyzer: Prioritizes verification targets using AST-derived complexity (Lizard) and vulnerability (LEOPARD) metrics, efficiently focusing computational resources on high-risk functions. Proofer: Orchestrates and parallelizes AutoUP harness generation and CBMC execution, dramatically improving verification throughput. Report Generator: Transforms raw verification logs into an interactive codebase summary, grouping violations by threat severity and providing actionable fix suggestions for developers. Experimental evaluation on the RIOT operating system demonstrated a reduction in verification time for 192 functions from 288 hours to 30 hours. Furthermore, LAFVT successfully triaged 147 memory-safety violations. By orchestrating harness generation and automating output analysis, LAFVT establishes a practical pathway for integrating formal verification into standard industrial software engineering lifecycles