Autoformalization of Agent Instructions into Policy-as-Code

How can developers reliably enforce safety policies on autonomous AI agents without relying on probabilistic guardrails, which lack formal guarantees, or manual symbolic coding, which is difficult to scale?

The authors propose the "Verification Sandwich," a layered architecture that automates the creation of formal policies. The pipeline consists of three layers: a grounding layer that maps agent tools to a structured ontology; a model layer that uses an LLM to generate candidate policies; and a safety layer that employs a generator-critic loop. This loop uses a "hard" critic (deterministic Cedar parser) to check for syntax errors, schema compliance, and logical contradictions, and a "soft" critic (LLM-as-a-judge) to ensure semantic alignment with the original natural language instructions.

When evaluated on the MedAgentBench benchmark, the autoformalized Cedar policies provided significantly broader coverage of safety rules compared to previous hand-coded symbolic guardrails. By decoupling policy enforcement from the agent's reasoning context, the system prevents adversarial techniques like prompt injection from bypassing safety rules. The authors demonstrate that their approach effectively blocks unauthorized actions, particularly in high-stakes scenarios involving write operations, while maintaining a clear audit trail through the human-readable Cedar language.

As AI agents gain elevated privileges to interact with sensitive systems (such as electronic medical records), traditional prompt-based steering becomes insufficient. This work provides a scalable, verifiable method for governing agent behavior, moving toward a "Policy-as-Code" paradigm that allows security engineers to audit and enforce deterministic constraints on non-deterministic LLM agents.