guardians-lemmascript

A LemmaScript verification of the core safety argument behind Guardians (Erik Meijer, "Guardians of the Agents", CACM Jan 2026): an agent's tool workflow is checked before it runs so that tainted data from a source tool can never reach a sink parameter. Guardians itself is Python; this is a greenfield TypeScript core whose proofs are generated by lsc and discharged by Dafny. The Python repo serves as the reference oracle, not a porting target.

What is verified

Tools' source/sanitizer behaviour is always passed as higher-order parameters, so every theorem holds for any assignment.

src/taint_core.ts — taint over a workflow, single boolean label

• taintMonotone — more incoming taint can only mean more outgoing taint; taint is never lost except through a sanitizer.
• noSanitizerKeepsTaint — without a sanitizer downstream, tainted data stays tainted: a fetch(source) → send(sink) pipeline is provably flagged.
• endSanitizerClean — a sanitizer (redact) as the final step clears taint: the fix is accepted, and for a real reason, not vacuously.
• workflowSound — with conditionals (Block = tool | cond), the static check cannot know which branch runs, so it over-approximates by unioning both. This proves the over-approximation is sound: for any branch choice, a concrete run that ends tainted was already flagged statically — a clean verdict rules out a tainted sink on every path. (Composes per-block soundness with workflowAbstractMonotone, which leans on taintMonotone.)

src/wf_core.ts — nested conditionals over the real recursive AST

workflowSound above models a conditional's branches as linear pipelines. This file removes that restriction: a workflow is a recursive datatype Wf = done | tool(tool, rest) | cond(thenB, elseB, rest) where a conditional's branches are themselves full workflows, so conditionals nest to any depth (recursion is structural, as in examples/preorder.ts).

