AutoCedar — HITL Cedar Policy Synthesis

AutoCedar is a human-in-the-loop policy authoring agent for Cedar access control policies. It turns natural-language policy intent into reviewed schema and property atoms, checks those atoms with Cedar/CVC5 where possible, and uses the packaged v1 CEGIS harness to verify and synthesize Cedar policies against formal bounds.

Start Here

You do not need to clone this repository to use AutoCedar. The normal path is the published Python package.

Option A: Install From PyPI

Use this if you just want to run the AutoCedar agent. This installs a persistent autocedar command on your PATH.

1. Install uv if you do not have it:

   curl -LsSf https://astral.sh/uv/install.sh | sh
   

   Restart your terminal after installing uv.

2. Install AutoCedar:

   uv tool install autocedar
   autocedar --version
   

   If your shell cannot find autocedar, restart the terminal. uv will also print the tool-bin directory it added to PATH.

   You can also install with pip, but only when that pip belongs to Python 3.11 or newer:

   python3.11 -m pip install --upgrade autocedar
   # or, if python3 is already 3.11+
   python3 -m pip install --upgrade autocedar
   autocedar --version
   

   If pip install autocedar says No matching distribution found, check python3 --version. AutoCedar requires Python 3.11+, and older Python interpreters will not see compatible PyPI releases.

3. Sign in to Codex for model-backed authoring:

   codex login
   autocedar doctor
   

   AutoCedar uses local Codex OAuth by default and reads the same ~/.codex/auth.json cache used by Codex. No OPENAI_API_KEY is required.

   Anthropic is still available as an explicit opt-in provider. If you want that path, run:

   autocedar apikey
   

   Paste the Anthropic key when prompted. AutoCedar writes it to your user config (~/.config/autocedar/.env by default), redacts it in the terminal output, validates it with Anthropic before saving, and uses it immediately and on later launches. The config directory and key file are stored with private permissions (0700 and 0600, respectively). You can also run autocedar apikey sk-ant-... if you prefer a one-line command. Do not share or commit your API key.

4. Install/check the local verifier tools:

   autocedar setup --yes
   autocedar doctor
   

   setup installs or prints install steps for Cedar CLI and CVC5. doctor verifies the exact toolchain AutoCedar will use.

5. Start AutoCedar:

   autocedar
   

Already tried AutoCedar before? Use one of these update paths:

# Persistent install.
uv tool upgrade autocedar

# If you want to upgrade every installed uv tool.
uv tool upgrade --all

# One-off latest run without installing/upgrading the persistent command.
uvx --refresh --from autocedar@latest autocedar

Check which version you are running:

# Persistent install.
autocedar --version

# One-off latest package.
uvx --refresh --from autocedar@latest autocedar --version

# Repo-local development checkout.
uv run autocedar --version

uvx and uv tool install are different modes. uvx --refresh --from autocedar@latest autocedar is a one-off latest run; it does not register AutoCedar as a persistent tool. uv tool list only shows tools installed with uv tool install autocedar, so AutoCedar not appearing there is expected if you use the uvx path. For normal use, prefer uv tool install autocedar, then run autocedar.

Option B: Local From The Repo

Use this only for development, modifying AutoCedar itself, running tests, or working directly with repo-local examples/datasets.

1. Clone the repo:

   git clone https://github.com/neselab/cedar-synthesis-engine.git
   cd cedar-synthesis-engine
   

2. Install the Python environment and sign in to Codex:

   uv sync
   codex login
   uv run autocedar doctor
   

   AutoCedar uses Codex OAuth by default. Anthropic is optional and explicit: use AUTOCEDAR_PROVIDER=anthropic or /provider anthropic, then run uv run autocedar apikey only if you intentionally want the Anthropic path.

3. Install/check the verifier tools:

   uv run autocedar setup --yes
   uv run autocedar doctor
   

   If setup says Cargo is not installed, install Rust first:

   curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
   

   If you prefer manual installation, these are the required checks:

   cargo install cedar-policy-cli --locked --version 4.10.0 --features analyze --force
   cedar --version
   cedar symcc --help | grep principal-type
   cvc5 --version
   

   If CVC5 lives outside your shell PATH, put its path in .env:

   CVC5=/path/to/cvc5
   

   On Ubuntu/Debian, that usually looks like:

   sudo apt-get update
   sudo apt-get install -y cvc5
   echo "CVC5=$(command -v cvc5)" >> .env
   

   On macOS with Homebrew, that usually looks like:

   brew install cvc5
   echo "CVC5=$(which cvc5)" >> .env
   

