From Formal Verification to Agents: A Method-Transfer Audit of "False Completion" in AI Agent Harnesses

An agent that reports Task Completed has produced a claim, not an observation. In 2026 measure-ments this is not a corner case: 65.4% of one industry evaluation’s agent failures ended in confidentfalse completion [1], and a separate 2026 study across two benchmarks found that no LLM-judgeconfiguration it tested stayed above AUROC 0.65 at separating false successes from real ones [2].The failure is therefore not only common but resistant to the obvious remedy — asking a secondmodel to look — because that remedy is still reading the agent’s own account.Audit methods are usually presented as though they were about their subject matter. They arejust as much about their medium — and that becomes visible when the medium changes. Thispaper takes an audit method built for a formal-verification corpus and asks what survives when itis transferred to AI agent harnesses, a setting that differs on four axes: it is stochastic rather thandeterministic, its inputs are private rather than public, it has no reference implementation, and itsobservables are the system’s own narration.We give a transfer analysis instrument by instrument. Three instruments move. The falsifiabilitycondition — a property no mutant can kill is a decoration — carries over unchanged, because itis a statement about signals, not about specifications. Same-origin detection moves but degrades:in the source system it was a computation (re-derive both artifacts from public bytes and compare);in the target it is only a search for a shared coordinate. Mutation moves and strengthens, becausein the target it needs no correct reference — a condition that must fail can be synthesised. Recom-putation is lost entirely, and we argue this single loss is the load-bearing fact: it is what forcesthe metric denominator from a workload to a published probe suite, and what makes INVALID themodal verdict rather than an edge case.Applied to the target, the transferred method yields a four-mode taxonomy of false completion gen-erated from one condition (a signal losing its carrier, moment, referent, or range), an audit proce-dure over evidence origin, execution witness and mutation probing, a four-valued verdict alphabet,and three metrics with probe-suite denominators.We are explicit that the mechanism is not our discovery: that an agent derives its check from thesame reading as its solution — so the check inherits the misreading and passes — has been statedin prose by 2026 industry evaluation work [1], and that LLM judges are weak at this is now mea-sured [2] (no configuration above AUROC 0.65). Our claim is about the transfer: which instrumentssurvive, what they cost, and which conclusions become unsupportable on arrival. We claim mech-anism, not prevalence.