From Natural Language Policies to Executable Obligations: A Verification Harness for Dependable In-Car LLM Agents

From Natural Language Policies to Executable Obligations: A Verification Harness for Dependable In-Car LLM Agents Radouane Bouchekir, Damir Safin and Tomas Bueno Momcilovic fortiss GmbH, Munich, Germany {bouchekir, safin, momcilovic}@fortiss.org

arXiv:2608.23282v1 [cs.SE] 24 Aug 2026

Abstract

tasks may be performed, including preconditions, mandatory side effects, confirmation requirements, and disclosure obligations. CAR-bench [4] captures these deployment challenges in the in-car domain. The benchmark evaluates ambiguity resolution (disambiguation), admitting unavailable capabilities (hallucination), and policy-compliant execution (base), using conjunctive success criteria over environment state, tool execution, policy compliance, and task termination. In this paper we present AgentGuardUtil, our submission to CAR-bench Track 11 . The design rests on two complementary principles (see Fig. 1). First, a student–teacher decomposition separates proposal from approval: the LLM (student) only proposes actions, while a verification harness (teacher) reviews each draft, returns concrete findings, and re-verifies the revision before any action reaches the agent (simulated driver). Second, the interaction between the two follows an assume–guarantee discipline in the spirit of compositional verification [2]: the verification harness assumes only that the student is a capable but fallible proposer, and carries the guarantee (i.e. policy compliance, grounding in observed data, and policy adherence) through deterministic checks compiled from the conversation’s own artifacts (policy text, tool schemas, observations), independently of the student’s behavior. At the first turn, the natural-language policy is compiled into typed machine-checkable rules, part of which receive an executable form. On every draft action, a deterministic obligation engine evaluates these rules against live tool results and the simulated post-write state of the draft itself, computing the exact remedial calls the policy requires; 25 further deterministic gates enforce identifier provenance, schema validity, and interaction protocols, and an LLM critic adjudicates the uncertain findings. Surviving findings drive a bounded revise-and-recheck loop before anything reaches the simulated driver. The main contributions of this work are summarized as follows: (i) Runtime policy compiler producing typed rules with an executable sublanguage, cached per policy hash (§2.2); (ii) Deterministic obligation engine that evaluates executable rules on a projection of the environment state, including simulation of the draft’s own writes, and emits exact remedial tool calls (§2.3); (iii) Tiered verification loop combining deterministic gates

Large Language Models (LLMs) agents deployed in vehicles must satisfy a written operating policy on every turn: a single hallucinated identifier, omitted mandatory side-effect, or premature completion claim fails the task. We present AgentGuardUtil, our entry to CAR-bench Track 1, which treats the AI planer (LLM) as a fallible proposer inside a grounded verify-and-revise loop. Its core novelty is a runtime policy compiler: the natural-language policy shipped with each conversation is compiled, once per policy, into typed machine-checkable rules, a subset of which receive an executable form. A deterministic obligation engine interprets these rules against live tool results and the simulated post-write state of the draft itself, emitting the exact remedial calls with computed arguments rather than natural-language reminders. Around this engine, 25 deterministic gates (identifier provenance, schema and enum validity, gather-beforeact, confirmation and future-time protocols) and an LLM critic produce tiered findings that drive a bounded revision loop tuned for the Passk metric.

1

Introduction

LLM-based agents are moving rapidly from research prototypes into products that act on the physical world. In-vehicle voice assistants are an exemplary setting: the agent controls windows, climate, lighting, navigation, charging, and communication on behalf of a driver whose attention is limited, under a manufacturer policy that encodes safety and interaction rules. Therefore, the most impactful scenario involving an unreliable agent is an autonomous action (e.g., a wrong interpretation of a speed limits) that leads to a safety incident (e.g., crash into another vehicle) - far more than a lower benchmark point. The conditions under which current AI agents are evaluated differ substantially from those encountered in deployment. In operational settings, user requests are frequently incomplete or ambiguous, requiring agents to either infer missing information or request clarification. Necessary tools, parameters, or external resources may be unavailable, making it essential for agents to acknowledge these limitations rather than fabricate outcomes. In addition, deployment environments impose domain-specific policies that regulate how

1 https://car-bench.github.io/car-bench/index. html

1

Agent under test AgentGuardUtil (Teacher)

Verification harness (one step per draft action (a) )

Policy text e.g., If AC on then close windows > 20%

