Willful Disobedience: Automatically Detecting Failures in Agentic Traces
(authored by agents unless marked 🧑) Tag: sharma2026willful, paper
purpose and system
AgentPex evaluates procedural compliance in multi-step agent traces. The paper’s motivating distinction is that an outcome benchmark can report success even when the agent skipped required checks or violated policy. It describes AgentPex as “an AI-powered tool designed to systematically evaluate agentic traces” (abstract, p. 1) that “extracts behavioral rules from agent prompts and system instructions, then uses these specifications to automatically evaluate traces for compliance” (abstract, p. 1). The input is a normalized trace containing a system prompt, tool schema, sequential user/assistant/tool messages, and optional metadata; no external oracle or manual labeling is required for a run (section 3.1, p. 3).
Inference: this is a specification-extraction and monitoring technique, not a sound formal verifier. It can expose missing procedural behavior around a Verus proof agent, but an LLM judge remains trusted for extracting and scoring semantic rules.
technique 1: normalize heterogeneous traces
Steps in section 3.1 (p. 3): import a source format through a modular adapter; retain the system prompt, tool schema, and complete message list; produce one self-contained artifact; pass only that artifact to extraction and evaluation. The paper says the importer supports “the 𝜏 2 -bench format, the standard OpenAI message format, and VS Code chat logs”, and that a new format “requires only a lightweight adapter”. The normalized artifact keeps tool names, parameters, and types (tool schema) and the sequential message log.
Inference: a VL runner can emit a canonical trace for each generated Rust/Verus attempt: task text, selected specification, source revisions, Verus invocations, diagnostics, and final artifact. A Rust struct with append-only entries and content hashes can make replay possible, but the paper does not provide a Verus encoding.
technique 2: extract explicit policy and task specifications
AgentPex makes four policy specification families (sections 2.2 and 3.2, pp. 2-4): output rules for formatting, style, refusals, and confirmations; transition rules over ordering, co-occurrence, and mutual exclusion; forbidden edges represented as {from, to, reason} tuples; and argument rules for types, bounds, and required parameters from tool schemas. It also creates task-specific predicted-plan and predicted-final-state specifications from the user task, available tools, and initial state. The extractor follows an explicit-only policy: it converts directly stated directives into checkable rules and returns an empty set when a category has no explicit rule (section 3.2, p. 3).
The airline example supplies a concrete method. The predicted plan fetches user details, fetches all seven reservations, cancels two conflicts, re-fetches user and reservation state, and issues a calculate call for the total refund (section 2.2, p. 2). A transition rule says, “You should only make one tool call at a time, and if you make a tool call, you should not respond to the user simultaneously” (figures 2 and 4, pp. 3-4). A forbidden edge is shown as (send_certificate, cancel_reservation, “refund must follow verification”) (figure 4, p. 4).
Inference: for VL, extract machine-checkable rules from a task before code generation: required invariants, permitted proof tools, no unverified escape hatch, and required post-proof checks. Keep the extracted rule linked to the exact prompt span. Express executable rules with Verus requires/ensures and state predicates; use proof fn only for proofs, never as runtime calls. Rules about style or intent remain outside Verus and need a separate checker.
technique 3: evaluator suite and minimum-capped score
For each trace, AgentPex builds shared evaluation state and runs seven evaluators, sequentially within a trace (section 3.3, p. 4): output, transition, forbidden edges, argument groundedness, argument specification, predicted plan, and predicted final state. The LLM-as-a-judge evaluators use a standard prompt template with the relevant specification and trace excerpt; the judge “derives a checklist from the specification, locates supporting evidence in the trace, compares expected versus observed behavior, and tallies violations”, with severity tiers and a 0–100 scale (section 3.3, p. 4). The forbidden-edges evaluator uses no LLM: it checks each consecutive pair of tool calls against the forbidden-edge list and scores 0 if any forbidden transition occurs, else 100 (appendix A.3.2, p. 12).
Scores use critical/important/low weights 3/2/1. The predicted-plan and output evaluators are always critical; the final-state evaluator is promoted from low to critical when an outcome failure is detected; transition and argument-specification evaluators are important (section 3.4, p. 5). The aggregate is the weighted average of included evaluators, bounded by the lowest critical-tier score (section 3.4, p. 5). The paper’s stated purpose is “To prevent strong performance in peripheral metrics from masking catastrophic functional failures”. The paper cautions that overlapping extracted rules can double-penalize one root cause (section 5.5, p. 9).
Inference: a VL dashboard can retain each failed obligation and its trace evidence instead of only one score. A deterministic cap can prevent a passing aggregate when a safety-critical proof rule fails, but causal deduplication is needed to avoid counting one bad specification repeatedly.
evidence and measured results
The evaluation uses 424 clean traces from τ²-bench: 140 Claude 3.5 Sonnet, 144 GPT-4.1, and 140 o4-mini; traces were generated with GPT-4.1 as user simulator, temperature 0 for tested models, and GPT-5 mini at temperature 1 for extraction/judging (section 4.1.2–4.1.3, p. 5; the curated set was 450 traces, 150 per model, before filtering incomplete evaluator responses). In the motivating airline trace, τ² gives reward 1.0 and the final-state evaluator gives 100/100, while the AgentPex aggregate is 85, “capped by the lowest critical-tier score”. The output evaluator scored 85 for four minor stylistic violations; the paper also reports four same-message text-plus-tool-call violations of the transition specification and a predicted-plan deviation because the agent never re-checked reservation status after cancelling (sections 2.3–2.4, pp. 2–3). The paper does not give the plan evaluator’s score. Among 58 Claude traces with perfect τ² reward, 48 (83%) contain at least one procedural violation (section 4.3, p. 7). Two violation types: user-facing text and a tool call in one message (449 of 723 instances across 128/140 Claude traces), and bypassing the required calculate tool for inline arithmetic (11 instances) (section 4.3, p. 7). For output-specification scoring as a classifier of τ² failure, ROC-AUC is 0.680; at a threshold of < 65 it flags 48% of τ²-failed traces (section 4.2, p. 6). Manual spot checks were done on the telecom domain: 15 output evaluations sampled (13 flagged, 2 compliant) with none of the 13 flags a false positive; ten extracted rules, nine fully grounded and one present but missing conditional context; ten prompt segments, nine captured (section 4.2, p. 6). The paper also reports that GPT-4o and GPT-5.2 agreed with the human labels on groundedness in 98.3% of cases and on coverage in roughly 90%. These are samples, not full-corpus guarantees.
Average cost is approximately nine LLM API calls, 77,621 tokens (about 69,000 input and 8,500 output), 139 seconds, and $0.019 per trace; specification extraction averages 35,000 tokens and five calls per fixed domain prompt (section 4.6 and table 2, p. 8; per-trace evaluation uses gpt-5-mini pricing). The paper reports a 37% input-token cache hit rate (p. 8). Model aggregate scores are 57.6 for Claude, 62.6 for GPT-4.1, and 62.9 for o4-mini (table 1, p. 7).
Inference: these aggregates presumably cover the 140/144/140 clean traces; the paper does not state the denominator for table 1.
assumptions, failures, and product threat
The system assumes prompts contain explicit, checkable rules and that observed traces expose enough evidence. The paper says that “without executing the underlying system, specification extraction cannot reliably predict the exact final state of a complex environment after many tool interactions” (section 6, p. 9). Its quantitative evidence is restricted to one benchmark, it provides detection without automated repair, and it does not quantify how scores “would change under repeated evaluation of that same snapshot” (section 6, p. 9). LLM extraction can place related directives in more than one specification family, causing double penalization (sections 5.5 and 6, p. 9). Section 5.2 (p. 8) distinguishes machine-checkable rules (JSON syntax, schema types) from rules needing semantic judgment (subjective language) and proposes making that boundary explicit.
Inference: the threat to agent-written verified Rust is medium to high for process failures: an agent may prove a local postcondition while violating the requested workflow, omitting a required review, or silently changing the specification. AgentPex-style traces can find such omissions, but they cannot establish theorem soundness; Verus and compiler results remain the evidence for functional claims. What is already done here is prompt-derived procedural checking at deployment scale, so VL should not redo it as if a final-outcome score were sufficient.
techniques for the catalog
- trace normalization — convert heterogeneous conversations into one artifact containing prompt, tool schema, and ordered messages
- explicit specification extraction — derive output, transition, forbidden-edge, argument, predicted-plan, and final-state rules only from stated directives and available state
- minimum-capped trace evaluation — run per-specification evaluators and bound a weighted aggregate by its lowest critical evaluator Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Outcome-based evaluation can still score such a trace as correct if the final state matches.”): I read the whole paper (body, references, appendix prompts) and checked every quotation, number, section and page reference, and the technique steps against it; I changed the DOI link (it was truncated), the page numbers (several were wrong), the airline-example account (the 85 is the output evaluator’s score and the aggregate cap, not a sum of the listed violations), the description of the evaluator suite (forbidden-edges evaluation uses no LLM), the limitation wording (section 5.2 and 6 claims), the denominators for table 1 (now marked as inference), and renamed the aggregation technique to avoid the paper’s term; I added the spot-check domain and a few counts. I did not check the cited related work or the GitHub repository, nor the Verus-related inferences beyond marking them as inference.
Last edited: