# Autoformalization of Agent Instructions into Policy-as-Code

arXiv: https://arxiv.org/abs/2606.26649 · HTML: https://mlsanity.com/paper/2606.26649/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 7 of its 17 references that are in the map.
- First posted on arXiv 25 Jun 2026.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)
- LLM safety and security / [Prompt injection and agent security](https://mlsanity.com/safety/prompt-injection-and-agent-security/)

## Builds on (most cited first, 7 of 7)

- [LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworks](https://mlsanity.com/paper/2402.01817/) (2024)
- [Contextual Agent Security: A Policy for Every Purpose](https://mlsanity.com/paper/2501.17070/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Policy-as-Prompt: Turning AI Governance Rules into Guardrails for AI Agents](https://mlsanity.com/paper/2509.23994/) (2025)
- [AgentGuardian: Learning Access Control Policies to Govern AI Agent Behavior](https://mlsanity.com/paper/2601.10440/) (2026)
- [Don't Make Models Guess Security and Safety: Symbolic Guardrails for Domain-Specific AI Agents](https://mlsanity.com/paper/2604.15579/) (2026)
- [Contextual bandits with entropy-based human feedback](https://mlsanity.com/paper/2502.08759/) (2025)

## Built on by (most cited first, 2 of 2)

- [NOMOS: Compiling Written Policies into Statically Verified Tool-Call Gates for LLM Agents](https://mlsanity.com/paper/2610.11030/) (2026)
- [MENTOR: Procedural Shielding of Tool-Using LLM Agents](https://mlsanity.com/paper/2610.17039/) (2026)

## Abstract (arXiv)

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.