# RvLLM: LLM Runtime Verification with Domain Knowledge

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

## Key facts

- Cited by 17 papers in the map (data through 14 Oct 2026).
- Builds on 35 of its 70 references that are in the map.
- First posted on arXiv 24 May 2025.

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Measuring Massive Multitask Language Understanding](https://mlsanity.com/paper/2009.03300/) (2020)
- [Qwen2.5 Technical Report](https://mlsanity.com/paper/2412.15115/) (2024)
- [TruthfulQA: Measuring How Models Mimic Human Falsehoods](https://mlsanity.com/paper/2109.07958/) (2021)
- [Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language models](https://mlsanity.com/paper/2206.04615/) (2022)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [SelfCheckGPT: Zero-Resource Black-Box Hallucination Detection for Generative Large Language Models](https://mlsanity.com/paper/2303.08896/) (2023)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [AGIEval: A Human-Centric Benchmark for Evaluating Foundation Models](https://mlsanity.com/paper/2304.06364/) (2023)
- [C-Eval: A Multi-Level Multi-Discipline Chinese Evaluation Suite for Foundation Models](https://mlsanity.com/paper/2305.08322/) (2023)
- [DecodingTrust: A Comprehensive Assessment of Trustworthiness in GPT Models](https://mlsanity.com/paper/2306.11698/) (2023)
- [SummaC: Re-Visiting NLI-based Models for Inconsistency Detection in Summarization](https://mlsanity.com/paper/2111.09525/) (2021)
- [Trustworthy LLMs: a Survey and Guideline for Evaluating Large Language Models' Alignment](https://mlsanity.com/paper/2308.05374/) (2023)
- [HaluEval: A Large-Scale Hallucination Evaluation Benchmark for Large Language Models](https://mlsanity.com/paper/2305.11747/) (2023)
- [LegalBench: A Collaboratively Built Benchmark for Measuring Legal Reasoning in Large Language Models](https://mlsanity.com/paper/2308.11462/) (2023)
- [Hallucination is Inevitable: An Innate Limitation of Large Language Models](https://mlsanity.com/paper/2401.11817/) (2024)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Don't Make Your LLM an Evaluation Benchmark Cheater](https://mlsanity.com/paper/2311.01964/) (2023)
- [LM vs LM: Detecting Factual Errors via Cross Examination](https://mlsanity.com/paper/2305.13281/) (2023)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Complex Claim Verification with Evidence Retrieved in the Wild](https://mlsanity.com/paper/2305.11859/) (2023)
- [How Many Unicorns Are in This Image? A Safety Evaluation Benchmark for Vision LLMs](https://mlsanity.com/paper/2311.16101/) (2023)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [LLMs Will Always Hallucinate, and We Need to Live With This](https://mlsanity.com/paper/2409.05746/) (2024)
- [ChatGPT as a Factual Inconsistency Evaluator for Text Summarization](https://mlsanity.com/paper/2303.15621/) (2023)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Red Teaming Visual Language Models](https://mlsanity.com/paper/2401.12915/) (2024)
- [MultiTrust: A Comprehensive Benchmark Towards Trustworthy Multimodal Large Language Models](https://mlsanity.com/paper/2406.07057/) (2024)
- [ALI-Agent: Assessing LLMs' Alignment with Human Values via Agent-based Evaluation](https://mlsanity.com/paper/2405.14125/) (2024)

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

- [Trust but Verify! A Survey on Verification Design for Test-time Scaling](https://mlsanity.com/paper/2508.16665/) (2025)
- [Cryptographic Runtime Governance for Autonomous AI Systems: The Aegis Architecture for Verifiable Policy Enforcement](https://mlsanity.com/paper/2603.16938/) (2026)
- [AI-NativeBench: An Open-Source White-Box Agentic Benchmark Suite for AI-Native Systems](https://mlsanity.com/paper/2601.09393/) (2026)
- [Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems](https://mlsanity.com/paper/2511.14435/) (2025)
- [LLM-enabled Applications Require System-Level Threat Monitoring](https://mlsanity.com/paper/2602.19844/) (2026)
- [Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization](https://mlsanity.com/paper/2605.10974/) (2026)
- [Evaluating LLM-Generated ACSL Annotations for Formal Verification](https://mlsanity.com/paper/2602.13851/) (2026)
- [Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic](https://mlsanity.com/paper/2602.18607/) (2026)
- [One-Token Verification for Reasoning Correctness Estimation](https://mlsanity.com/paper/2603.01025/) (2026)
- [Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows](https://mlsanity.com/paper/2605.20923/) (2026)
- [Representation Transitions Reveal Emerging Safety Risks in Multi-Turn LLM Agents](https://mlsanity.com/paper/2610.00400/) (2026)
- [ATLAS-RTC: Closing the Loop on LLM Agent Output with Token-Level Runtime Control](https://mlsanity.com/paper/2603.27905/) (2026)
- [Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study](https://mlsanity.com/paper/2604.14867/) (2026)
- [TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples](https://mlsanity.com/paper/2605.07935/) (2026)
- [Who Holds the Pen? Let Specifications, Not Agents, Sign Off](https://mlsanity.com/paper/2609.29921/) (2026)
- [RSure-Agent: Reliable Use of Tool Observations for Remote Sensing Agents](https://mlsanity.com/paper/2610.04836/) (2026)
- [One Monitor Does Not Fit All: Formalism-Agnostic Runtime Verification for Agentic AI](https://mlsanity.com/paper/2610.19818/) (2026)

## Abstract (arXiv)

Large language models (LLMs) have emerged as a dominant AI paradigm due to their exceptional text understanding and generation capabilities. However, their tendency to generate inconsistent or erroneous outputs challenges their reliability, especially in high-stakes domains requiring accuracy and trustworthiness. Existing research primarily focuses on detecting and mitigating model misbehavior in general-purpose scenarios, often overlooking the potential of integrating domain-specific knowledge. In this work, we advance misbehavior detection by incorporating domain knowledge. The core idea is to design a general specification language that enables domain experts to customize domain-specific predicates in a lightweight and intuitive manner, supporting later runtime verification of LLM outputs. To achieve this, we design a novel specification language, ESL, and introduce a runtime verification framework, RvLLM, to validate LLM output against domain-specific constraints defined in ESL. We evaluate RvLLM on three representative tasks: violation detection against Singapore Rapid Transit Systems Act, numerical comparison, and inequality solving. Experimental results demonstrate that RvLLM effectively detects erroneous outputs across various LLMs in a lightweight and flexible manner. The results reveal that despite their impressive capabilities, LLMs remain prone to low-level errors due to limited interpretability and a lack of formal guarantees during inference, and our framework offers a potential long-term solution by leveraging expert domain knowledge to rigorously and efficiently verify LLM outputs.