Autoformalization of Agent Instructions into Policy-as-Code

🕒 Published (v1): 2026-06-25 06:23 UTC · Source: Arxiv · Venue: ICML 2026 · link

Why this paper was selected

ICML 2026; first formal Policy-as-Code autoformalization for agent safety with hard guarantees

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

LLM-powered agents need formal safety guarantees that probabilistic guardrails (classifiers, prompt steering) cannot provide. This paper introduces an autoformalization pipeline that converts natural-language agent instructions, MCP tool schemas, and policy documents into Cedar Policy Language rules via a generator-critic loop, enforcing them at runtime through an external deterministic policy engine. On MedAgentBench, the pipeline covers substantially more of an 88-rule policy than hand-coded symbolic guardrails covering only 23 of those rules.

Problem

Agent safety approaches fall into two inadequate camps: (1) probabilistic guardrails (fine-tuned classifiers like Llama Guard, prompt-based steering) that offer no formal guarantees and are vulnerable to jailbreaks and prompt injection; and (2) hand-coded symbolic enforcement that requires significant manual effort and scales poorly to real policy documents with dozens or hundreds of rules. There is no scalable path from natural-language policy specifications to formally verified, deterministically enforced agent constraints.

Method

The pipeline implements a three-layer Verification Sandwich:

1. Grounding layer — extracts entities, MCP tool schemas (OpenAI JSON schema format), and constructs a principal-resource-action ontology. A Cedar schema is generated programmatically from MCP tool definitions.

2. Model layer (generator) — Gemini 3 Pro is prompted with the agent system prompt, tool definitions, and policy documents to produce candidate Cedar policy sets.

3. Safety layer (dual critic):

4. Hard critic: deterministically invokes the Cedar reference tooling (Rust cedar-policy CLI) for syntax validation, schema compliance, vacuous-policy detection, and logical contradiction checks. On failure, error messages are fed back to the generator (up to 3 retries).
5. Soft critic: a two-stage LLM-as-judge pipeline (Gemini 2.5 Flash at temperatures 0.3 and 0.1, Judge → Verifier) evaluating semantic alignment against a rubric.

The loop runs until the hard critic passes; the resulting Cedar policy set is enforced at runtime by an external deterministic policy engine that sits outside the LLM context window (fail-closed: errors default to deny). For MedAgentBench evaluation, Claude Opus 4.7 additionally transcribed FHIR constraints from the reference MCP server into Cedar rules to achieve parity with the baseline's MCP-level enforcement.

Key Contributions

• Autoformalization pipeline translating agent cards (system prompt + MCP tool definitions + natural-language policy documents) into Cedar policies via a generator-critic loop.
• Open-source Cedar policy harness for agent scaffolds with custom Python Cedar language bindings.
• Verification Sandwich architecture formalizing the grounding → generation → dual-critic structure.
• Empirical evaluation on MedAgentBench showing broader policy coverage than prior hand-coded symbolic guardrails (23 of 88 rules vs. the pipeline's broader autoformalized set).
• Cedar schema auto-generated from MCP tool definitions, enabling type-safe policy enforcement without manual schema authoring.

Results

• On MedAgentBench (300 original trajectories, 50 adversarial trajectories), Cedar block rates vs. Hong et al.'s unsafe rates:

Condition	Dataset	Hong et al. Unsafe ↓	Cedar Block Rate ↑
Raw	Original	39.0%	30.3% (91/300)
Baseline	Original	23.0%	57.7% (173/300)
Guardrail	Original	0.0%	55.7% (167/300)
Raw	Adversarial	78.0%	72.0% (36/50)
Baseline	Adversarial	62.0%	82.0% (41/50)
Guardrail	Adversarial	0.0%	85.7% (42/49)

• The Cedar block rate is higher than Hong et al.'s unsafe rate because Cedar covers more of the 88-rule policy; Hong et al.'s 0% Guardrail unsafe rate is by construction within their 23-rule scope.
• Among trajectories containing at least one POST (write) attempt, Cedar blocks 100% in Original Raw, Original Guardrail, and all three Adversarial conditions (94.0%–100% across all write-containing splits).
• All 7 Adversarial Guardrail "misses" involved no POST: 5 had no tool calls at all (agent self-refused), 2 were read-only GET retrievals.
• Most-fired rules: 2_4_restate_patient_before_write (416 firings), 5_1_writes_require_confirmation (416), 6_3_stop_on_tool_error (346), 5_9_service_request_priority_stat (280).

Limitations

• Cedar is stateless: does not natively support multi-turn agentic workflows requiring action ordering or persistent context across turns (acknowledged; future work targets temporal logic integration and memory-aware policies).
• Coverage gap for dialog-only behavior: Cedar can only intercept tool calls, not LLM-generated text responses; trajectories involving no POST writes are unblockable by design.
• Soft critic remains non-deterministic: semantic alignment checking relies on an LLM judge, introducing the same probabilistic uncertainty at policy generation time that the approach eliminates at enforcement time.
• Policy friction trade-off: overly restrictive autoformalized policies degrade agent utility; the "Goldilocks zone" requires a sophisticated soft critic and is not fully solved.
• Evaluation scope: tested on a single benchmark (MedAgentBench) with a synthetically generated 88-rule policy; generalizability to other domains and real policy documents is undemonstrated.
• Generator model dependency: policy quality depends on the capability of Gemini 3 Pro; confabulation risk at generation time is mitigated but not eliminated by the hard critic.

Relevance to Agentic AI / LLM Agents

This work directly addresses one of the most critical open problems in deploying LLM agents in high-stakes settings: the gap between natural-language safety specifications and enforceable guarantees. By externalizing policy enforcement to a deterministic engine outside the context window, it provides a principled defense against prompt injection and jailbreaks that in-context guardrails cannot offer. The MCP tool schema integration is immediately relevant to the emerging agentic ecosystem (LangGraph, Amazon Strands, Claude's tool-use), as it makes policy generation automatic from the same tool definitions agents already consume. The generator-critic loop pattern also generalizes as a template for other neurosymbolic agent safety architectures where formal correctness must be reconciled with LLM-generated content.