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

Agents that operate phones decide for themselves when a task is done, and that decision is where they fail: they stop with sub-goals unfinished, give up on facts that are hard to find, and report values they never saw. Proof-carrying operation (PCO) takes the decision away from the model. The agent compiles the goal into typed obligations (state changes to make, facts to report, results to derive, conditions to resolve) and must close each with the value it claims and the recorded screen that shows it. A deterministic checker with no app knowledge accepts a claim only if the cited screen's accessibility tree contains it, challenges every claim of absence, refuses to end the episode while obligations are open, and completes the final answer only from claims it accepted. Every run leaves a certificate. On iOSWorld, PCO raises performance from 77 to 90 of 133 tasks fully passed (57.9% to 67.7%) and the mean rubric score from 0.857 to 0.885 (exact McNemar p = 0.007); a replicate run lands at 91/133 (0.890), without app-specific knowledge. The gain sits in multi-app tasks (25 to 36 of 60) and in criteria about actions on the device, not in answer wording. An ablation without resumption rounds keeps most of the gain (86/133), which locates the effect in the obligation ledger the agent must keep rather than in being sent back. We audit the checker itself: of 60 randomly sampled accepted claims, 48 sound, 5 editor-state, 4 weak and 3 mismatched; every ledger, screen and certificate is published so that the audit can be repeated. On AndroidWorld, near its ceiling, the same operator averages 95.1% pass@1 over three suite seeds with no app knowledge. Code: https://github.com/verdikt-ai/verdikt. Every run, frame and statistic: https://verdikt-ai.github.io/verdikt/