# VeriPlan: Integrating Formal Verification and LLMs into End-User Planning

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

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- Builds on 63 of its 125 references that are in the map.
- First posted on arXiv 25 Feb 2025.

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting](https://mlsanity.com/paper/2305.04388/) (2023)
- [Large Language Models are not Fair Evaluators](https://mlsanity.com/paper/2305.17926/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [On Faithfulness and Factuality in Abstractive Summarization](https://mlsanity.com/paper/2005.00661/) (2020)
- [CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquing](https://mlsanity.com/paper/2305.11738/) (2023)
- [ChatEval: Towards Better LLM-based Evaluators through Multi-Agent Debate](https://mlsanity.com/paper/2308.07201/) (2023)
- [MathVerse: Does Your Multi-modal LLM Truly See the Diagrams in Visual Math Problems?](https://mlsanity.com/paper/2403.14624/) (2024)
- [LLM-Planner: Few-Shot Grounded Planning for Embodied Agents with Large Language Models](https://mlsanity.com/paper/2212.04088/) (2022)
- [Understanding the planning of LLM agents: A survey](https://mlsanity.com/paper/2402.02716/) (2024)
- [Harnessing the Power of LLMs in Practice: A Survey on ChatGPT and Beyond](https://mlsanity.com/paper/2304.13712/) (2023)
- [Describe, Explain, Plan and Select: Interactive Planning with Large Language Models Enables Open-World Multi-Task Agents](https://mlsanity.com/paper/2302.01560/) (2023)
- [TravelPlanner: A Benchmark for Real-World Planning with Language Agents](https://mlsanity.com/paper/2402.01622/) (2024)
- [A Survey of Hallucination in Large Foundation Models](https://mlsanity.com/paper/2309.05922/) (2023)
- [Explainability for Large Language Models: A Survey](https://mlsanity.com/paper/2309.01029/) (2023)
- [On the Planning Abilities of Large Language Models : A Critical Investigation](https://mlsanity.com/paper/2305.15771/) (2023)
- [LEVER: Learning to Verify Language-to-Code Generation with Execution](https://mlsanity.com/paper/2302.08468/) (2023)
- [Making Large Language Models Better Reasoners with Step-Aware Verifier](https://mlsanity.com/paper/2206.02336/) (2022)
- [Large Language Models as General Pattern Machines](https://mlsanity.com/paper/2307.04721/) (2023)
- [LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworks](https://mlsanity.com/paper/2402.01817/) (2024)
- [LLM Lies: Hallucinations are not Bugs, but Features as Adversarial Examples](https://mlsanity.com/paper/2310.01469/) (2023)
- [Benchmarking Cognitive Biases in Large Language Models as Evaluators](https://mlsanity.com/paper/2309.17012/) (2023)
- [Who Validates the Validators? Aligning LLM-Assisted Evaluation of LLM Outputs with Human Preferences](https://mlsanity.com/paper/2404.12272/) (2024)
- [Generalized Planning in PDDL Domains with Pretrained Large Language Models](https://mlsanity.com/paper/2305.11014/) (2023)
- [Uncertainty as a Form of Transparency: Measuring, Communicating, and Using Uncertainty](https://mlsanity.com/paper/2011.07586/) (2020)
- [Reframing Human-AI Collaboration for Generating Free-Text Explanations](https://mlsanity.com/paper/2112.08674/) (2021)

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

- [ACE: A Security Architecture for LLM-Integrated App Systems](https://mlsanity.com/paper/2504.20984/) (2025)
- [LLM-Based Human-Agent Collaboration and Interaction Systems: A Survey](https://mlsanity.com/paper/2505.00753/) (2025)
- [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025)
- [ToolGate: Contract-Grounded and Verified Tool Execution for LLMs](https://mlsanity.com/paper/2601.04688/) (2026)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification](https://mlsanity.com/paper/2510.03469/) (2025)
- [RepV: Safety-Separable Latent Spaces for Scalable Neurosymbolic Plan Verification](https://mlsanity.com/paper/2510.26935/) (2025)
- [Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement](https://mlsanity.com/paper/2608.14590/) (2026)
- [Verifying Memoryless Sequential Decision-making of Large Language Models](https://mlsanity.com/paper/2510.06756/) (2025)
- [GNNVerifier: Graph-based Verifier for LLM Task Planning](https://mlsanity.com/paper/2603.14730/) (2026)
- [LitPivot: Developing Well-Situated Research Ideas Through Dynamic Contextualization and Critique within the Literature Landscape](https://mlsanity.com/paper/2604.02600/) (2026)
- [Meta-Agent: From Task Descriptions to Verified Multi-Agent Systems](https://mlsanity.com/paper/2605.25233/) (2026)
- [Persuasive or Neutral? A Field Experiment on Generative AI in Online Travel Planning](https://mlsanity.com/paper/2509.14259/) (2025)
- [HyPlan: Hybrid Learning-Assisted Planning Under Uncertainty for Safe Autonomous Driving](https://mlsanity.com/paper/2510.07210/) (2025)
- [Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification](https://mlsanity.com/paper/2511.00202/) (2025)
- [Do You Understand How I Feel?: Towards Verified Empathy in Therapy Chatbots](https://mlsanity.com/paper/2601.08477/) (2026)
- [Explorable Proofs: Making Written Proofs Explorable by Grounding Them in Formal Representations](https://mlsanity.com/paper/2604.02598/) (2026)
- [U-Define: Designing User Workflows for Hard and Soft Constraints in LLM-Based Planning](https://mlsanity.com/paper/2605.02765/) (2026)
- [From Tool to Agent: How Worker Needs Reorganize Across the Agentic Roles of Workplace AI](https://mlsanity.com/paper/2605.03078/) (2026)
- [Agentic Cognitive Depth: Operational Criteria for Evaluating LLM Agents](https://mlsanity.com/paper/2610.04168/) (2026)

## Abstract (arXiv)

Automated planning is traditionally the domain of experts, utilized in fields like manufacturing and healthcare with the aid of expert planning tools. Recent advancements in LLMs have made planning more accessible to everyday users due to their potential to assist users with complex planning tasks. However, LLMs face several application challenges within end-user planning, including consistency, accuracy, and user trust issues. This paper introduces VeriPlan, a system that applies formal verification techniques, specifically model checking, to enhance the reliability and flexibility of LLMs for end-user planning. In addition to the LLM planner, VeriPlan includes three additional core features -- a rule translator, flexibility sliders, and a model checker -- that engage users in the verification process. Through a user study (n=12), we evaluate VeriPlan, demonstrating improvements in the perceived quality, usability, and user satisfaction of LLMs. Our work shows the effective integration of formal verification and user-control features with LLMs for end-user planning tasks.