Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems
Not on the map. Why?
Abstract (arXiv)
Assuring the safety and trustworthiness of autonomous systems is particularly difficult when learning-enabled components and open environments are involved. Formal methods provide strong guarantees but depend on complete models and static assumptions. Runtime verification (RV) complements them by monitoring executions at run time and, in its predictive variants, by anticipating potential violations. Large language models (LLMs), meanwhile, excel at translating natural language into formal artefacts and recognising patterns in data, yet they remain error-prone and lack formal guarantees. This vision paper argues for a symbiotic integration of RV and LLMs. RV can serve as a guardrail for LLM-driven autonomy, while LLMs can extend RV by assisting specification capture, supporting anticipatory reasoning, and helping to handle uncertainty. We outline how this mutual reinforcement differs from existing surveys and roadmaps, discuss challenges and certification implications, and identify future research directions towards dependable autonomy.
Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). Builds on 10 of its 18 references that are in the map. First posted on arXiv 18 Nov 2025.
Builds on
10 of 18 references.
References · 10
- 2023A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validationcited by 91
- 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
- 2022Conformal Prediction for STL Runtime Verificationcited by 34
- 2024The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmapcited by 20
- 2025RvLLM: LLM Runtime Verification with Domain Knowledgecited by 15
- 2025ClassInvGen: Class Invariant Synthesis using Large Language Modelscited by 11
- 2025Leveraging LLMs for Formal Software Requirements -- Challenges and Prospectscited by 5
- 2025Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specificationscited by 2
- 2025Statistical Runtime Verification for LLMs via Robustness Estimationcited by 2
- 2024Predictive Monitoring with Strong Trace Prefixescited by 1
Built on by
Citing papers per year: 2026: 1.
1 paper.