Autoformalization Translates Agent Instructions into Formal Policy-as-Code.

Ensuring agent safety in high-stakes environments demands formal policy enforcement, yet current approaches often fall short. Probabilistic guardrails, such as fine-tuned classifiers or prompt-based steering, lack formal guarantees, while hand-coded symbolic enforcement struggles to scale with the complexity and breadth of real-world policy specifications. This paper presents an innovative autoformalization pipeline designed to bridge this gap. It leverages an LLM-based generator-critic loop to translate various forms of agent instructions—including prompts, tool descriptions, and natural language policy documents—into formally verified policies. These policies are expressed in the Cedar Policy Language, providing a robust and verifiable framework. Evaluations on the MedAgentBench benchmark demonstrate the pipeline's effectiveness. The autoformalized policies achieve substantially greater coverage of the source natural-language specifications compared to prior work that relied on hand-coded symbolic enforcement. This advancement offers a scalable and formally guaranteed method for enforcing agent behavior, crucial for critical applications.