verify

ltl analyze verify rules.ts --workflow workflow.ts

A declared graph is finite, so this one needs no solver: every step order the declaration permits is walked, turned into a real trace, and run through the same engine a live run would use. A violation is reported with the step order that produces it.

  violated     STEP-01 is broken by the step order ingestAlert → restartService → queryMetrics → closeIncident
  out-of-scope SEC-01 depends on tool.call, which a declaration does not determine; monitor it at run time

Verify what is static; monitor what is dynamic

A declaration determines which steps run and in what order. It says nothing about which tool an agent will pick or whether a human will be asked, so a rule mentioning anything outside the step structure is reported as out of scope rather than quietly marked clean.

That distinction is the whole value of this command. A rule that the structure guarantees does not need to be enforced at runtime; a rule the structure cannot see must be.

Note the first finding above: a parallel that merely permits the wrong order fails. A declaration that allows a bad interleaving is a declaration that will eventually produce one.

Branching time: CTL over the workflow graph

A runtime monitor observes exactly one future — the one that happened — so over a trace, CTL’s path quantifiers collapse and the logic degenerates into LTL with extra syntax. Branching time needs a model of all possible behaviours, and analysis manufactures one: the workflow step graph, whose branch, parallel and loop constructs make it a Kripke structure.

CTL over that graph expresses what a linear rule structurally cannot. AG EF notify — notify remains reachable from every reachable state, possibility rather than inevitability. AG(escalate -> EF resolve) — resolution never foreclosed.

Reachability.alwaysReachable('notifyChannel')             // AG EF stepStart(notifyChannel)
Reachability.neverForeclosed('escalate', 'closeIncident')  // AG(stepStart(escalate) -> EF stepStart(closeIncident))

Layer 1 is the CTL namespace — CTL.AG, CTL.EF, CTL.AF, CTL.EG, CTL.AX, CTL.EX, CTL.AU, CTL.EU — over the same propositions and boolean connectives.

Quantified rules are a static-analysis fragment only. createMonitor rejects them at construction with a pointer here. The static fragment sees step structure and step identities, never payloads and never the agent’s runtime tool choices; a payload matcher under a quantifier is rejected with instructions to move that condition to a runtime rule.

The soundness stance

Load-bearing, and worth reading before trusting a result. The extracted graph over-approximates behaviour: every edge is treated as takeable, though runtime conditions may never enable some.

• AG f verdicts are sound — holds on the model implies holds on every real run.
• EF f verdicts are possibilistic — the structure permits it; runtime conditions may still prevent it.

Reports label universal and existential verdicts accordingly, and the CLI’s human output says so in one line per result that rests on an existential.

Two modelling conventions

Every terminal node receives a self-loop, because CTL semantics assumes a total transition relation; reports name the convention. And parallel arms are modelled as sibling regions without interleavings — the extractor warns whenever a parallel block exists, and cross-arm ordering properties are out of scope.

Where the graph comes from

Extracted from the committed workflow through the Mastra adapter, or supplied directly as nodes, edges and an initial node via graphFromDescription — which is also the seam that needs no workflow engine at all.