4. Run AutoCedar:

   uv run autocedar
   

autocedar setup installs or prints the missing verifier-tool install steps. autocedar doctor checks the exact Cedar, SymCC, CVC5, and model auth state AutoCedar will use. Fix any FAIL lines before authoring. After that, you should see the AutoCedar interactive terminal UI.

Option C: Docker

Docker is optional. Use it when you specifically want a containerized runtime with Cedar/CVC5 already bundled.

Without cloning the repo:

docker run --rm -it \
  --env-file .env \
  -v "$HOME/.codex:/root/.codex:ro" \
  -v "$PWD:/work" \
  -w /work \
  ghcr.io/neselab/autocedar:latest

From a cloned repo, the helper script builds/runs the image and preflights autocedar doctor:

./scripts/docker-autocedar

If Docker on Linux requires sudo, prefer the PyPI/local setup above. Running sudo docker with -v "$PWD:/work" can leave root-owned files in your working directory.

The Docker image pins Cedar CLI 4.10.0 with SymCC analyze enabled and installs CVC5 in the image. It should not depend on your host machine's Cedar or CVC5.

First Things To Type

Once the TUI opens, try:

/settings
/models
/model gpt-5.5
/effort high
start a policy draft
Doctors can read records for patients on their care team.
show the draft
save this as clinical.md

When you are ready to run authoring:

author this

If you already have a Cedar schema, use author this with schema workspace/schema.cedarschema instead.

AutoCedar will ask for confirmation before executing actions and will pause for human review when it proposes schema/property atoms.

What Each Setup File Does

Architecture

graph LR
    A["User in autocedar TUI<br/>or autocedar author"] --> B["Policy spec<br/>plain English"]
    B --> B0["Stage 0<br/>source DAG + local context packets"]
    B0 --> C{"Schema supplied?"}
    C -- "No" --> D["Stage 1<br/>LLM proposes schema atoms from bounded source packets"]
    D --> E["HITL review<br/>approve / reject / edit / question"]
    E --> F["Composed Cedar schema"]
    C -- "Yes" --> G["Use supplied schema<br/>skip Stage 1"]
    F --> H["Stage 2<br/>LLM proposes bounded local property bundles"]
    G --> H
    H --> I["Symbolic checks<br/>cedar symcc + CVC5"]
    I --> J["HITL review<br/>approve / reject / edit / question"]
    J --> R{"Rejected?"}
    R -- "No" --> K["Approved target updated"]
    R -- "Yes" --> RP["Model-planned repair<br/>current property / prior property / schema / skip / clarify"]
    RP --> H
    K --> IC["Incremental candidate check<br/>against approved atoms so far"]
    IC --> H
    K --> L["Final Stage 3 synthesis<br/>v1 CEGIS harness"]
    L --> M["candidate.cedar"]
    M --> N{"All checks pass?"}
    N -- "No, verifier feedback" --> L
    N -- "Yes" --> O["Verified policy"]

Engine Layer

Workspace Layer (workspace/)

Three Verification Check Types

Entities vs. Domains

In Cedar, entities (entities.json) define concrete instances for runtime authorization (cedar authorize). This engine operates at the symbolic/type level using cedar symcc, which reasons over all possible inputs — so no entities.json is needed.

For bounding string values (e.g., valid departments), @domain annotations in the schema give the SMT solver a finite model, serving a similar conceptual role to entities but at the type-constraint level.

Full Workflow

The normal workflow is inside the CLI agent. You do not have to hand-write a schema before authoring unless you already have one.

Step 1: Start the agent

uv run autocedar

Inside the TUI, describe what you want in normal language. Plain conversation stays conversational. Drafting and tool execution only start after explicit confirmation.

Step 2: Capture or load a policy spec

You can type a spec into the TUI:

start a policy draft
Doctors can read records for patients on their care team.
Nurses can update vitals, but only during their shift.
show the draft
save this as clinical.md

Or you can start from an existing file:

author clinical.md

Step 3: Choose schema mode

There are two supported paths:

If you need bounded string values for symbolic reasoning, mention that in the spec or add/edit the schema during review with Cedar @domain annotations.

Step 4: Review schema and property atoms

AutoCedar uses the same review controls for both schema intent and policy intent:

Common edit examples:

E cedar_type=Bool
E optional=true
E field_name=isPublic
E principal_types=User,Admin
E resource_types=Document
E action=view
E constraint_type=floor

