v0.1.3: approval policies, policy-check, text example, docs

Author: dragon-ai-agent

README.md

@@ -152,13 +152,14 @@ top level. `just stdlib` proves them all.
 
 ## Examples
 
-The repo currently has three worked examples:
+The repo currently has four worked examples:
 
 | Example | Contracts | What it demonstrates |
 | --- | --- | --- |
 | [`examples/email`](examples/email) | `emails.only`, `emails.none`, `emails.no_guarantees`, `emails.unique_recipients`, `emails.content_length_at_most` | allowlists, explicit absence of guarantees, absence of effects, pairwise uniqueness, string length bounds |
 | [`examples/bank`](examples/bank) | `bank.max_spend`, `bank.only_account` | numeric aggregation, field equality, and fixed-bound loop unrolling over trusted calls |
 | [`examples/email-from-db`](examples/email-from-db) | `emails.addresses_from`, `db.only_table`, `db.only_where` | for-loops over trusted query returns, column-binding constraints |
+| [`examples/text`](examples/text) | `text.length_between`, `text.must_not_contain`, `text.no_regex_metacharacters`, `text.only_edit_under`, `text.edit_length_at_most` | string-length bounds, required/banned substrings, regex-metacharacter safety before sending, and file-edit path/size policies |
 
 All examples use generic effect relations inferred from trusted function
 signatures. There is no email-specific, bank-specific, or database-specific logic in the core.
@@ -177,11 +178,19 @@ Implemented pieces include:
 - `clauz3 install` for copying a trusted `tools/` layer from a local path or a
   bundled stdlib tool (`stdlib:filesystem`, `stdlib:grep`), optionally
   generating `agents/skills/<domain>/SKILL.md` stubs.
+- `clauz3 config` for writing this repo's default Claude Code permissions
+  (read-only tools plus the `clauz3` CLI) to `.claude/settings.json`. Idempotent
+  and the configuration counterpart to `install`.
 - `clauz3 run` for proving a complete inline program, submitting an approval
   request to an externally configured approval service, and executing `main`
   only after an approval receipt is returned.
 - `clauz3 approval-service` for starting a simple localhost FastAPI approval
-  service with REST endpoints and a browser UI for user decisions.
+  service with REST endpoints and a browser UI for user decisions. With
+  `--policy`, a policy admin's rules can auto-approve or auto-reject a request
+  by asking the prover whether the program *entails* the rule's contracts,
+  falling back to a human otherwise. `clauz3 policy-check` dry-runs a policy
+  against a program. See
+  [docs/todos/approval-policies.md](docs/todos/approval-policies.md).
 - `clauz3 mock-approval-service` for config-driven tests and local demos.
 - For-loops over `list[Row]`-returning trusted calls, with column-binding
   contracts via `UserRow.email` markers. See
@@ -218,6 +227,7 @@ More detail:
 - [ClauZ3 Python subset](docs/reference/python-subset.md)
 - [Approval service](docs/how-to/approval-service.md)
 - [User approval dialog design](docs/todos/user-approval-dialog.md)
+- [Guardians synergies](docs/todos/guardians-synergies.md)
 - [Ideas](docs/todos/ideas.md)
 
 ## Development

docs/examples/email.md

@@ -33,6 +33,33 @@ prover.
 
 {{ include_file("examples/email/cases/only_bob_fail.py") }}
 