• taintWfSound — the over-approximation soundness, re-proved over this faithful AST: for any branch-choice function, a concrete run that ends tainted was already flagged statically — at every nesting depth. Structural induction composing branch soundness with taintWfMonotone over the continuation.
• leaksWfSound — the actual taint rule ("does tainted data reach a sink?"), not just taint flow, proved sound over the nested AST. This is the taint decision the adapter calls with a proof behind it.
• verifyWfSound — the capstone: a single unified static check (verifyWf = no taint leak ∧ no automaton target reachable) rules out, on every concrete path, both a leak to a sink and an automaton error. The automaton here is the demo's shape (a target tool under a symbolic guard); since "target reachable" is tool membership, it decomposes over branches with no state-tracking. Composes leaksWfSound and reachesTargetWfSound.
• leaksSrcFaithful — the marshalling proof. The adapter receives a workflow as a flat step-list; buildWf collapses it (with nested conditionals) onto this Wf AST. This proves that collapse is verdict-faithful at any depth: leaksWf(buildWf(list)) == leaksSrc(list) (the source list's own leak rule). It lives in the same module as leaksWfSound, about the same leaksWf, so the two compose with no copy to drift — source workflow → marshal → check is backed end-to-end (taintSrcFaithful carries the branch-union taint).

src/loop_core.ts — unbounded loops (a fixpoint over-approximation)

Guardians' AST also has a loop: a body that runs some number of times. Unlike a conditional (a finite branch union), a loop needs a fixpoint argument. The key fact: for a single taint bit with bodyTaint monotone, sat = t0 ‖ bodyTaint(t0) is a one-step pre-fixpoint (bodyTaint(sat) ⟹ sat), so it soundly bounds the taint after any iteration count — no iteration-to-fixpoint required.

• loopExitSound — the taint after running the body n times is bounded by sat, for every n (induction on n, via bodyMonotone + the pre-fixpoint).
• loopLeakSound — if any iteration leaks, the body leaks from sat; so the static check leaksBody(sat, body) rules out a leak at every iteration count.

src/prov_core.ts — per-source provenance (the real Guardians analysis)

Taint becomes a set of source labels in a value's lineage (represented per-label, so the set is the family over lbl; introduces/sanitizes take the label). A rule fires only for a source actually present; sanitizers are per-rule.

• introducedSourcePresent — a source introduced anywhere with no sanitizer downstream reaches the end (the rule fires for genuinely-present sources).
• joinFlagsContributingSource — the payoff: a join (a tool consuming several inputs) is tainted by a source if any input carried it, so taint propagates transitively through multi-input tools. The per-label structure is also why sanitizing one source leaves the others intact.

src/automaton_core.ts — security automata

Guardians' other check: a policy is a finite automaton over the tool-call sequence, with guarded transitions to error states. At verification time a guard's truth is unknown (symbolic args), so the static analysis explores both outcomes; the concrete run follows the actual guard. Guards are HOF parameters, so there is no condition DSL.

• automatonSound — the static reachability over-approximates the concrete one: if any concrete run reaches an error state, the static checker (exploring all guard choices) already found a path to error.
• automatonSafeVerdict — the usable form: a clean static verdict means the concrete run never reaches an error state, for any data. This is what lets Guardians admit a workflow before it runs.

What a passing verdict guarantees — and what it doesn't

The headline theorem is verifyWfSound in src/wf_core.ts (its inductive proof is the additions-only diff in src/wf_core.dfy over the generated src/wf_core.dfy.gen). Its //@ ensures, in full:

verifyWf(introduces, sanitizes, isSink, isTarget, t0, wf)
  ==> ( !leaksWfConcrete(introduces, sanitizes, isSink, chooseThen, t0, wf)
        && !reachesTargetWfConcrete(isTarget, chooseThen, wf) )

with all of introduces, sanitizes, isSink, isTarget, chooseThen, t0, wf universally quantified. In words: for every workflow, every assignment of which tools are sources / sanitizers / sinks / guarded targets, every starting taint, and every way the conditionals branch at runtime (chooseThen) — if the static check verifyWf passes, that execution neither feeds tainted data into a sink nor fires a guarded tool. Quantifying chooseThen makes this hold on every path.

Every property in this repo follows the same triple, so the code is easy to read:

role	functions (e.g. for the leak rule)
abstract checker (runs on the plan)	leaksWf, reachesTargetWf
concrete semantics (what a run does)	leaksWfConcrete, reachesTargetWfConcrete
soundness lemma (abstract ⊇ concrete)	leaksWfSound, reachesTargetWfSound

The //@ ensures on a function in the .ts is the claim; the inductive proof lives in the matching .dfy (the lines it adds over .dfy.gen). It holds for all inputs — every workflow, policy assignment, and path.

Two boundaries are worth knowing:

• Scope. Taint (over nested conditionals and loops) and a single-target automaton are modeled; Guardians' Z3 preconditions/frame conditions, allowlist, and scope checks are not. leaksWf is order-based taint — a sound over-approximation of data-flow taint (it can flag more, never less).
• The adapter. A real Workflow/Policy reaches the proved cores through src/verify.ts. Its marshalling onto the Wf AST is now proved verdict-faithful (leaksSrcFaithful), and the taint/automaton decisions are the proved functions — so what stays trusted is only the 1:1 Step[]→datatype transcription, string→int interning, and the taintPrecise lineage tracing: a shape copy with no decisions. compare/ differentially tests our verdict against the real Python Guardians (testing, alongside the proofs).

Verify

for f in taint_core prov_core automaton_core wf_core loop_core; do
  node ../LemmaScript/tools/dist/lsc.js regen --backend=dafny src/$f.ts
done
../LemmaScript/tools/check.sh dafny

Running it, and diffing against Python

src/verify.ts is a small adapter: it maps a Guardians-style Workflow/Policy onto the verified cores and returns a verdict in the same shape as Python's guardians.verify(). The taint and automaton decisions are the proved functions (provAfter, leaksWf, reachesErrorAbstract), and the marshalling onto the Wf AST is proved verdict-faithful too (buildWf / leaksSrcFaithful). What remains plain glue is the 1:1 Step[]→datatype transcription (buildSrc), string interning, and the taintPrecise lineage tracing — a shape copy with no decisions.

                Guardians-style Workflow (steps: Step[]) + Policy
                                     |
  +----------------------------------------------------------------------+
  |  src/verify.ts — ADAPTER  (trusted glue: shuffles shapes, makes no    |
  |                            taint/automaton decision of its own)       |
  |    idOf      tool-name string -> int                                  |
  |    buildSrc  Step[] -> SrcList   (1:1 transcription)                  |
  |    lineage   tools transitively feeding a sink argument               |
  +------+--------------------+---------------------------+---------------+
         | lineage chain      | SrcList                   | tool-id seq
  =======|====================|===========================|==== TRUST BOUNDARY ==
         v                    v                           v
    provAfter           buildWf -> Wf              reachesErrorAbstract
    (prov_core)         (wf_core)                  (automaton_core)
    PROVED sound        PROVED faithful            PROVED sound
         |              (leaksSrcFaithful)                |
         |                   |                            |
         |              leaksWf  (wf_core)                |
         |              PROVED sound (leaksWfSound)       |
         v                   v                            v
    taintPrecise          taintWf                     automaton
    data-flow taint,   proved-sound over-           finite-automaton
    matches Python     approx (over-flags,          check, matches
                       never misses)                Python
         |                   |                            |
         +-------------------+----------------------------+
                             v
       Verdict { ok = !(taintPrecise || automaton),  taintPrecise,
                 taintWf,  automaton }
                             v
       compare/diff.sh  --  diffed scenario-by-scenario against
                            real Python  guardians.verify()

  Above the boundary: trusted glue, small enough to audit by eye.
  Below: machine-checked by Dafny (59 proof obligations, 0 errors).

The adapter reports two taint verdicts: taintPrecise (binding provenance, via provAfter) and taintWf (the proved leaksWf over the real AST).

compare/diff.sh runs our verify() and the real Python guardians.verify() on five email-agent scenarios (incl. a nested-conditional leak and a source-then- literal-send) and compares:

# one-time: cd ../guardians && python3 -m venv .venv && .venv/bin/pip install -e .
./compare/diff.sh

Results: taintPrecise and automaton match Python exactly on all five, including the nested-conditional case (so wf_core's nesting is validated against the reference). The proved taintWf is a sound over-approximation: it flags every taint Python flags, and is conservatively stronger on exactly one scenario (fetchThenLiteralSend — a sink that runs after a source but does not consume its data). Python additionally reports a precondition category on external sends — the Z3 check this project does not model (a coverage gap, not a disagreement).