Shift-Left Requirements Verification: Integrating LLMs and Formal Methods for Automotive Systems

Zi Pong Lim, Bozhi Wu, Yon Shin Teo, Shang-Wei Lin, and Yi Li

In Proceedings of the 27th International Symposium on Formal Methods (FM), 2026

Abstract: Requirement defects are a major source of late-stage failures in automotive systems, yet rigorous validation is rarely applied during early development. While formal methods offer strong guarantees, their adoption at the requirements level is limited by high formalization cost and expertise barriers. We present an industry-oriented, shift-left verification approach that integrates Large Language Models (LLMs) with formal methods to enable requirements-level validation. Requirements are classified and decomposed by LLMs, translated into CSP system models and assertions, and refined through a CEGAR-inspired loop using the FDR4 model checker. Validation is decomposed into requirement–assertion pairs supported by natural-language back-translations and confidence scores, preserving expert control without manual formal modeling. Domain knowledge–based validation further leverages historical defect data to identify implicit requirement gaps. We evaluate the approach on three real-world automotive case studies. Results show high automation for small-to-medium systems (80–100% synthesis success for up to ~60 requirements), effective expert validation guided by LLM confidence estimates, and 100% detection of known historical defects alongside 22 novel gaps. The workflow completes within 10–35 minutes per project at negligible cost (<$8 per project), with limited expert effort. Our results demonstrate that LLM+formal method hybridization can provide scalable, rigorous, and industrially viable requirements-level verification, supporting practical shift-left adoption in automotive systems.

Cite:

@inproceedings{Lim2026SLR,
  author = {Lim, Zi Pong and Wu, Bozhi and Teo, Yon Shin and Lin, Shang-Wei and Li, Yi},
  booktitle = {Proceedings of the 27th International Symposium on Formal Methods (FM)},
  month = may,
  title = {Shift-Left Requirements Verification: Integrating {LLMs} and Formal Methods for Automotive Systems},
  year = {2026}
}