AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis
On the map: LLM agents and tool use → Agent threats, guardrails and governance
Abstract (arXiv)
Large Language Models are increasingly used to turn natural-language requirements into code. In access control, that shortcut is dangerous: a generated policy can compile and read correctly while granting access that no one approved. The difficulty is not only writing policy code. It is fixing what the requirements mean before code is written, and then checking that the final policy actually satisfies that intent. We present AutoCedar, a verifier-guided system that first turns natural-language access-control requirements into a reviewed, checkable target, and then synthesizes Cedar policies against that target. AutoCedar decomposes schema and policy authoring into small intent atoms: reviewable claims about vocabulary and behavior. Once those atoms pass mechanical validation and human intent review, the model proposes a candidate policy, the verifier checks it against the approved target, and each failure is turned into a repair signal that tells the model whether to broaden, narrow, or restructure the policy without changing the target. Because the model's work is split into small problems, each grounded in reviewed intent and backed by verifier feedback, end-to-end policy authoring becomes tractable. AutoCedar converges on all 221 tasks of CedarBench, our benchmark of authorization tasks paired with executable semantic boundaries. Across three requirements-corpus case studies covering healthcare, education, and conference management, AutoCedar converts noisy prose and extracted access-control fragments into reviewed schemas, formal checks, and a globally verified Cedar policy store for each scenario.
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 11 of its 27 references that are in the map. First posted on arXiv 4 Jul 2026.
Builds on
11 of 27 references.
References · 11
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
- 2020Generative Language Modeling for Automated Theorem Provingcited by 388
- 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
- 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
- 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
- 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 98
- 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
- 2024Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)cited by 34
- 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 12
- 2026Faithful Autoformalization via Roundtrip Verification and Repaircited by 8
- 2025Synthesizing Access Control Policies using Large Language Modelscited by 6
Built on by
Citing papers per year: 2026: 2.
2 papers.
Similar, not cited
Close in wording, no citation either way
- 2026PolicyBank: Evolving Policy Understanding for LLM Agents
- 2026From Natural Language Policies to Executable Obligations: A Verification Harness for Dependable In-Car LLM Agents
- 2026Sketch-based Access Control: A Multimodal Interface for Translating User Preferences into Intent-Aligned Policies
- 2026Autoformalization of Agent Instructions into Policy-as-Code
- 2026PolicyGuard: A Dialogue-Grounded Sub-Agent Verifier for Policy Adherence in LLM Agents
- 2026ActGov: Governing LLM Agent Actions via Policy-Constrained Validation
- 2025ARPaCCino: An Agentic-RAG for Policy as Code Compliance
- 2025Secure and Efficient Access Control for Computer-Use Agents via Context Space