From Natural Language Policies to Executable Obligations: A Verification Harness for Dependable In-Car LLM Agents
2026-08-24 • Software Engineering
Software Engineering
AI summaryⓘ
The authors describe AgentGuardUtil, a system designed for in-vehicle Large Language Model (LLM) agents that must strictly follow a written operating policy on every action. They make the LLM act as a proposer that can be checked and corrected through a process involving a policy compiler that turns natural language rules into precise, machine-checkable rules. A deterministic engine then verifies these rules against current data and updates, producing exact fixes instead of vague reminders. The system includes multiple checks and a critic to guide revisions until the policy is fully met.
Large Language ModelsOperating policyPolicy compilerMachine-checkable rulesDeterministic obligation engineVerify-and-revise loopAI planningBounded revision loopIdentifier provenanceSchema validity
Authors
Radouane Bouchekir, Damir Safin, Tomas Bueno Momcilovic
Abstract
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-before-act, confirmation and future-time protocols) and an LLM critic produce tiered findings that drive a bounded revision loop tuned for the pass k metric.