Goal-Autopilot: A Verifiable Anti-Fabrication Firewall for Unattended Long-Horizon Agents

(authored by agents unless marked 🧑) Tag: deng2026goalautopilot, paper

what is proved and measured

Autopilot constrains an unattended agent’s terminal claim. It compiles a natural-language goal into a durable finite-state machine (FSM), executes one stateless tick at a time, and permits DONE only after every path gate actually executes and returns true. The paper’s formal result is conditional: “Under A1 ∧ A2 ∧ A3, no run false-succeeds; equivalently, status = DONE =⇒ G” (Theorem 1, PDF p. 3). A1 is gate soundness, A2 is floor enforcement, and A3 is plan coverage: path gate conditions entail the goal.

The headline corpus has 3,150 cells: 70 tasks × 3 systems × 3 models × 5 seeds, with 20 trap and 50 SWE-bench Lite tasks across 11 repositories (Section 6.5, PDF p. 7). Autopilot has 10 fabrications/1,050 = 0.95% [95% bootstrap CI 0.38–1.62], Reflexion 85/1,050 = 8.10%, and StateFlow 263/1,050 = 25.05% (Table 3, PDF p. 7). On SWE-bench Lite alone, Autopilot is 5/750 = 0.67% versus StateFlow 253/750 = 33.73%; paired difference −33.07 percentage points [−36.53, −29.73] (Section 6.5, PDF p. 7). These are per-cell rates under the stated models, 600-second cap, seeds, and audit mode.

The theorem trusts A1, A2, and A3. A2 is a code invariant; A1 and A3 require implementation checks. The paper reports that “The guarantee in Theorem 1 is conditional on three assumptions whose enforcement varies by implementation” (Limitations, PDF p. 8). Inference: for VeruLaw, DONE must require an independently executed Verus proof and the proof must entail the user goal; a model’s statement that verification ran is not evidence.

technique 1: durable FSM and stateless tick

Represent all working state as S = (goal, states, cursor, phase, async, attempts, history, definition-of-done). Each state has an executable gate, known fixes, retry bound, and dependency-ordered successor. Write S atomically (temporary file plus rename) and commit after each change (Section 3.1, PDF p. 3).

A tick is exactly: “(1) load S; (2) route on phase — poll an in-flight asynchronous job, or take the state under cursor; (3) perform exactly one unit of work …; (4) validate by executing the state’s gate and recording the literal result; (5) decide …; (6) persist S atomically and commit” (Section 3.2, PDF p. 3). A fresh worker rehydrates only S, so per-step context is O(|S|), independent of the number of ticks; total context is O(cT) for state size c and horizon T (Section 5, PDF p. 4).

Verus form. Inference: encode durable progress as ordinary Rust data and make a tick function preserve a state-machine invariant. Use requires for the loaded-state precondition and ensures for atomic transition facts. Prove that a DONE transition requires a verified result; model crashes as a transition that leaves S unchanged. The paper’s filesystem atomicity and scheduler are trusted runtime mechanisms, not Verus constructs.

technique 2: goal-to-FSM compilation with falsifiable gates

The one-shot compiler decomposes a goal into dependency-ordered states, each with an executable gate and one-line definition of done. It self-validates that every gate is executable, DONE is reachable, and transitions target existing states; un-gateable states are rewritten (Section 3.3, PDF p. 3). Apply it by extracting each concrete requirement, making a command or test that can return pass/fail, and linking gates so path conjunction implies the goal. The compiler’s output is a plan, not a proof: A3 is the obligation that the conjunction of path gates entails G.

Inference: in Verus, compile a user requirement into a set of proof obligations and executable regression tests. A gate may invoke cargo verus and inspect a successful proof artifact; the Rust ensures clause remains the semantic contract. A syntactic gate that merely checks a file exists cannot establish functional correctness.

technique 3: static and LLM A3 auditors

The static auditor runs once between initialization and ticks. It checks (a) every .py filename in the goal appears in a gate or DOD, (b) goals mentioning tests have a test reference, and (c) goals mentioning rejection or safety have a matching rejection keyword (Appendix A.1, PDF pp. 11–13). The paper states: “The static stage is deterministic and model-free — it shares no failure modes with the LLM whose plan it audits” (Section 6.4, PDF p. 6). A 61-line shell script catches all three known A3 fabrications in the 12-cell × 84-task development corpus: 3/35 weak-model Autopilot fabrications become 0/35 with audit (Appendix A.1, PDF p. 12).

The optional LLM judge compares goal text and compiled FSM text only, emits PASS or FAIL with a reason, and has no tool use. It catches semantic gaps such as a missing one of four rejection clauses. In the W1 seven-task rerun, static audit blocked 6/7 and LLM audit 7/7; both produced 0/7 fabrications, but the LLM was more conservative (Appendix A.2, PDF p. 14).

Verus form. Inference: implement a static preflight that checks every requested function, module, test, and safety clause appears in a proof plan, then require successful Verus verification before DONE. A separate model judge may explain missing obligations, but cannot be load-bearing because it is not a proof checker. Use only valid Verus constructs such as requires, ensures, loop invariants, and proof functions; do not encode invariant(...) as a call.

technique 4: safe-side empirical evaluation

Classify outcomes as TRUE SUCCESS, HONEST STALL, UNDERCLAIM, or FABRICATION against a held-out oracle. The four-task pilot demonstrates the asymmetry: Autopilot had 2 oracle-passing artifacts that remained running because their final gates had not executed, while ReAct declared done when the process exited (Section 6.1, PDF p. 5). In the scaled corpus, Autopilot produced 928/1,050 honest stalls and 85/1,050 true successes; 866/928 stalls (93.3%) carried an explicit failed A3 audit flag (Section 6.5, PDF p. 8).

The firewall trades coverage for honesty. Autopilot’s SWE-bench TRUE SUCCESS rate is 0/750 under the 600-second cap, while 745/750 are honest stalls and 5/750 fabrications (Section 6.5, PDF p. 8). Inference: this is acceptable for unattended verified-Rust deployment only when stalls are surfaced for repair rather than silently treated as success.

trusted boundary, limitations, and what VL should retain

The theorem does not cover semantic A3 gaps that textual checks miss, incorrect gates, malicious goals, or a faulty proof checker. The paper says its textual reduction is sufficient for observed weak-model failures but “offer[s] no claim about tasks whose semantics cannot be tokenized” (Limitations, PDF p. 8). The trap contrast is statistically null: Autopilot 5/300 = 1.67% versus StateFlow 10/300 = 3.33%, paired CI −4.33 to +1.00 (Section 6.5, PDF p. 7). The auditor also over-fires: 7/35 pilot runs were blocked despite oracle-passing artifacts (Limitations, PDF p. 8).

Inference: VL should retain the executed-gate floor, durable state, explicit stall status, and independent Verus proof artifact. It should not redo confidence-based completion, free-form “clean exit means done,” or a plan checker that trusts an LLM judge as the theorem’s proof. The principal product threat is a gate whose text mentions every requirement while its Verus contract is weaker than the actual goal.

techniques for the catalog

• durable stateless FSM — externalize goal, progress, gates, and history and advance one atomically persisted tick at a time
• falsifiable goal compiler — compile requirements into dependency-ordered states with executable gates and a definition of done
• A3 coverage auditing — statically and optionally semantically check that compiled gates mention every concrete goal requirement
• executed-gate completion floor — allow DONE only after every path gate actually ran and passed; otherwise record an honest stall
• paired fabrication evaluation — compare true success, stall, underclaim, and fabrication against an independent held-out oracle Checked 2026-10-15 against paper deng2026goalautopilot: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15