VeriAct: A Certificate Veto Costs Coverage on Unverifiable Actions, Not on Failing Ones

A computer-use agent that must act at every step inherits the full error rate of its model. We study a training-free gate between a frozen GUI agent's policy and the environment that decides, for each proposed action, whether to ACT, ABSTAIN, or ASK a human. The gate fuses three uncertainty signals (self-consistency over equivalence clusters of the sampled actions, a frozen pre-operative critic, and model confidence), applies a machine-checkable static executability certificate over the accessibility tree or DOM as a veto, and turns the fused score into an ACT threshold whose executed-step error is bounded by simultaneous Bentkus bounds over a fixed threshold family, fitted on independent episode anchors. On AndroidControl and Mind2Web's three splits with two frozen 7B backbones the gate attains an 8.9% mean AURC reduction over the best of its own component signals used alone, with no external calibrated gate compared, and the pooled certificate keeps executed risk at or below the target at every non-vacuous setting. The main finding concerns the veto. 72.9% / 66.1% of what it withholds on AndroidControl and on Mind2Web carries no applicable check at all rather than a check that fails. What the veto buys is that no proposal violating the static checker's preconditions executes, and withholding only that checker-failing slice keeps the certificate and recovers certified coverage on both benchmarks, most of it on AndroidControl. The certified level does not transfer across splits although the ordering of policies does, and all claims are offline and step-level, with no live execution.