Simulated driver Persona, conversation style Task instruction (base, halluc., disamb.)

Multi-turn messages

Runtime policy compiler

1

1b: typed + executabl e rules

(once, cached by policy hash)

2a: hard findings (bypass the critic)

2

Deterministic obligation engine

3

2b: advisory

LLM critic

confirm/discard advisories only

candidates

3a: yes: reply to driver LLM Proposer (Student)

0: prompt (user msg + policy text)

1

Tiered findings list 𝐹(𝑎) = ℎ𝑎𝑟𝑑 ∪ 𝑐𝑜𝑛𝑓𝑖𝑟𝑚𝑒𝑑

𝐹 𝑎 = ∅?

3b: yes: verified writes

Environ ment Tools, states, databases

1a: draft action a 3c: no: findings F(a) (revise, ≤ R rounds)

LLM Planner

tool results

Figure 1: Overview of AgentGuardUtil architecture and one verified turn. A student LLM proposes; a deterministic teacher disposes. The policy is compiled once into executable rules (1). Each draft action (2) passes one verification step: deterministic gates, including the obligation engine, emit hard findings, and an LLM critic may only confirm or discard advisory candidates (3). If the tiered list F (a) is non-empty, the draft returns to the student for revision, ≤ R rounds; if empty, verified writes reach the environment and the reply reaches the simulated drive. Under the assume–guarantee reading, the student is assumed only capable-but-fallible; every arrow leaving the teacher carries the guarantee. with an LLM critic (§2.4). The design composes chain-ofverification prompting [3] and self-consistency [1], but moves the decisive checks out of the model and into code that the model cannot hallucinate around;

Algorithm 1: V ERIFIED T URN(h, S) 1 2

if first turn for this policy Π then R ← RUNTIME P OLICY C OMPILER(Π, S) ; hash(Π)

// cached by

L ← L ∪ E XTRACTA SKS(new user msg);
a ← M ODALVOTE {LLM(h, S)}1..n ; 5 for i ← 1 to R do
6 F ← Fhard (a, h, R) ∪ C RITIC Fadv (a, h, R) ; 7 if F = ∅ then break; 8 a ← R EVISE(h, a, F ); 3 4

2

The AgentGuardUtil

2.1

Architecture

10

if a was revised and Fhard (a) ̸= ∅ then a ← R EVISEesc (h, a, Fhard (a)) ;

11

return S ANITIZE(a)

9

Fig. 1 and Algo. 1 follow one turn through the verification harness. The turn is prepared in three steps. First, at the first turn of a conversation, RUNTIME P OLICY C OMPILER translates the policy text Π into typed, executable rules R (§2.2); the result is cached under hash(Π), so later turns skip this step. Second, E XTRACTA SKS scans the new user message and appends each explicit request to a ledger L of outstanding asks, against which the completion gate (§2.4) later checks any claim of success. Third, the student proposes a draft a, i.e. a candidate answer for the turn, a spoken reply, tool calls, or both, which is neither shown to the driver nor executed until it passes verification. If the draft would mutate environment state and voting is enabled, the same prompt is sampled n times from the same LLM and M ODALVOTE keeps the action set proposed most often (the multiset of tool calls with normalized arguments), a majority vote in the sense of selfconsistency [1]. The draft then enters a verify-and-revise loop of at most R rounds, and each round separates two kinds of evidence. First, the deterministic gates of §2.4, among them the obligation engine of §2.3, produce hard findings Fhard , which stand as issued. Second, the same gates produce advisory candidates Fadv , which C RITIC (an LLM) may confirm or discard, but can neither extend with a finding of its own nor use to override a hard one. If the merged tiered list F is empty, the loop exits; otherwise R EVISE re-prompts the student with F

// safety net

injected as an internal note, and the revision re-enters verification. Two steps close the turn. First, because a revision can itself introduce a new defect, a safety net follows the loop: if the draft was revised and still carries hard findings, R EVISEesc runs once more on those deterministic findings alone, optionally under a stronger escalation model. Second, S ANITIZE strips the reply of markup that cannot be spoken, and the turn is released: verified tool calls reach the environment and the sanitized reply reaches the simulated driver.

2.2

Runtime Policy Compilation

At the first turn of a conversation, the policy text Π is compiled by an LLM into a rule set R. Each rule r = ⟨id, κ, Tr , ρ⟩ carries a type κ (precondition, auto-action, confirmation, prohibition, disclosure, constraint, selection), trigger tools Tr grounded against the live tool inventory, and an imperative requirement ρ. Compound clauses are split into atomic rules (one condition, one remedy). A second, focused 2

