Guardians

Static verification for AI agent workflows.

An implementation of the ideas in Erik Meijer's "Guardians of the Agents" (CACM, January 2026). The paper's thesis: the root cause of prompt injection in agentic systems is the same as SQL injection — code and data aren't separated. The fix is the same too.

Instead of letting the LLM call tools one at a time and decide what to do after each result, the LLM generates a structured plan upfront using symbolic references (placeholders, not real data). A static verifier checks the plan against a security policy before any tool runs. Only verified plans execute.

The verifier uses three independent checks: taint analysis (does data flow from a source to a forbidden sink?), security automata (does the tool-call sequence reach an error state?), and Z3 theorem proving (do preconditions and frame conditions hold?).

The demo scenario from the paper: you ask your AI to summarize your inbox. A malicious email tells the agent to forward everything to the attacker. Three checks fire. The workflow never executes.

~1900 lines of core, 130 tests, two dependencies (pydantic, z3-solver). No LLM calls needed for verification. Python 3.11+.

Workflow AST ──→ verify(wf, policy, registry) ──→ WorkflowExecutor.run(wf)
                        │                                  │
                  VerificationResult              env, trace (results)
                  (violations, warnings)

Install

pip install -e .            # core only (pydantic + z3-solver)
pip install -e ".[llm]"     # adds litellm for LLM planning

Running tests

Install the dev extras, then run pytest from the repo root. There is no pytest on the PATH, so invoke it as python3 -m pytest.

pip install -e ".[dev]"           # pytest + ruff
python3 -m pytest                    # all 130 tests

python3 -m pytest tests/core         # core only (115)
python3 -m pytest tests/adapters     # LLM agent + planner (11)
python3 -m pytest tests/integration  # end-to-end scenarios (4)
python3 -m pytest -v                 # verbose, per-test output

Directory	Tests	Covers
tests/core	115	Workflow AST, verifier (taint/automata/Z3), executor, conditions, safe-eval, scope, loop fixpoint
tests/adapters	11	GuardedAgent and the planner — requires the .[llm] extra (litellm)
tests/integration	4	Full verify→execute pipeline on the paper's email prompt-injection demo (examples/email_agent.py)

Quick start

from guardians import (
    Workflow, WorkflowStep, ToolCallNode, SymRef,
    ToolSpec, ParamSpec, ToolRegistry,
    Policy, TaintRule,
    verify, WorkflowExecutor,
)

# 1. Define tools
registry = ToolRegistry()
registry.register(
    ToolSpec(name="fetch_data", source_labels=["sensitive"],
             params=[ParamSpec(name="query", type="str")]),
    lambda query="": [{"result": "data"}],
)
registry.register(
    ToolSpec(name="summarize",
             params=[ParamSpec(name="items", type="list")]),
    lambda items=None: "summary",
)

# 2. Define policy
policy = Policy(
    name="example",
    allowed_tools=["fetch_data", "summarize"],
)

# 3. Build a workflow
wf = Workflow(
    goal="Fetch and summarize",
    steps=[
        WorkflowStep(label="Fetch", tool_call=ToolCallNode(
            tool_name="fetch_data", arguments={"query": "recent"},
            result_binding="data")),
        WorkflowStep(label="Summarize", tool_call=ToolCallNode(
            tool_name="summarize",
            arguments={"items": SymRef(ref="data")},
            result_binding="summary")),
    ],
)

# 4. Verify
result = verify(wf, policy, registry)
assert result.ok

# 5. Execute
executor = WorkflowExecutor(registry, policy, auto_approve=True)
executor.run(wf)
print(executor.env["summary"])

What is checked

Static (verifier, before execution)

Check	Category
Tool in allowlist	allowlist
Tool has a registered spec	missing_spec
All symbolic refs are in scope	well_formedness
Tainted data does not flow to sinks	taint
Z3 preconditions hold	precondition
Z3 postconditions hold	postcondition
Z3 frame conditions hold	frame
Security automata stay in safe states	automaton

Runtime (executor, during execution)

Allowlist, preconditions, postconditions, automata, and budgets.

Frame conditions and taint are static-only. The default verify_first=True ensures they are checked before any tool runs.

Adapters (optional)

from guardians.adapters.agent import GuardedAgent

agent = GuardedAgent("email_agent", planner=my_planner)

@agent.tool(taint_labels=["email_content"])
def fetch_mail(folder: str = "inbox") -> list: ...

@agent.tool(sink_params=["body"])
def send_email(to: str, body: str) -> dict: ...

agent.deny("send_email", "to", not_in_domain=["company.com"])
agent.no_data_flow("fetch_mail", to="send_email.body")

result = agent.run("Summarize my inbox")

Adapters live under guardians.adapters and are never imported by the core.

Examples

Runnable scripts in examples/:

python examples/email_agent.py     # verify/execute pipeline; the paper's demo
python examples/guarded_agent.py   # decorator API + sanitizer escape hatch
python examples/llm_planning.py    # a live LLM plans; the verifier gates it

llm_planning.py needs the [llm] extra and Bedrock credentials. It shows a real LLM planning two goals: a benign one is verified and executed, while a benign-sounding request to forward inbox data offsite produces a sending plan that the verifier rejects (taint + domain) — and no retry gets it past the verifier, so nothing is sent. Override the model with GUARDIANS_MODEL.

Project layout

src/guardians/
    __init__.py          # core exports only
    workflow.py          # Workflow AST, SymRef
    tools.py             # ToolSpec, ToolRegistry
    policy.py            # Policy, automata, taint rules
    conditions.py        # condition grammar, Z3 translation
    safe_eval.py         # runtime expression evaluator
    results.py           # VerificationResult, Violation
    errors.py            # SecurityViolation
    verify.py            # static verifier
    execute.py           # runtime executor
    adapters/
        planner.py       # Planner protocol, prompt helpers
        litellm.py       # LiteLLM planner (requires [llm])
        agent.py         # GuardedAgent high-level API

Documentation

• Design — architecture, semantics, guarantees