# Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Placed in General LLM agent frameworks and benchmarks, one of 16 directions in LLM agents and tool use.
- Builds on 13 of its 24 references that are in the map.
- First posted on arXiv 3 Oct 2025.

## Placed in

- LLM agents and tool use / [General LLM agent frameworks and benchmarks](https://mlsanity.com/agents/general-llm-agent-frameworks-and-benchmarks/)

## Builds on (most cited first, 13 of 13)

- [Why Do Multi-Agent LLM Systems Fail?](https://mlsanity.com/paper/2503.13657/) (2025)
- [PlanBench: An Extensible Benchmark for Evaluating Large Language Models on Planning and Reasoning about Change](https://mlsanity.com/paper/2206.10498/) (2022)
- [LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworks](https://mlsanity.com/paper/2402.01817/) (2024)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [CodeMirage: Hallucinations in Code Generated by Large Language Models](https://mlsanity.com/paper/2408.08333/) (2024)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [VeriPlan: Integrating Formal Verification and LLMs into End-User Planning](https://mlsanity.com/paper/2502.17898/) (2025)
- [Formally Specifying the High-Level Behavior of LLM-Based Agents](https://mlsanity.com/paper/2310.08535/) (2023)
- [Software Vulnerability and Functionality Assessment using LLMs](https://mlsanity.com/paper/2403.08429/) (2024)
- [VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models](https://mlsanity.com/paper/2411.19275/) (2024)
- [Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview](https://mlsanity.com/paper/2503.10784/) (2025)
- [Specification and Evaluation of Multi-Agent LLM Systems -- Prototype and Cybersecurity Applications](https://mlsanity.com/paper/2506.10467/) (2025)
- [GenPlanX. Generation of Plans and Execution](https://mlsanity.com/paper/2506.10897/) (2025)

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

- [AgentRx: Diagnosing AI Agent Failures from Execution Trajectories](https://mlsanity.com/paper/2602.02475/) (2026)
- [AgentLTL: A Trace-Verification Framework for Measuring, Enforcing, and Training Procedural Compliance in Tool-Using LLM Agents](https://mlsanity.com/paper/2607.02599/) (2026)
- [Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement](https://mlsanity.com/paper/2608.14590/) (2026)
- [Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory](https://mlsanity.com/paper/2606.06523/) (2026)
- [TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples](https://mlsanity.com/paper/2605.07935/) (2026)
- [Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guarantees](https://mlsanity.com/paper/2608.05493/) (2026)
- [Agentic Cognitive Depth: Operational Criteria for Evaluating LLM Agents](https://mlsanity.com/paper/2610.04168/) (2026)

## Abstract (arXiv)

We introduce a novel framework for evaluating the alignment between natural language plans and their expected behavior by converting them into Kripke structures and Linear Temporal Logic (LTL) using Large Language Models (LLMs) and performing model checking. We systematically evaluate this framework on a simplified version of the PlanBench plan verification dataset and report on metrics like Accuracy, Precision, Recall and F1 scores. Our experiments demonstrate that GPT-5 achieves excellent classification performance (F1 score of 96.3%) while almost always producing syntactically perfect formal representations that can act as guarantees. However, the synthesis of semantically perfect formal models remains an area for future exploration.