# Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 39 of its 83 references that are in the map.
- First posted on arXiv 15 May 2026.

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

- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Constitutional AI: Harmlessness from AI Feedback](https://mlsanity.com/paper/2212.08073/) (2022)
- [The Curious Case of Neural Text Degeneration](https://mlsanity.com/paper/1904.09751/) (2019)
- [Language Models (Mostly) Know What They Know](https://mlsanity.com/paper/2207.05221/) (2022)
- [Red Teaming Language Models with Language Models](https://mlsanity.com/paper/2202.03286/) (2022)
- [Open Problems and Fundamental Limitations of Reinforcement Learning from Human Feedback](https://mlsanity.com/paper/2307.15217/) (2023)
- [Monitoring Reasoning Models for Misbehavior and the Risks of Promoting Obfuscation](https://mlsanity.com/paper/2503.11926/) (2025)
- [ScienceWorld: Is your Agent Smarter than a 5th Grader?](https://mlsanity.com/paper/2203.07540/) (2022)
- [TextWorld: A Learning Environment for Text-based Games](https://mlsanity.com/paper/1806.11532/) (2018)
- [Chain of Thought Monitorability: A New and Fragile Opportunity for AI Safety](https://mlsanity.com/paper/2507.11473/) (2025)
- [AI Control: Improving Safety Despite Intentional Subversion](https://mlsanity.com/paper/2312.06942/) (2023)
- [Automatically Auditing Large Language Models via Discrete Optimization](https://mlsanity.com/paper/2303.04381/) (2023)
- [Auditing large language models: a three-layered approach](https://mlsanity.com/paper/2302.08500/) (2023)
- [Black-Box Access is Insufficient for Rigorous AI Audits](https://mlsanity.com/paper/2401.14446/) (2024)
- [Explore, Establish, Exploit: Red Teaming Language Models from Scratch](https://mlsanity.com/paper/2306.09442/) (2023)
- [Predictive Business Process Monitoring with LSTM Neural Networks](https://mlsanity.com/paper/1612.02130/) (2016)
- [Visibility into AI Agents](https://mlsanity.com/paper/2401.13138/) (2024)
- [LTL2Action: Generalizing LTL Instructions for Multi-Task RL](https://mlsanity.com/paper/2102.06858/) (2021)
- [Plug in the Safety Chip: Enforcing Constraints for LLM-driven Robot Agents](https://mlsanity.com/paper/2309.09919/) (2023)
- [Outsider Oversight: Designing a Third Party Audit Ecosystem for AI Governance](https://mlsanity.com/paper/2206.04737/) (2022)
- [NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models](https://mlsanity.com/paper/2305.07766/) (2023)
- [Monitoring Monitorability](https://mlsanity.com/paper/2512.18311/) (2025)
- [Who Audits the Auditors? Recommendations from a field scan of the algorithmic auditing ecosystem](https://mlsanity.com/paper/2310.02521/) (2023)
- [SCANS: Mitigating the Exaggerated Safety for LLMs via Safety-Conscious Activation Steering](https://mlsanity.com/paper/2408.11491/) (2024)
- [Supporting Human-AI Collaboration in Auditing LLMs with LLMs](https://mlsanity.com/paper/2304.09991/) (2023)
- [AI auditing: The Broken Bus on the Road to AI Accountability](https://mlsanity.com/paper/2401.14462/) (2024)
- [Variational Temporal Abstraction](https://mlsanity.com/paper/1910.00775/) (2019)
- [Avoiding Side Effects By Considering Future Tasks](https://mlsanity.com/paper/2010.07877/) (2020)
- [Learning a natural-language to LTL executable semantic parser for grounded robotics](https://mlsanity.com/paper/2008.03277/) (2020)
- [Can Reasoning Models Obfuscate Reasoning? Stress-Testing Chain-of-Thought Monitorability](https://mlsanity.com/paper/2510.19851/) (2025)

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

- [Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows](https://mlsanity.com/paper/2605.20923/) (2026)
- [BeTaL-GBI: Admission-Aware Benchmark Tuning and Full-Stack Verification of Geometric Belief Interfaces](https://mlsanity.com/paper/2608.21503/) (2026)
- [Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)](https://mlsanity.com/paper/2609.32912/) (2026)

## Abstract (arXiv)

We examine one particular dimension of AI governance: how to monitor and audit AI-enabled products and services throughout the AI development lifecycle, from pre-deployment testing to post-deployment auditing. Combining principles from formal methods with SoTA machine learning, we propose techniques that enable AI-enabled product and service developers, as well as third party AI developers and evaluators, to perform offline auditing and online (runtime) monitoring of product-specific (temporally extended) behavioral constraints such as safety constraints, norms, rules and regulations with respect to black-box advanced AI systems, notably LLMs. We further provide practical techniques for predictive monitoring, such as sampling-based methods, and we introduce intervening monitors that act at runtime to preempt and potentially mitigate predicted violations. Experimental results show that by exploiting the formal syntax and semantics of Linear Temporal Logic (LTL), our proposed auditing and monitoring techniques are superior to LLM baseline methods in detecting violations of temporally extended behavioral constraints; with our approach, even small-model labelers match or exceed frontier LLM judges. Our predictive and intervening monitors significantly reduce the violation rates of LLM-based agents while largely preserving task performance. We further show through controlled experiments that LLMs' temporal reasoning shows a pronounced degradation in accuracy with increasing event distance, number of constraints, and number of propositions.