Autoformalization of Agent Instructions into Policy-as-Code

Technical Summary: Autoformalization of Agent Instructions into Policy-as-Code

Problem Statement
The deployment of autonomous Large Language Model (LLM) agents in high-stakes domains (e.g., healthcare) presents a critical security trade-off: agents require elevated privileges to perform complex tasks, yet these privileges expand the attack surface for adversarial techniques like prompt injection. Current industry practices rely heavily on probabilistic guardrails, such as fine-tuned safety classifiers (e.g., Llama Guard) or prompt-based steering. While these methods offer some utility, they lack formal guarantees and are often inadequate for security-critical applications where deterministic enforcement is required. Conversely, hand-coded symbolic enforcement offers formal guarantees but fails to scale to the breadth and complexity of real-world policy specifications.

Methodology
The authors propose an autoformalization pipeline that translates natural language agent instructions, Model Context Protocol (MCP) tool descriptions, and policy documents into formally verified policies written in the Cedar Policy Language. This pipeline operates via a generator-critic loop structured as a "Verification Sandwich" with three distinct layers:

1. The Grounding Layer (Bottom): This layer establishes the foundation by extracting entities, identifying tool schemas (e.g., OpenAI JSON schemas), and defining a principal-resource-action ontology. It ensures that the agent operates within a structured environment where potential actions map to real-world entities and valid system identifiers. Crucially, it programmatically generates a Cedar schema from MCP tool definitions to serve as a strict type-checking mechanism.
2. The Model Layer (Middle): Utilizing state-of-the-art LLMs, this layer interprets natural language instructions and generates candidate policy sets. It leverages parametric knowledge to propose policies that reflect the intended agent logic.
3. The Safety Layer (Top): This layer employs a dual-critic mechanism to validate candidates:
   • Hard Critic: A deterministic, programmatic check using Cedar's built-in static analysis tools. It verifies syntax, enforces schema compliance, and detects logical contradictions (e.g., vacuous policies or conflicting rules).
   • Soft Critic: An LLM-as-a-judge that evaluates semantic alignment against a predefined rubric. It ensures the formal logic accurately reflects the spirit of the original natural language instructions and policy documents.

The loop iterates, feeding feedback from both critics back to the generator until the policy set passes both the hard and soft checks. The resulting policies are enforced at runtime by an external, deterministic policy engine, decoupling safety logic from the LLM's reasoning context.

Key Contributions

• Verification Sandwich Architecture: A novel layered approach to autoformalization that combines grounding, generative reasoning, and dual-mode verification (hard/soft) to translate unstructured policy into formal code.
• Open-Source Implementation: The release of an open-source policy harness for agent scaffolds implemented in Cedar, including custom Python bindings.
• Scalable Autoformalization: A pipeline that automatically converts agent cards (instructions + tool schemas) into verified authorization policies, addressing the scalability limitations of manual symbolic enforcement.
• Evaluation Framework: A rigorous evaluation on the MedAgentBench benchmark, comparing the autoformalized approach against prior hand-coded symbolic guardrails.

Results
The system was evaluated on MedAgentBench, a benchmark for tool-using electronic medical record (EMR) agents. The study compared three conditions: Raw HTTP tools, a Baseline with typed MCP tools, and a Guardrail condition using the authors' Cedar policies versus Hong et al.'s hand-coded symbolic guardrails.

• Coverage: The autoformalized pipeline covered substantially more of the source 88-rule natural language specification than the hand-coded approach, which only implemented 23 rules.
• Blocking Rates: In the "Guardrail" condition, the Cedar policy engine blocked a significantly higher percentage of policy violations compared to the hand-coded baseline, particularly in adversarial scenarios.
  • On the Original dataset, Cedar blocked 55.7% of trajectories (167/300), whereas the hand-coded guardrails blocked 0% (by construction, as they only covered a subset of rules).
  • On the Adversarial dataset, Cedar blocked 85.7% of trajectories (42/49).
• Write-Attempt Analysis: When filtering for trajectories containing actual write attempts (POST requests), the Cedar block rate approached 100% (e.g., 100.0% in the Adversarial Guardrail condition), demonstrating that the system effectively prevents unauthorized data modifications when they occur.
• Robustness: The system successfully prevented "jailbreaking" and indirect prompt injection by enforcing rules outside the LLM's context window.

Significance and Claims
The paper claims that this approach provides strong formal guarantees about agent behavior, a capability missing from probabilistic guardrails. By decoupling policy enforcement from the LLM's reasoning context, the architecture mitigates the risk of an attacker convincing the security layer to ignore its rules. The use of Cedar ensures that policies are human-readable, auditable, and formally verified, bridging the gap between the flexibility of natural language and the rigor of symbolic logic.

The authors acknowledge a "friction-utility trade-off," noting that overly restrictive policies can degrade agent utility. They posit that the Generator-Critic Loop, particularly the inclusion of a soft critic, is essential for achieving a "Goldilocks zone" where agents are sufficiently constrained yet remain functional. The work demonstrates that autoformalization can scale policy enforcement to complex, real-world specifications without sacrificing the formal guarantees required for high-stakes domains.

Limitations and Future Work
The authors note that Cedar is stateless by design, which limits its ability to handle multi-turn workflows dependent on action ordering or persistent context. Future work aims to address this by integrating temporal logic for prerequisite sequences and developing memory-aware policies that allow the engine to reference an agent's trajectory history.