pass translates state-conditional rules into an executable form er = g, φ, ◁, v, ω ,

or that failed, marks the affected variables as unknown. Because rules are evaluated on this post-action estimate, a draft whose own actions would create a violation immediately produces the actions that repair it. - Step 2: compute the missing actions. A rule is active if one of its trigger tools was already used or appears in the draft (R▷ = {r : Tr ∩ (Wh ∪ Wa ) ̸= ∅}).

(1)

where g is a read tool, φ a field-name pattern with one wildcard, ◁ ∈ {<, ≤, >, ≥, =, ̸=, ∋, ̸∋}, v a threshold, and ω(x) = ⟨u, β(x)⟩ an obligation template binding the matched item x into the arguments of tool u. The compiler sees real signatures u(p1 , . . . , pm ); an obligation whose arguments cannot be validated is dropped, degrading that rule to advisory, the engine can only add precision, never force an invalid call.

Ω(a, h) =

\ Eh ∪ A a .

(2) For every active rule, and for every entity x (a window, a seat, a destination) whose projected value violates the rule’s condition, the engine fills the rule’s action template ω with x; it then removes actions the agent has already performed (Eh ) or already included in the draft (Aa ). What remains, Ω, is exactly the set of actions the agent still owes. - Step 3: match the expected granularity. If every entity violates the condition and the tool accepts an ALL-style argument, the per-entity actions collapse into one collective action, the granularity against which the benchmark scores intermediate states. The mirror check flags excess: actions on entities the condition exempts, and collective actions where only some entities qualify. Each finding quotes its actions ready to execute, together with the observed evidence, so the student no longer has to recall the policy — it only has to transcribe the correction.

get vehicle window positions, window * position, >, 20, open close window(⟨item⟩, 0) .

The executable form means: fetch the window positions with g; every returned field matching φ whose value exceeds v=20 binds its wildcard match (driver, passenger, . . . ) into the obligation template ω, validated against the declared enum of the window parameter (DRIVER, PASSENGER, . . . , ALL). At runtime (§2.3), with observed positions 25/100/0/10, exactly two obligations survive, open close window(DRIVER, 0) and open close window(PASSENGER, 0), and are quoted to the student verbatim with their evidence, window driver position = 25 > 20.

2.3

ω(x) : φ ∼ x, σ̂(x) ◁ v

r∈R▷

Example. To illustrate policy compilation, we consider the example of the policy “When setting the air conditioning to ON, automatically close all windows if they are open more than 20%”. first compiles to the typed rule r011 = ⟨011, auto-action, {set air conditioning}, ρ⟩. The trigger set contains the tool whose invocation activates the rule, which is the remedy. The second pass grounds r011 into the executable form of Eq. (1): e011 =

