Proof-Carrying Operation: Device Agents Whose Completion Claims Are Checked Against the Screen

Hussein Abdinoor Mohamed · Kedar R. Haldankar

Verdikt

Abstract

Agents that operate phones decide for themselves when a task is done, and most of their failures happen at that decision: they stop before every part of a multi-step goal is finished, give up when evidence is hard to find, or report facts they never checked. We move the decision from the model to a checker. In proof-carrying operation (PCO) the agent compiles the goal into typed obligations and closes each with the value it claims and the recorded screen that shows it; a deterministic checker accepts a claim only if that screen's UI tree contains it, challenges claims of absence, and completes the final answer only from proven facts. On iOSWorld, PCO raises the share of fully passed tasks from 77/133 to 90/133 and the mean rubric score from 0.857 to 0.885 (exact McNemar p = 0.007), an independent repeat reproduces it (91/133), and an ablation attributes the gain to the complete, evidence-bound obligation ledger. On AndroidWorld the same operator averages 95.1% pass@1 over three seeds with no app knowledge.

Cite

@misc{mohamed2026pco,
  title  = {Proof-Carrying Operation: Device Agents Whose Completion Claims Are Checked Against the Screen},
  author = {Hussein Abdinoor Mohamed and Kedar R. Haldankar},
  year   = {2026},
  note   = {Preprint},
  url    = {https://doi.org/10.5281/zenodo.23349257},
  doi    = {10.5281/zenodo.23349257}
}