# How We Built Cedar: A Verification-Guided Approach

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Jul 2024.

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

- [ETDI: Mitigating Tool Squatting and Rug Pull Attacks in Model Context Protocol (MCP) by using OAuth-Enhanced Tool Definitions and Policy-Based Access Control](https://mlsanity.com/paper/2506.01333/) (2025)
- [Verifiable Agentic Infrastructure: Proof-Derived Authorization for Sovereign AI Systems](https://mlsanity.com/paper/2605.15228/) (2026)
- [AgentFlow: A Flow-Centric Policy Language and Framework for Securing LLM Agent Systems](https://mlsanity.com/paper/2608.22868/) (2026)

## Abstract (arXiv)

This paper presents verification-guided development (VGD), a software engineering process we used to build Cedar, a new policy language for expressive, fast, safe, and analyzable authorization. Developing a system with VGD involves writing an executable model of the system and mechanically proving properties about the model; writing production code for the system and using differential random testing (DRT) to check that the production code matches the model; and using property-based testing (PBT) to check properties of unmodeled parts of the production code. Using VGD for Cedar, we can build fast, idiomatic production code, prove our model correct, and find and fix subtle implementation bugs that evade code reviews and unit testing. While carrying out proofs, we found and fixed 4 bugs in Cedar's policy validator, and DRT and PBT helped us find and fix 21 additional bugs in various parts of Cedar.