[ 

Example. Continuing e011 : the windows were observed at 25/100/0/10 (driver, passenger, and the two rear windows), and the draft proposes only set air conditioning(on). That proposed action activates rule 011; no other action has run since the observation, so the projected state equals the observed one. The driver (25) and passenger (100) windows violate the > 20 condition, and no closing action exists in the history or the draft, so Ω = {open close window(DRIVER, 0), open close window(PASSENGER, 0)} — issued as a hard finding with the evidence window driver position=25 > 20. The projection matters in both directions. Had the draft instead proposed opening all windows to 50% with the air conditioning on, simulating it would put every window at 50 in the projected state and the finding would demand the closes — a violation the draft itself would create. Conversely, once the student adds the two closing actions, simulation drives both windows to 0, Ω = ∅, and the draft is approved.

Executable Obligations

The agent perceives the environment only through tool calls: observation tools report part of the environment state, and action tools change it. For every draft run, the engine answers one question: given everything the agent has observed and the actions it now proposes, which further actions does the policy still require? It proceeds in three steps: - Step 1: estimate the post-action environment state. Let σg be the most recent observation returned by tool g, let w1 , . . . , wm be the actions executed after that observation, and let Wa be the actions the draft proposes. Each action may have changed, or would change, what was observed, so the engine applies all of them, in order, to the observation and obtains a projected state σ̂ = π(σg ; w1..m ·Wa ): its best estimate of the environment after the draft would execute. An action whose effect is predictable from a compiled rule is simulated, i.e. the affected state variable is set to the action’s argument value (an ALL-style argument affects every matching variable); an action whose effect is not predictable,

2.4

Tiered Verification and Variance Control

Around the obligation engine run 25 deterministic gates. Each gate checks one protocol the draft must respect, and each is decidable from the episode’s own artifacts: the transcript, the tool schemas, and prior observations. Each gate is a function that takes the draft a, the conversation history h, and the compiled rules R, and returns findings, hard or advisory; the most important ones are summarized in Table 1. 3

Gate

What it checks

Example finding

Identifier provenance

Collects every opaque identifier in the draft’s tool calls and looks each one up among the identifiers returned by earlier observations. An identifier that was never observed blocks the offending call: the agent may copy identifiers, never invent them. Compares every argument of every proposed call against the tool’s declared parameter types and allowed values, before anything executes. An argument outside the declaration is rejected. For every rule the draft activates, checks whether the observation its condition depends on has ever been made. If not, demands that observation — always a read-only call, never an action. For every proposed call the policy marks as requiring consent, searches the history for an intent question that the user affirmed. Without one, the call is blocked. Extracts the actions the draft’s reply claims to have performed and verifies that each was actually executed or is part of the draft itself. A claim without a matching action is rejected. When the reply tells the user something cannot be done, checks whether the free observation that would answer the request was ever made; if not, demands that read first. Detects that the request refers to a future moment (e.g. an arrival time) and checks that the draft answers it from unfiltered data evaluated at that moment, rather than filtering by the current moment.

Routing to loc lux 222378 is allowed only if some earlier tool result returned that id — a deterministic anti-hallucination check.

Schema validity

Gather-before-act

Confirmation protocol

Completion

Refusal-read

Future-condition

open close window(window=FRONT) is rejected because FRONT is not among the declared window values.

Rule 011 conditions on window positions, so set air conditioning(on) is held until get vehicle window positions has been called (§2.2). Opening a window beyond 25% while the air conditioning is on requires a question such as “shall I proceed?” and a “yes” before the action may execute. “I have closed all windows” with no open close window call is returned to the student. Replying “I cannot check the rear window” without ever calling get vehicle window positions forces that read. “Will the charging station still be open when I arrive at 20:00?” must be answered from the station’s opening hours, not from an open now filter that reflects the present.

Table 1: The principal deterministic gates. Each takes the draft a, the history h, and the compiled rules R, and returns findings; all seven above issue hard findings, which stand as issued and always trigger revision. until the round budget R is exhausted. What the step returns is the tiered findings list F (a). Tiering is what keeps the harness’s own variance bounded. A hard finding is deterministically certain and always triggers revision, so the decisive checks never depend on a sampled judgment; an advisory candidate is uncertain by construction and reaches the student only if the critic confirms it against the episode’s artifacts. Because the critic is confined to filtering a set it did not generate, a bad sample can only cost a missed advisory, never a spurious correction or a suppressed hard finding, the guarantees carried by the teacher degrade gracefully rather than inverting.

Algorithm 2: V ERIFY D RAFT(a, h, R) — one verification step (the line Fhard ∪ C RITIC(Fadv ) of Algorithm 1) Fhard ← ∅; Fadv ← ∅; foreach gate γ ∈ Γ do // Γ: 25 deterministic gates, incl. the obligation engine Ω of §2.3 3 (H, A) ← γ(a, h, R) ; // on internal error: 4 Fhard ← Fhard ∪ H; Fadv ← Fadv ∪ A;

1 2

5 6

(∅, ∅)

if Fadv ̸= ∅ then Fadv ← C RITIC(Fadv , h, S) ; // LLM critic: confirm or discard only; never adds, never overrides Fhard

8

foreach f ∈ Fhard ∪ Fadv do if f re-demands an action set the student already revised away then drop f and relax the gather gate // oscillation valve;

9

return Fhard ∪ Fadv ;

7

// tiered findings list F (a)

3

Evaluation

We report the official CAR-bench Track 1 results2 on the organizers’ hidden set of 30 tasks, three independent trials each, with the student instantiated as Claude Opus 4.8 and the harness at its defaults. The primary metric Pass3 credits a task only when all three trials succeed. We beat the baseline on all three scores. The gain is large on Pass@3, at 13.3 points, and small on Pass3 , at 3.3 points. This tells us what the harness does and does not do. It makes a good try better, because it removes mistakes before they reach the driver. It does not make the three tries more alike, because the student still writes a different draft each time. The three categories show where our checks work. Hallu-

Algorithm 2 details how the gates are combined into the single verification step that Algorithm 1 invokes once per revision round. First, every gate γ ∈ Γ is run over the same triple (a, h, R) and its two output sets are accumulated separately; a gate that raises an internal error contributes nothing, so a defective check can never block a well-formed draft. Second, if any advisory candidates were raised, the LLM critic adjudicates them as a batch against the transcript and the tool schemas: it may confirm or discard, but it may neither introduce a finding of its own nor overturn a hard one. Third, an oscillation valve scans the surviving findings and drops any that re-demand an action set the student has already revised away, relaxing the gather gate for the remainder of the turn; this prevents two gates from trading a draft back and forth

2 https://car-bench.github.io/car-bench/ leaderboard.html?team=track_1__team-16#explore

4

Pass3

Pass@3

Pass1

AgentGuardUtil Organizer baseline

53.3 50.0

80.0 66.7

66.7 60.0

hallucination base disambiguation

70.0 50.0 40.0

100.0 60.0 80.0

90.0 60.0 50.0

for markov decision process by using interval markov process. Innovations in Systems and Software Engineering, 14(3):229–244, 2018. [3] Shehzaad Dhuliawala, Mojtaba Komeili, Jing Xu, Roberta Raileanu, Xian Li, Asli Celikyilmaz, and Jason Weston. Chain-of-verification reduces hallucination in large language models. In Findings of the association for computational linguistics: ACL 2024, pages 3563–3578, 2024.

Table 2: CAR-bench Track 1 results (%), in total and per category (10 tasks each). Pass1 is the success rate of a single try. Pass@3 counts a task if at least one try succeeds. Pass3 counts it only if all three succeed. Our entry is 9.–11. of 21 on Pass3 .

[4] Johannes Kirmayr, Lukas Stappen, and Elisabeth Andre. CAR-bench: Evaluating the consistency and limitawareness of LLM agents under real-world uncertainty. In Maria Liakata, Viviane P. Moreira, Jiajun Zhang, and David Jurgens, editors, Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 40599–40618, San Diego, California, United States, July 2026. Association for Computational Linguistics.

cination is our best result. Here the checks are simple facts that code can look up. Was this identifier seen in an earlier tool result? Does this argument match the tool schema? No judgment is needed, so the answer is always the same. Disambiguation is our worst result. Code can check that the agent asked the user a question and got a “yes”. Code cannot tell whether the agent should have asked, because nothing in the transcript or the schemas answers that. This is left to the LLM critic, and the critic is not always right. The main loss is the gap between Pass@3 (80.0) and Pass3 (53.3). Eight tasks succeed in some tries but not in all three. Our checks are stable, but the student is not, and the checks are silent when no compiled rule covers the task. So the way to raise Pass3 is to turn more of the policy into executable rules. The harness is also slow and expensive. One try costs 362k tokens and 19.2 s per turn, against 82k and 3.2 s for the baseline. Across the whole field, spending more tokens does not give a better score (r=0.435).

4

Conclusion

AgentGuardUtil pairs an LLM student that drafts each turn with a deterministic teacher that checks every draft before it takes effect: the policy is compiled once into executable rules, each draft is evaluated against what was actually observed, including the state the environment would reach after the draft’s own actions, and the findings go back to the student until none remain. This addresses the three challenge classes directly: hallucinated identifiers are blocked (every outgoing identifier must have been observed), ambiguous requests are held behind confirmation checks, and forgotten policy side-effects come back as ready-to-execute actions.

References [1] Toufique Ahmed and Premkumar Devanbu. Better patching using llm prompting, via self-consistency. In 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 1742–1746. IEEE, 2023. [2] Redouane Bouchekir and Mohand Cherif Boukala. Learning-based symbolic assume-guarantee reasoning 5

Related documents

• OpenComputer: Verifiable Software Worlds for Computer-Use Agents#204842
• AgentTrails: Towards Trust and Reuse for Agentic Tasks#386977
• Moral Kernel Optimization as an Alignment Constraint for Large Language Models#85109
• Agent Safety From Within: Detecting Harmful Trajectories from LLM Internal States#1117751
• Agent-Facing Information Design in LLM Tool Registries: A Preregistered Test of Rhetoric, Position and Structure#1143778