For example, if AutoCedar proposes a schema attribute as String but it should be a boolean flag, use E cedar_type=Bool. AutoCedar re-presents the edited atom before you approve it. If you edit a property atom, symbolic checks are rerun after approval so stale verification results are not reused.

After the schema is established, AutoCedar asks the model for bounded local Stage 2 property bundles from a source packet plus the current schema and approved target. This cuts repeated model round trips without changing the review contract: each returned property atom is still symbolically checked and sent through HITL review one by one before it can enter the formal target. Each source packet records the current source node, nearby clauses, related definitions, approved atoms, and prior review history. During this stage, AutoCedar prints property progress and shows a TUI progress bar over source packets, with details such as the current source packet, open source-node count, approved/rejected atom count, and queued atoms so long reviews do not look stuck.

The approved atoms become the formal verification harness:

• verification_plan.py — check descriptors such as implies, always-denies-liveness, and never-errors
• references/*.cedar — reviewed ceiling/floor reference policies

If you reject a property atom, AutoCedar now asks the model for a structured repair plan instead of guessing from keywords in your rejection text. The model must choose one of these actions:

After each approved property atom, AutoCedar compiles the approved target so far and runs an incremental candidate check. This is an early diagnostic pass: it does not replace final Stage 3 synthesis, but it surfaces candidate/schema/atom conflicts while the intent target is still being built.

Step 5: Synthesize and verify

Once the approved atoms compile into a harness, Stage 3 runs the CEGIS loop:

                    ┌──────────────────────────────────┐
                    │                                  │
                    ▼                                  │
            ┌──────────────┐                           │
            │ Synthesizer  │                           │
            │ reads spec,  │                           │
            │ schema, and  │                           │
            │ prior errors │                           │
            └──────┬───────┘                           │
                   │ writes                            │
                   ▼                                   │
         candidate.cedar                               │
                   │                                   │
                   ▼                                   │
  ┌────────────────────────────────┐                   │
  │        ORCHESTRATOR.PY         │                   │
  │                                │                   │
  │  Gate 1: cedar validate        │                   │
  │    → syntax/type errors?       │                   │
  │                                │                   │
  │  Gate 2: cedar symcc + CVC5    │                   │
  │    → implies / always-denies   │                   │
  │      / never-errors            │                   │
  └────────────┬───────────────────┘                   │
               │                                       │
               ▼                                       │
        ┌─────────────┐      Yes                       │
        │ loss == 0 ? │──────────▶ ✅ VERIFIED          │
        └──────┬──────┘                                │
               │ No                                    │
               ▼                                       │
      Counterexamples returned                         │
      to the synthesizer for fixing                    │
               │                                       │
               └───────────────────────────────────────┘
                    (max 20 iterations)

Example Iteration Trace

Iteration 1 — Agent writes a naive policy:

permit (principal, action == Action::"delete", resource);

Result: loss: 1 — implies check fails.

COUNTEREXAMPLE: principal.department = "HR", resource.is_locked = false → ALLOW

Iteration 2 — Agent adds department constraint:

permit (principal, action == Action::"delete", resource)
when { principal.department == "Engineering" };

Result: loss: 1 — still fails.

COUNTEREXAMPLE: resource.is_locked = true → ALLOW

Iteration 3 — Agent adds lock guard:

permit (principal, action == Action::"delete", resource)
when { principal.department == "Engineering" && !resource.is_locked };

Result: loss: 0 — all checks pass ✓. Policy is formally verified.

Detailed Setup Reference

AutoCedar is published on PyPI. For normal use, install the persistent command:

uv tool install autocedar
autocedar

pip also works when it is tied to Python 3.11+:

python3.11 -m pip install --upgrade autocedar
# or, if python3 is already 3.11+
python3 -m pip install --upgrade autocedar
autocedar --version

If plain pip install autocedar cannot find a matching distribution, that usually means the pip command is using Python 3.10 or older. Use a Python 3.11+ interpreter explicitly, or use the uv tool install autocedar path above.

To upgrade a persistent install:

uv tool upgrade autocedar
autocedar --version

For repo-local development, use:

uv run autocedar

The runtime package installs the Python agent/library and the autocedar console script. Verification also needs the Cedar CLI and CVC5 solver. Use the guided setup path:

autocedar apikey
autocedar setup --yes
autocedar doctor
autocedar --version
autocedar

If setup cannot safely install a system dependency on your platform, it prints the exact blocked prerequisite. Docker/GHCR remains the fully bundled path.

For a one-off latest run without installing a persistent command:

uvx --refresh --from autocedar@latest autocedar

External Dependencies

• Python 3.11+
• Cedar CLI v4.10+ with SymCC analysis enabled: cargo install cedar-policy-cli --locked --version 4.10.0 --features analyze
• CVC5 SMT solver: AutoCedar first uses $CVC5, then cvc5 on $PATH, then falls back to ~/.local/bin/cvc5

AutoCedar looks for:

• $CEDAR, defaulting to ~/.cargo/bin/cedar
• $CVC5, defaulting to cvc5 on $PATH, then ~/.local/bin/cvc5

If those binaries live elsewhere, set them in your shell or .env.

Check the verifier setup before running policy verification:

uv run autocedar setup
uv run autocedar doctor
cedar --version
cedar symcc --help | grep principal-type
cvc5 --version

If cedar symcc --help says the CLI was built without analyze, or if grep principal-type prints nothing, the installed Cedar binary cannot run AutoCedar's symbolic verification path. Reinstall with:

cargo install cedar-policy-cli --locked --version 4.10.0 --features analyze --force

LLM Providers And Local Config

AutoCedar supports three live model providers:

• OpenAI Codex by local Codex OAuth. This is the default provider. It reuses the login cache created by codex login and defaults to gpt-5.5.
• Anthropic by API key. This is explicit opt-in via AUTOCEDAR_PROVIDER=anthropic or /provider anthropic.
• Local model servers such as vLLM. This is explicit opt-in via AUTOCEDAR_PROVIDER=local or /provider local. vLLM's OpenAI-compatible protocol is an internal transport detail; no OpenAI cloud service is used.

Anthropic API Key

The easiest explicit Anthropic path is the CLI helper:

uv run autocedar apikey

It prompts for the key with hidden input, creates or updates the user-level AutoCedar config, and sets ANTHROPIC_API_KEY for that process. By default the key is stored here:

~/.config/autocedar/.env

Project .env files still work and override the user config when present. To write a specific project file:

uv run autocedar apikey --env ./policy-project/.env

To remove the persisted key:

uv run autocedar apikey clear

You can also export it:

export ANTHROPIC_API_KEY=sk-ant-...
autocedar

Or create a .env file in the directory where you run AutoCedar:

AUTOCEDAR_PROVIDER=codex
AUTOCEDAR_CODEX_MODEL=gpt-5.5
AUTOCEDAR_EFFORT=high
CEDAR=/usr/local/bin/cedar
CVC5=/usr/bin/cvc5

At startup, autocedar loads the nearest .env from the current directory or one of its parents. Existing shell environment variables are not overridden. For a normal project, the path is simply:

your-policy-project/.env

OpenAI Codex OAuth

To use the default Codex provider, sign in once with the Codex CLI:

codex login

Codex stores the local login under ~/.codex/auth.json by default. Treat that file like a password; it contains OAuth tokens. AutoCedar reads that cache, refreshes it when needed, calls the Codex backend directly, and discovers the models visible to that token. No OPENAI_API_KEY is required for this path.

Inside AutoCedar, these commands show or adjust the default path:

/provider codex
/models
/model gpt-5.5
/effort high

/models lists the models visible to your Codex OAuth token and shows each model's supported reasoning levels, default reasoning level, context window, speed/service tiers, and verbosity support. AutoCedar keeps the UI spelling max; when the selected provider is Codex, /effort max sends Codex's token-visible xhigh reasoning level.

Local Models Through vLLM

Start a chat/instruction model with an OpenAI-compatible server such as vLLM, then point AutoCedar at that server. The served model name must match the model name AutoCedar sends:

export AUTOCEDAR_PROVIDER=local
export AUTOCEDAR_LOCAL_BASE_URL=http://127.0.0.1:8000/v1
export AUTOCEDAR_LOCAL_API_KEY=autocedar-local
export AUTOCEDAR_LOCAL_MODEL=autocedar-local
export AUTOCEDAR_LOCAL_MAX_TOKENS=8192

autocedar doctor
autocedar author policy_spec.md --out ./autocedar-runs --model autocedar-local

The endpoint-specific key is optional if the local server does not require one. AutoCedar never reuses OPENAI_API_KEY implicitly for this path. Local model calls are reported at zero API cost; GPU allocation cost is outside that estimate. When using 127.0.0.1, the server and AutoCedar must run on the same machine or Slurm node. AUTOCEDAR_LOCAL_MAX_TOKENS caps only local-model responses, which is useful when the served model has a smaller context window.

For a freshman-friendly Slurm walkthrough, including rootless Cedar/CVC5 setup, vLLM startup, human review keys, and troubleshooting, see the standalone autocedar-jarvis guide.

To switch to Anthropic explicitly:

/provider anthropic

If your Codex auth file lives somewhere else, set one of:

export CODEX_HOME=/path/to/codex-home
export AUTOCEDAR_CODEX_AUTH_PATH=/path/to/auth.json

TUI Settings

The interactive agent can configure the current session from inside the TUI:

/settings
/provider codex|anthropic|local
/models
/model gpt-5.5
/effort low|medium|high|max
/apikey
/apikey clear

/apikey prompts for the Anthropic key, redacts it in the transcript, and validates it with Anthropic before saving. /apikey sk-ant-... also works for one-line setup. Rejected keys are not persisted. Valid keys save to the same user-level AutoCedar config, so the key persists across new uvx sessions and package upgrades. /provider codex uses the Codex OAuth cache instead of the Anthropic API key. /provider local uses AUTOCEDAR_LOCAL_BASE_URL; /models queries that server's /v1/models endpoint.

Docker

Docker is an optional containerized runtime. It is useful for reproducibility, but local install is usually simpler on Linux because Docker often requires extra daemon permissions.

./scripts/docker-autocedar

The script builds the image, uses .env, and mounts the current repo.

Manual equivalent:

docker build -t autocedar .
docker run --rm -it \
  --env-file .env \
  -v "$HOME/.codex:/root/.codex:ro" \
  -v "$PWD:/work" \
  -w /work \
  autocedar

If Docker reports invalid reference format, use the one-line form below. That error is usually caused by hidden Unicode spaces or broken line continuations in a copied multi-line command:

docker run --rm -it --env-file .env -v "$HOME/.codex:/root/.codex:ro" -v "$PWD:/work" -w /work autocedar

Tagged releases publish the same image to GitHub Container Registry:

docker run --rm -it \
  --env-file .env \
  -v "$HOME/.codex:/root/.codex:ro" \
  -v "$PWD:/work" \
  -w /work \
  ghcr.io/neselab/autocedar:latest

Docker users who want the default Codex provider should mount their Codex auth cache into the container, for example -v "$HOME/.codex:/root/.codex:ro". If you explicitly switch to Anthropic, pass -e ANTHROPIC_API_KEY=... or mount a project directory containing .env; AutoCedar will load that mounted .env from the container working directory.

How To Use AutoCedar

From this repo, prefix commands with uv run:

uv run autocedar
uv run autocedar verify workspace
uv run autocedar synthesize cedarbench/scenarios/realworld/emergency_break_glass \
  --no-review --max-iters 20
uv run autocedar author path/to/spec.md --out ./autocedar-runs

After package installation, drop the uv run prefix and use autocedar directly.

With no arguments, autocedar opens the Textual-based interactive agent shell. Talk to it in normal language: "verify the workspace", "save this as policy.md", "author this", or "start a policy draft". Use "author this with schema workspace/schema.cedarschema" only when you already have a schema. Normal language stays conversational until drafting is explicitly approved; policy-like prose opens a "start drafting and add this?" gate instead of silently mutating the draft. Slash commands and explicit subcommands remain as shortcuts for repeatable runs. Before running authoring, verification, synthesis, saving, clearing, or starting draft capture, the TUI summarizes the inferred action and waits for "yes" / "no". The conversational layer can answer questions about the current TUI state, while author still runs with clean authoring inputs: the saved prose spec, optional schema, and HITL review decisions. verify and synthesize wrap the v1 CEGIS harness. The CLI/TUI authoring path uses LLM-backed Stage 1 schema atomization and one-at-a-time Stage 2 property atomization, then runs Stage 3 through the packaged v1 CEGIS harness adapter. The Stage 3 hook remains injectable for library users and tests; the explicit synthesize command also wraps the v1 CEGIS harness directly.

Interactive Agent Usage

Start the agent:

uv run autocedar

Inside the TUI, normal language is the primary interface once Codex OAuth is available through codex login, or once you explicitly switch to Anthropic and configure an Anthropic key. The live planner maps each message to one validated tool action; AutoCedar does not run a separate local phrase router.

start a policy draft
Doctors can read records for patients on their care team.
Managers can approve access only for records in their department.
show the draft
save this as clinical.md
author this
verify the workspace
synthesize emergency_break_glass no review max iters 7

If you already have a Cedar schema, say author this with schema workspace/schema.cedarschema to skip schema atomization and use that schema.

The agent does not silently mutate the draft. Starting policy authoring only turns on draft-capture mode; it does not add the sentence that started the mode to the draft. After AutoCedar says policy authoring has started, paste the natural-language requirements you want captured. Operational actions such as authoring, verification, synthesis, clearing, and saving also show a yes/no confirmation before execution.

Slash shortcuts are available for repeatable control:

You can also say this in ordinary language, for example: change line 2 to Nurses can update vitals only during their shift, delete draft line 3, or insert before line 2 Patients can view their own records. The model planner turns that into the same draft-edit action as the slash shortcuts.

During HITL atom review, the prompt accepts one-line review commands:

Useful edits:

E cedar_type=Bool
E optional=true
E principal_types=User,Admin
E resource_types=Document
E action=view
E reference_cedar=permit (...) when { ... };

After an edit, AutoCedar shows the atom again. Approve only when the corrected schema/property intent matches what you mean.

If a property atom fails symbolic checks, prefer R reason when the atom is conceptually wrong and E field=value when a specific field is wrong. A rejected property atom is repaired by the model and shown again for review; it is not silently approved.

Non-Interactive Commands

Use explicit subcommands for scripts and repeatable experiments:

uv run autocedar author policy_spec.md \
  --out ./autocedar-runs \
  --schema workspace/schema.cedarschema \
  --model gpt-5.5 \
  --effort high

uv run autocedar verify workspace

uv run autocedar synthesize cedarbench/scenarios/realworld/emergency_break_glass \
  --no-review \
  --max-iters 20 \
  --phase1-model gpt-5.5 \
  --phase2-model gpt-5.5

Output Files

Authoring writes session artifacts under the --out directory, usually autocedar-runs/<session-id>/. The important files are:

Troubleshooting

For packaging, runtime code lives under autocedar/. The packaged v1 harness import surface is autocedar.harness; the root-level scripts remain for backwards-compatible local workflows.

Distribution

AutoCedar is distributed as a lean Python runtime package. CedarBench and the larger research datasets are intentionally not included in the wheel; keep them as repository or release artifacts for benchmark and paper reproduction.

Release builds are produced with:

uv build
uvx twine check dist/*

The release workflow template lives at docs/release-workflow.yml. Install it as .github/workflows/release.yml using a GitHub token with workflow scope, then pushing a vX.Y.Z tag builds the Python distributions, publishes to PyPI through trusted publishing, and publishes the Docker image to GHCR.

The reference policies are the security contract

In a real deployment, the reference policies (ceilings + floors) are the formal spec — they encode what the organization intends to allow. That's precisely the kind of thing a security team would sign off on, just like they review IAM policy boundaries today. The difference is these are machine-verifiable, not just documented in a wiki somewhere.

The NL translation layer is a natural extension

And your instinct about the NL layer is spot on — it would slot in cleanly:

Security Admin (NL)
     ↕  ← LLM translation layer
Reference Policies (Cedar)
     ↓
Verification Engine (SMT)
     ↕  ← counterexample feedback
Synthesizer (policy generation)

The translation works in both directions:

1. Ceiling → NL: "This reference policy says: View access is allowed only when the user is a Clinical Researcher with clearance above 3, the document is not Highly Restricted, the project is Active, and either the departments match or the user is a Global Auditor."
2. Admin feedback → Updated ceiling: Admin says "Actually, I want clearance level 5 for confidential documents specifically" → LLM updates the ceiling policy → engine re-verifies the candidate.
3. Counterexample → NL: Instead of showing raw entity graphs, translate them: "A user in HR with clearance 3 was able to edit an Active project document — is this intended?"

This closes the loop on the Verifiable Synthesis Paradox from our research. The paradox was: LLMs generate convincing explanations but incorrect policies. This architecture inverts that:

• The LLM writes the policy (where it's unreliable) → but the SMT solver catches errors
• The LLM translates formal specs to NL (where it's reliable) → so humans can audit the ground truth
• The security admin never needs to read Cedar — they review NL summaries of formally verified specs

The LLM is used where it's strong (NL ↔ NL translation, code generation with feedback) and the formal methods handle what it's weak at (correctness guarantees). That's a much cleaner division of labor than either pure LLM synthesis or pure manual policy writing.