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

• Post-action verification cannot prevent irreversible actions, motivating VSA’s pre-action design for operations such as payments and messages.Source: §1 · p. 2
• Repeated LFM-based validation can accumulate errors across action sequences, degrading overall system accuracy.Source: §1 · p. 2
• VSA translates natural-language instructions into formal specifications and deterministically verifies proposed GUI actions before execution.Its autoformalization approach bridges probabilistic agent actions and logic-based safety.Source: §1 · p. 2
• Up to 98.33% verification accuracy, with 1.3% false positives and 0.3% false negatives, was achieved using GPT-4o and about 437 additional lines of code per app.Source: §1 · p. 2
• 130% task-completion improvement over reflection agents demonstrates the benefit of VSA’s structured feedback, while reflection agents corrected no tasks.The evaluation used 300 instructions across 18 mobile applications.Source: §1 · pp. 2–3

• Pre-action reflection can abort errors before execution but often has low accuracy because it must predict an action’s outcome.Source: §2 · p. 3
• Post-action reflection can assess executed actions more concretely but cannot prevent irreversible operations such as payments or messages.Source: §2 · p. 3
• VSA provides reliable pre-action verification based on logic-based deduction rather than probabilistic reasoning.Source: §2 · p. 3
• Formal software verification provides established methods for checking runtime behavior against mathematical specifications.Source: §2 · p. 3

3 VeriSafe Agent (VSA): Overview

• VSA intercepts proposed UI actions, verifies their anticipated state transitions against logical rules, and passes or rejects them with corrective feedback.Source: §3 · p. 3, §3.2 · pp. 4–5

3.1 Challenges

• The DSL and developer library jointly represent user intent and application behavior as logically verifiable rules, states, and transitions.Source: §3.1 · pp. 3–4
• Self-corrective encoding refines natural-language translations through syntactic and semantic checks, while two-tier verification adjusts intensity to action significance.Source: §3.1 · p. 4
• Structured feedback identifies precise unmet predicates or constraints instead of merely flagging an action as incorrect.Source: §3.1 · p. 4

3.2 System Workflow

• The workflow continues until the task reaches a final state or the agent terminates despite feedback, causing task failure.Source: §3.2 · p. 5

4.1 Design of Domain-Specific Language

• Horn-clause rules decompose instructions into predicates and objectives, enabling incremental verification of constraints, execution flows, and conditional branches.Source: §4.1.1 · p. 5, §4.1 · p. 5

4.1.1 Syntax and Semantics.

• The restaurant example encodes reservation conditions, successful completion, and unavailability before 19:00 as separate rules with precedence relationships.Source: §4.1.2 · p. 6

4.1.2 Running Example.

• Runtime evaluation updates initially undefined variables through GUI-induced state transitions and re-evaluates associated constraints.Source: §4.1.2 · p. 6

4.2 Developer Library

• Developers define application states and transitions through the library, gaining precise rule-based verification at the cost of additional effort.Source: §4.2 · p. 6

4.2.2 Pre-action State Update Triggers.

• Pre-action triggers return expected state updates before execution, preventing violating irreversible actions and enabling retries without reverting prior effects.Source: §4.2.2 · p. 6
• Developer-controlled verification granularity focuses checks on meaningful state changes rather than every preparatory atomic action.Source: §4.2.2 · p. 7

4.2.3 Post-action State Update Triggers.

• Post-action updates handle network delays, asynchronous operations, errors, and dynamically determined content after outcomes become known.Source: §4.2.3 · p. 7

5.1.1 Self-Corrective Encoding.

• Self-corrective encoding checks generated specifications through DSL syntax and type validation, then semantic comparison between decoded specifications and the original instruction.Syntax errors produce structured feedback, while a checker LFM identifies semantic discrepancies for correction.Source: §5.1.1 · p. 7

5.1.2 Experience-driven Encoding.

• Experience-driven encoding caches successful specifications and prioritizes previously useful predicates to reduce the encoder’s search space and improve consistency.Shared rules across instructions for the same application make prior encodings reusable.Source: §5.1.2 · p. 8

5.2 Intent Verifier

• At each state update, VSA updates constraint variables and re-evaluates affected predicates, while predicate-level verification detects potential deviations without treating every intermediate failure as definitive.A failed predicate can reflect a necessary intermediate step, so VSA reverts the update and issues soft feedback.Source: §5.2 · p. 8
• At irreversible or critical checkpoints, rule-level verification requires all predicates for the targeted objective to be satisfied before permitting the action.Unsatisfied conditions trigger hard feedback and block the action.Source: §5.2 · p. 8
• The verifier uses a two-tiered strategy that guides agents toward objectives while ensuring safer execution of high-risk actions.Predicate-level checks are advisory, whereas rule-level checks enforce critical preconditions.Source: §5.2 · p. 8

Roadmap Feedback

• Roadmap feedback translates each specification rule into natural-language guidance describing required predicates, current progress, and next objectives.The specification therefore provides guidance beyond ambiguous action histories or abstract planning.Source: §6 · pp. 8–9

Predicate-level Soft Feedback

• Predicate-level soft feedback describes the desired state after a failed predicate, but permits repetition because the deviation may be an intermediate step.This feedback warns the agent without strictly prohibiting non-critical actions.Source: §6 · p. 9

