Autoformalization of Agent Instructions into Policy-as-Code
For developers of LLM-based agents in high-stakes domains, this work provides a scalable method to generate formally enforceable policies from natural language, reducing reliance on probabilistic guardrails.
The authors present an autoformalization pipeline that translates agent instructions and natural language policies into formally verified Cedar policies, achieving broader coverage of source specifications than hand-coded enforcement on MedAgentBench.
Agent safety in high-stakes domains requires formal policy enforcement, but most existing approaches either rely on probabilistic guardrails (fine-tuned classifiers, prompt-based steering) that offer no formal guarantees, or on hand-coded symbolic enforcement that does not scale to the breadth of real policy specifications. We present an autoformalization pipeline that translates agent prompts, MCP tool descriptions, and natural language policy documents into formally verified policies using an LLM-based generator-critic loop. The resulting policies are written in the Cedar Policy Language. On the MedAgentBench benchmark, our autoformalized policies cover substantially more of the source natural-language specification than the hand-coded symbolic enforcement in prior work.