# VeriSafe Agent: Safeguarding Mobile GUI Agent via Logic-based Action Verification

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

## Key facts

- Cited by 22 papers in the map (data through 14 Oct 2026).
- Placed in GUI and mobile agents, one of 16 directions in LLM agents and tool use.
- Builds on 24 of its 51 references that are in the map.
- First posted on arXiv 24 Mar 2025.

## Placed in

- LLM agents and tool use / [GUI and mobile agents](https://mlsanity.com/agents/gui-and-mobile-agents/)

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

- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [FActScore: Fine-grained Atomic Evaluation of Factual Precision in Long Form Text Generation](https://mlsanity.com/paper/2305.14251/) (2023)
- [CogAgent: A Visual Language Model for GUI Agents](https://mlsanity.com/paper/2312.08914/) (2023)
- [Retrieval Augmentation Reduces Hallucination in Conversation](https://mlsanity.com/paper/2104.07567/) (2021)
- [GPT-4V(ision) is a Generalist Web Agent, if Grounded](https://mlsanity.com/paper/2401.01614/) (2024)
- [AppAgent: Multimodal Agents as Smartphone Users](https://mlsanity.com/paper/2312.13771/) (2023)
- [Chain-of-Verification Reduces Hallucination in Large Language Models](https://mlsanity.com/paper/2309.11495/) (2023)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Mobile-Agent-v2: Mobile Device Operation Assistant with Effective Navigation via Multi-Agent Collaboration](https://mlsanity.com/paper/2406.01014/) (2024)
- [Entity-level Factual Consistency of Abstractive Text Summarization](https://mlsanity.com/paper/2102.09130/) (2021)
- [GUI Agents with Foundation Models: A Comprehensive Survey](https://mlsanity.com/paper/2411.04890/) (2024)
- [Assessing The Factual Accuracy of Generated Text](https://mlsanity.com/paper/1905.13322/) (2019)
- [Plug in the Safety Chip: Enforcing Constraints for LLM-driven Robot Agents](https://mlsanity.com/paper/2309.09919/) (2023)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Understanding the Weakness of Large Language Model Agents within a Complex Android Environment](https://mlsanity.com/paper/2402.06596/) (2024)
- [Explore, Select, Derive, and Recall: Augmenting LLM with Human-like Memory for Mobile Task Automation](https://mlsanity.com/paper/2312.03003/) (2023)
- [Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments](https://mlsanity.com/paper/2302.11649/) (2023)
- [Ever: Mitigating Hallucination in Large Language Models through Real-Time Verification and Rectification](https://mlsanity.com/paper/2311.09114/) (2023)
- [LlamaTouch: A Faithful and Scalable Testbed for Mobile UI Task Automation](https://mlsanity.com/paper/2404.16054/) (2024)
- [AutoDroid-V2: Boosting SLM-based GUI Agents via Code Generation](https://mlsanity.com/paper/2412.18116/) (2024)
- [SELP: Generating Safe and Efficient Task Plans for Robot Agents with Large Language Models](https://mlsanity.com/paper/2409.19471/) (2024)
- [Mitigating Hallucinations in Large Language Models via Self-Refinement-Enhanced Knowledge Retrieval](https://mlsanity.com/paper/2405.06545/) (2024)
- [SafePlan: Leveraging Formal Logic and Chain-of-Thought Reasoning for Enhanced Safety in LLM-based Robotic Task Planning](https://mlsanity.com/paper/2503.06892/) (2025)
- [RustHorn: CHC-based Verification for Rust Programs (full version)](https://mlsanity.com/paper/2002.09002/) (2020)

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

- [Towards Trustworthy GUI Agents: A Survey](https://mlsanity.com/paper/2503.23434/) (2025)
- [Phi-Ground Tech Report: Advancing Perception in GUI Grounding](https://mlsanity.com/paper/2507.23779/) (2025)
- [OS-Sentinel: Towards Safety-Enhanced Mobile GUI Agents via Hybrid Validation in Realistic Workflows](https://mlsanity.com/paper/2510.24411/) (2025)
- [A Framework for Formalizing LLM Agent Security](https://mlsanity.com/paper/2603.19469/) (2026)
- [MAS-Bench: A Unified Benchmark for Shortcut-Augmented Hybrid Mobile GUI Agents](https://mlsanity.com/paper/2509.06477/) (2025)
- [GEM: Gaussian Embedding Modeling for Out-of-Distribution Detection in GUI Agents](https://mlsanity.com/paper/2505.12842/) (2025)
- [CORA: Conformal Risk-Controlled Agents for Safeguarded Mobile GUI Automation](https://mlsanity.com/paper/2604.09155/) (2026)
- [Mobile GUI Agents under Real-world Threats: Are We There Yet?](https://mlsanity.com/paper/2507.04227/) (2025)
- [Options, Not Clicks: Lattice Refinement for Consent-Driven MCP Authorization](https://mlsanity.com/paper/2605.11360/) (2026)
- [Blind Gods and Broken Screens: Architecting a Secure, Intent-Centric Mobile Agent Operating System](https://mlsanity.com/paper/2602.10915/) (2026)
- [How Agents Ask for Permission: User Permissions for AI Agents, from Interfaces to Enforcement](https://mlsanity.com/paper/2607.13718/) (2026)
- [MobiBench: Multi-Branch, Modular Benchmark for Mobile GUI Agents](https://mlsanity.com/paper/2512.12634/) (2025)
- [SeerGuard: A Safety Framework for Mobile GUI Agents via World Model Prediction](https://mlsanity.com/paper/2607.15550/) (2026)
- [AgentLens: Adaptive Visual Modalities for Human-Agent Interaction in Mobile GUI Agents](https://mlsanity.com/paper/2604.20279/) (2026)
- [OpenAgentFlow: Enabling System-Wide Safety Boundaries for Heterogeneous AI Agent Fleets](https://mlsanity.com/paper/2609.00015/) (2026)
- [Securing Computer-Use Agents: A Unified Architecture-Lifecycle Framework for Deployment-Grounded Reliability](https://mlsanity.com/paper/2605.07110/) (2026)
- [Efficient GUI Agents: A Systems Survey of Observation, Memory, Action, and Runtime Optimization](https://mlsanity.com/paper/2609.02309/) (2026)
- [MATE: Policy-Aware Security Auditing for Mobile Agents via Synthesis-Driven Trajectory Learning](https://mlsanity.com/paper/2609.22724/) (2026)
- [PastForward: Faster On-Device GUI Agents via Computational Experience Reuse](https://mlsanity.com/paper/2609.32166/) (2026)
- [What Can Component-Replacement Evidence Establish? A Critical Scoping Review of Local Decisions in LLM Agents](https://mlsanity.com/paper/2609.39989/) (2026)
- [VEPA: Verified Evolving Formal Policy for Lifelong LLM Agent Guardrails](https://mlsanity.com/paper/2610.12813/) (2026)
- [Task-State Governance: A Virtual Machine for Verifiable and Recoverable GUI Agent Execution](https://mlsanity.com/paper/2610.20100/) (2026)

## Abstract (arXiv)

Large Foundation Models (LFMs) have unlocked new possibilities in human-computer interaction, particularly with the rise of mobile Graphical User Interface (GUI) Agents capable of interacting with mobile GUIs. These agents allow users to automate complex mobile tasks through simple natural language instructions. However, the inherent probabilistic nature of LFMs, coupled with the ambiguity and context-dependence of mobile tasks, makes LFM-based automation unreliable and prone to errors. To address this critical challenge, we introduce VeriSafe Agent (VSA): a formal verification system that serves as a logically grounded safeguard for Mobile GUI Agents. VSA deterministically ensures that an agent's actions strictly align with user intent before executing the action. At its core, VSA introduces a novel autoformalization technique that translates natural language user instructions into a formally verifiable specification. This enables runtime, rule-based verification of agent's actions, detecting erroneous actions even before they take effect. To the best of our knowledge, VSA is the first attempt to bring the rigor of formal verification to GUI agents, bridging the gap between LFM-driven actions and formal software verification. We implement VSA using off-the-shelf LFM services (GPT-4o) and evaluate its performance on 300 user instructions across 18 widely used mobile apps. The results demonstrate that VSA achieves 94.33%-98.33% accuracy in verifying agent actions, outperforming existing LFM-based verification methods by 30.00%-16.33%, and increases the GUI agent's task completion rate by 90%-130%.