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. Configure a model provider. Codex login is the default path:

   codex login
   autocedar doctor
   

   AutoCedar also supports Claude Code subscriptions through claude -p, direct Anthropic and OpenAI API keys, and local OpenAI-compatible servers. All five paths can be selected in the TUI. See Model providers and configuration.

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. Claude Code, direct Anthropic/OpenAI API keys, and local servers are provider choices in the TUI; see Model providers and configuration.

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.

From GitHub Container Registry (GitHub authentication may be required while the package is private):

mkdir -p "$HOME/.config/autocedar"
chmod 700 "$HOME/.config/autocedar"
docker run --rm -it \
  --env-file .env \
  -v "$HOME/.codex:/root/.codex:ro" \
  -v "$HOME/.config/autocedar:/root/.config/autocedar" \
  -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 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 five provider IDs:

Provider, model, effort, authentication, and the local endpoint are configurable inside the TUI. Non-secret settings and API keys are stored separately with private permissions; Codex and Claude credential files are never copied. For commands, precedence rules, environment variables, migration behavior, and security details, see Model providers and configuration.

Stevens/Jarvis-specific Slurm setup is intentionally isolated in autocedar-jarvis/.

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:

mkdir -p "$HOME/.config/autocedar"
chmod 700 "$HOME/.config/autocedar"
docker build -t autocedar .
docker run --rm -it \
  --env-file .env \
  -v "$HOME/.codex:/root/.codex:ro" \
  -v "$HOME/.config/autocedar:/root/.config/autocedar" \
  -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 "$HOME/.config/autocedar:/root/.config/autocedar" -v "$PWD:/work" -w /work autocedar

Tagged releases publish the same image to GitHub Container Registry. If the container package is private, authenticate first with a GitHub token that can read packages; PyPI installation does not require GitHub authentication:

docker run --rm -it \
  --env-file .env \
  -v "$HOME/.codex:/root/.codex:ro" \
  -v "$HOME/.config/autocedar:/root/.config/autocedar" \
  -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". Mount ~/.config/autocedar as shown above to preserve TUI settings and API-key logins across --rm runs. The helper script creates and mounts this directory automatically; set AUTOCEDAR_DOCKER_CONFIG_DIR to use an isolated host path. For direct API providers, pass the matching key with -e or through a mounted, gitignored project .env. The claude-cli provider requires the Claude CLI inside the runtime and is therefore intended primarily for normal host installs.

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 the selected provider is authenticated and reachable. 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 active release workflow lives at .github/workflows/release.yml. Pushing a vX.Y.Z tag that matches pyproject.toml runs the full tests, builds and checks 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.