Rule-level Hard Feedback

• Rule-level hard feedback lists all unfulfilled predicates for critical actions and blocks execution until every required condition is satisfied.Repeating the same action after hard feedback does not bypass the requirement.Source: §6 · p. 9

Structured Feedback

• Structured deterministic feedback guides agents toward correct task completion and outperforms existing reflection-based methods.The mechanism grounds guidance in formal logic rather than ambiguous or potentially incorrect generated feedback.Source: §6 · p. 9

Implementation

• VSA uses Python and an off-the-shelf GPT-4o Intent Encoder as a modular component that integrates with existing GUI agents without changing their architecture.The implementation is designed to sit alongside the underlying agent.Source: §7 · p. 9

Developer Library Guidelines

• Developer guidance warns that fine-grained predicates can increase false positives, whereas coarse-grained predicates can create loopholes and increase false negatives.The recommended process begins fine-grained and iteratively refines predicates to reduce false positives while considering false-negative severity.Source: §7 · p. 9

String Similarity

• String equivalence is computed with text-embedding-3-small cosine similarity, using a 0.7 threshold for determining equivalence.The threshold is based on empirical studies.Source: §7 · p. 9

8.1 Dataset

• The evaluation uses 300 instructions split equally between Correct and deliberately mismatched Wrong execution paths, including Challenge tasks with longer action sequences averaging 19.16 steps.Of 150 unique instructions, 125 were sampled from LlamaTouch and 25 were newly created for the Challenge dataset, spanning 9 applications.Source: §8.1 · pp. 9–10

8.2 Verification Accuracy

• VSA consistently outperforms reflection-based methods across Accuracy, Precision, Recall, and F1, achieving near-perfect accuracy on LlamaTouch.Post-action reflection performs better than pre-action reflection on simple LlamaTouch tasks, but its advantage diminishes on longer, more complex Challenge instructions.Source: §8.2 · p. 10
• VSA maintains high pre-action verification across datasets because it encodes specifications once and performs subsequent checks with rule-based logic.VSA-Warm achieves near-perfect LlamaTouch results and significantly outperforms baselines on Challenge, while predicate memory improves translation accuracy by reducing missing and superfluous predicates.Source: §8.2 · pp. 10–11
• Majority voting raises Challenge accuracy to 96% for VSA-Cold and 100% for VSA-Warm, although repeated verification adds latency and cost.The benefit is especially pronounced for VSA because stochastic predicate decisions can otherwise flip individual verification outcomes.Source: §8.2 · p. 11

8.3 Effectiveness of Feedback Generation

• VSA corrected 9 of 15 failed tasks with VSA-Cold and 13 of 15 with VSA-Warm, whereas neither reflection method corrected previously failed tasks.Its deterministic feedback identifies unmet predicates and can prevent repeated actions, although unconventional interfaces limited two VSA-Warm corrections.Source: §8.3 · pp. 11–12
• VSA can prematurely terminate a task after a false positive, and constructing predicate memory remains outside this paper’s scope.The evaluation reports practical benefits, but the authors identify false positives and memory construction as relevant boundaries for deployment.Source: §8.2 · p. 10, §8.3 · p. 12

8.4 Latency and Cost

• VSA overhead remains lower than reflection methods across task lengths because only specification encoding uses an LFM and later checks use rule-based logic.Reflection overhead scales as O(N) with action count, while VSA is near constant apart from a slight increase for longer specifications.Source: §8.4 · p. 12

8.5 Developer Burden

• Each application required an estimated 58.77 predicates, or approximately 437 lines of code, with 1,058 predicates defined across 18 applications.Predicate granularity, templating, and alignment with existing application state logic can reduce the practical burden, while the investment is intended to support ongoing error prevention.Source: §8.5 · pp. 12–13

10 Related Work

• VSA uses a domain-specific language and developer library to capture the semantics of ambiguous mobile GUI actions without relying on ground-truth actions.Source: §9 · p. 13
• Prior formal-logic safety systems target predefined environments such as robot navigation or indoor planning, whereas VSA targets the diverse environments represented by mobile apps.Source: §9 · p. 13

Piggybacking on App Development Frameworks

• Developer-defined states can potentially reuse state management in React Native, Jetpack Compose, and SwiftUI to reduce VSA adoption overhead.Source: §10 · p. 13

Automated State Definition via LFM

• LFM-based state-definition automation could reduce developer effort but may compromise reliability, so the current approach retains developer-defined states for precision.Source: §10 · p. 13

Automated Predicate Memory Construction

• Predicate memory currently depends on successful VSA-Cold task completion, while direct user feedback could provide ground truth and accelerate memory construction.Source: §10 · p. 13

Interactive Feedback & Dual Verification

• Human confirmation is proposed for repeated rule violations and critical operations because VSA cannot guarantee 100% safety, including protection against false negatives.Source: §10 · p. 13

11 Conclusion

• VSA is introduced as a logic-based verification system designed to improve the safety and reliability of Mobile GUI Agents.Source: §11 · p. 13
• Logic-driven verification can safeguard GUI agents against uncertainties inherent in LFM-based task automation.Source: §11 · p. 14