+## The runtime layer (deal as a backstop)
+
+The static prover is only the first layer. The `@deal.pre` on `send_email`
+(`addr` must contain `"@"`) is also a *runtime* contract. The two layers act on
+the same artifact at different times.
+
+Statically, `precondition_fail.py` is rejected by the prover before anything
+runs, because it cannot discharge that precondition for the call below:
+
+{{ include_file("examples/email/cases/precondition_fail.py") }}
+
+The same precondition is what [deal](https://deal.readthedocs.io/) enforces at
+runtime. If the program is run outside a successful proof — a weak or
+`no_guarantees()` contract, or runtime-only mode — deal still raises on the bad
+call at the trusted boundary:
+
+```pycon
+>>> from tools.email.trusted.effects import send_email
+>>> send_email("bob@example.com", "hi")        # precondition holds: runs
+>>> send_email("not-an-email", "hi")           # precondition violated
+deal.PreContractError: addr must contain "@" (where addr='not-an-email', msg='hi')
+```
+
+Same check, different time: the prover discharges it ahead of execution, deal
+enforces it at execution. See
+[Concepts: static proof vs runtime](../explanation/concepts.md#static-proof-vs-runtime).
+
 ## All cases
 
 Every file under `cases/` is a small program plus its declared guarantee.

docs/examples/text-all-cases.md

@@ -0,0 +1,9 @@
+# Text — all cases
+
+Every case file under `examples/text/cases/`, inlined. `_pass` cases
+should prove; `_fail` cases should be rejected by the prover.
+
+See the [curated walk-through](text.md) for context on the trusted module
+and contract vocabulary.
+
+{{ include_dir("examples/text/cases", glob="*.py") }}

docs/examples/text.md

@@ -0,0 +1,70 @@
+# Text example
+
+The text example shows the relation algebra's **string** side: length bounds,
+substring requirements, and prefix policies. Everything here compiles to Z3's
+string theory — `len(...)` becomes `z3.Length`, `x in s` becomes `z3.Contains`,
+and `s.startswith(...)` becomes `z3.PrefixOf` — so the prover reasons about the
+*shape* of text symbolically, across every reachable branch.
+
+The trusted module exposes two side-effecting functions:
+
+- `send_message(channel, text)` — post text somewhere;
+- `edit_file(path, new_text)` — replace a file's contents.
+
+The contract vocabulary then states policies an agent (or a user reviewing the
+permission request) cares about:
+
+- **lengths within limits** — `length_at_most`, `length_at_least`,
+  `length_between`;
+- **required or banned substrings** — `must_contain` (e.g. a mandatory
+  `[automated]` footer), `must_not_contain` (e.g. a banned token);
+- **regex safety before sending** — `no_regex_metacharacters`, which forbids
+  every regular-expression metacharacter so agent- or user-influenced text
+  cannot inject a pattern or trigger catastrophic backtracking (ReDoS)
+  downstream;
+- **bounded sends** — `sends_at_most`;
+- **file-edit policies** — `only_edit_under` (a path-prefix sandbox),
+  `edit_length_at_most` (bounded rewrites), and `no_edits`.
+
+## Trusted module
+
+The trusted effects are stubs decorated with `@deal.has(...)` and a
+non-empty precondition. The prover lifts each precondition into a proof
+obligation at every call site.
+
+{{ include_file("examples/text/tools/text/trusted/effects.py") }}
+
+The contract module builds the string vocabulary on top of the generic
+`effect("send_message")` and `effect("edit_file")` relations. Note that the
+length and substring checks live inside ordinary lambdas — the same relation
+language used elsewhere, just exercising its string operators.
+
+{{ include_file("examples/text/tools/text/trusted/contracts.py") }}
+
+## A passing case
+
+Both messages are within the 20-character bound, so `text.length_at_most(20)`
+is discharged.
+
+{{ include_file("examples/text/cases/length_at_most_pass.py") }}
+
+## A failing case
+
+Text that will be fed to a pattern matcher must be metacharacter-free; the
+classic ReDoS pattern `(a+)+$` violates `text.no_regex_metacharacters()` and
+the proof fails.
+
+{{ include_file("examples/text/cases/no_regex_metacharacters_fail.py") }}
+
+## All cases
+
+Every file under `cases/` is a small program plus its declared guarantee.
+Cases with the `_pass` suffix should prove; cases with `_fail` should be
+rejected. Browse the full set on the [all-cases page](text-all-cases.md).
+
+## How they run
+
+The example `Justfile` invokes `clauz3 prove` against each case. `_fail`
+cases are wrapped so a non-zero exit is the expected outcome.
+
+{{ include_file("examples/text/Justfile") }}

docs/explanation/background.md

@@ -88,17 +88,134 @@ The mechanism differs:
 - The deployment is governed by an environment contract: enforcement is only as
   sound as the facts the environment promises to publish.
 
-`clauz3` currently proves a single Python program before execution. FORGE
-enforces individual decisions during execution. Those designs are not
-substitutes. A static contract proof gives the user a concise permission
-artifact and avoids partial side effects; runtime enforcement gives defense in
-depth when execution drifts from the proved model.
+`clauz3` proves a single Python program before execution; that *static* proof
+is its distinctive layer. FORGE-style policy enforcement decides individual
+actions during execution. Those designs are not substitutes. A static contract
+proof gives the user a concise permission artifact and avoids partial side
+effects; policy-monitor runtime enforcement gives defense in depth when
+execution drifts from the proved model.
+
+Note this comparison is about *policy* enforcement, not about whether clauz3 has
+any runtime checks at all — it does. The trusted layer's deal preconditions and
+effect markers are enforced at runtime regardless of the proof (see
+[Concepts: static proof vs runtime](concepts.md#static-proof-vs-runtime)). What
+clauz3 lacks, relative to FORGE, is a reference monitor evaluating a policy over
+the agent's actions as they happen.
+
+## Guardians
+
+Meijer, *Guardians of the Agents: Formal verification of AI workflows*
+([ACM Queue 23(4), July–August 2025](https://queue.acm.org/detail.cfm?id=3762990);
+Communications of the ACM, January 2026;
+[doi:10.1145/3777544](https://doi.org/10.1145/3777544)), proposes a
+**generate → verify → execute** discipline for agents, with an open-source
+implementation at
+[`metareflection/guardians`](https://github.com/metareflection/guardians).
+Meijer frames it as "a safety paradigm rooted in mathematical proof
+verification" and an extension of Java/.NET **bytecode verification** to agentic
+computation — the same "complexity in production, verification stays simple"
+asymmetry that motivates proof-carrying code above.
+
+The core argument is that prompt injection has the same root cause as SQL
+injection: code (instructions) and data (content) are not separated, so the fix
+is the same. Instead of letting the model call one tool, read the result, and
+then decide the next side-effecting action, the model emits a complete
+structured **workflow** *up front* — a JSON AST of steps whose arguments are
+**symbolic references** (string result bindings such as `"emails_fetched"`,
+rendered `@emails_fetched` in the literate explanation; modeled as `SymRef` in
+the implementation) rather than concrete values. The plan is authored from the
+goal and tool specs alone, before any concrete (possibly attacker-controlled)
+data exists, then verified against a security policy, and only then executed.
+Because the code is fixed before the data arrives, malicious content in inbox
+data, tool results, *or tool descriptions* cannot introduce a new
+side-effecting step; anything unexpected is caught at verification and the
+workflow is rejected.
+
+The paper's running example is an email exfiltration: a malicious inbox message
+instructs the agent to silently forward a summary to `it@othercorp.com`.
+Verification draws on:
+
+- **Source-sink / taint analysis** — a policy forbidding data flow from
+  `fetch_email`'s result to `send_email`'s `body` when the `to` argument is
+  outside an allowlist. Meijer suggests a CodeQL path query or SemGrep; the
+  implementation carries this as its own `TaintRule` with provenance labels and
+  sanitizers.
+- **Security automata** — a finite state machine over the tool-call sequence
+  that rejects on reaching an error state (the paper's figure 2 forbids sending
+  to external domains). Meijer introduces this as a *runtime* monitor; the
+  implementation also evaluates it at verification time.
+- **Z3 / Dafny over pre/post/frame conditions** — including a careful treatment
+  of the **frame problem** (McCarthy & Hayes, 1969): a naive postcondition for
+  "delete foo.txt and bar.txt" is also satisfied by `delete_file("*.txt")`, so a
+  **frame condition** ("files not matching the pattern are unchanged") is needed
+  before the over-broad plan fails to verify.
+
+Meijer gives three reasons to verify first: prevention rather than detection,
+**eliminating the need for rollbacks** (only verified workflows run, so there is
+no partial side effect to undo), and automation. The middle reason is the same
+transactional argument `clauz3` makes for static proof over runtime monitors
+(see [static proof vs runtime](concepts.md#static-proof-vs-runtime)).
+
+The shared ground with `clauz3` is substantial: both reject unsafe behavior
+*before* side effects run, both make the tool/effect trust boundary explicit,
+both compile to Z3, and both replace ad-hoc natural-language promises with a
+checkable artifact. The mechanism differs:
+
+- Guardians verifies a structured **workflow AST** against an operator-defined
+  policy, with the plan fixed before data arrives.
+- `clauz3` proves an agent-authored **Python program** satisfies
+  agent-stated guarantees over trusted effect facts derived by symbolic
+  execution, and treats the proved contract as the user-facing consent artifact.
+
+Where Guardians is ahead, and `clauz3` is not yet:
+
+- a first-class symbolic workflow representation, with the clean code/data
+  separation that gives the prompt-injection story;
+- built-in taint/provenance tracking for source-to-sink data flow;
+- built-in security automata for tool-call *sequences*.
+
+One difference cuts the other way. Meijer needs explicit frame conditions
+because his Z3 obligations describe world state (`fileSystem`), and a model will
+satisfy an under-specified postcondition the cheapest way it can. `clauz3`
+reasons instead over a *closed-world finite trace* of effect facts — an effect
+not in the trace provably does not happen — so contracts like
+`filesystem.only_write_under` or `emails.only` bound the entire effect set
+directly, giving the frame guarantee implicitly for the effects the prover
+tracks (see
+[effect-IR](../todos/effect-ir.md#what-level-fol-datalog-or-the-z3-lisp-syntax)).
+
+`clauz3` does already reason about data it has not seen — its symbolic
+iteration over a trusted query's `list[Row]` return, with `UserRow.email`
+column-binding contracts (see
+[symbolic iteration](symbolic-iteration.md)), is the closest existing analog to
+"plan before the data." What it lacks is the provenance layer needed to say "a
+value that came from `fetch_mail` must not reach `send_email.body`," and any
+notion of effect *order* on which an automaton could run; today the effect facts
+are an unordered set carrying only path conditions.
+
+Where `clauz3` is distinct:
+
+- ordinary Python as the agent-authored surface, rather than a bespoke workflow
+  AST;
+- effect facts inferred from trusted function signatures, rather than
+  hand-declared `ToolSpec`s;
+- a user-facing contract vocabulary (allowlists, absence, uniqueness, counts,
+  sums, filtered counts, joins) and an approval service built around proved
+  guarantees and coverage, not pass/fail policy enforcement;
+- contract *abduction* — the agent proposes the permission artifact (see
+  "Operator Policy Versus Agent-Abduced Contracts" below).
+
+These projects look more like complementary halves than alternatives. The
+concrete synergy tracks — taint/provenance in the fact layer, security automata
+over effect traces, a workflow front-end that lowers into the effect IR, a
+combined approval surface, and a shared email-exfiltration benchmark — are
+collected in [Guardians synergies](../todos/guardians-synergies.md).
 
 ## Operator Policy Versus Agent-Abduced Contracts
 
-FORGE assumes policies are written by humans up front and applied to agents.
-That is the right shape for organizational rules the agent should not be able
-to weaken.
+FORGE and Guardians both assume policies are written by humans up front and
+applied to agents. That is the right shape for organizational rules the agent
+should not be able to weaken.
 
 `clauz3` explores the opposite surface: the agent proposes a contract for a
 specific program, the prover checks that program against that contract, and the
@@ -172,13 +289,18 @@ Provenance facts:
 The current prover records trusted calls as independent effect facts. It cannot
 yet express policies like "this URL must have come from a literal allowlist or
 from a trusted database table." A provenance relation in the fact layer would
-unlock that class of policy.
+unlock that class of policy. Guardians' source-sink taint model is the sharpest
+articulation of this idea; see
+[Guardians synergies](../todos/guardians-synergies.md) for how it could attach
+to the `FactInfo` layer.
 
 Benchmarks:
 
 The repo has examples by proof shape. It does not yet have an adversarial
 benchmark. Even a small corpus of plausible agent-authored programs that try to
-violate contracts would make prover coverage more measurable.
+violate contracts would make prover coverage more measurable. The Guardians
+email-exfiltration scenario is a natural first adversarial case; see
+[Guardians synergies](../todos/guardians-synergies.md#track-5-shared-examples-benchmark).
 
 ## What Is Distinct Here
 

docs/explanation/concepts.md

@@ -162,6 +162,26 @@ proof succeeds, the deal checks at runtime are redundant (but still safe). If
 the proof is skipped or the contract is intentionally weak, deal is still on
 guard at the trusted boundary.
 
+Concretely, the email trusted layer declares `@deal.pre(lambda addr, msg: "@"
+in addr)` on `send_email`. A program that calls `send_email("not-an-email",
+...)` is rejected *statically* by the prover (it cannot discharge the
+precondition). The exact same precondition fires *at runtime* if such a call is
+ever executed:
+
+```pycon
+>>> send_email("not-an-email", "hi")
+deal.PreContractError: addr must contain "@" (where addr='not-an-email', msg='hi')
+```
+
+Same obligation, two enforcement points. See
+[the email example](../examples/email.md#the-runtime-layer-deal-as-a-backstop)
+for the full worked case.
+
+So the only enforcement that is genuinely *not* implemented yet is binding the
+approval **receipt** into this runtime boundary — a trusted effect refusing to
+run without a valid receipt. The deal preconditions, postconditions, and effect
+markers themselves are enforced today.
+
 ## Glossary
 
 - **User** — reviews and consents to contracts; does not read or run code.