Combinators

The bottom layer. Everything above is implemented by calling these, so a rule written here is not a different kind of rule — it is the same tree, assembled by hand.

LTL.always(f)              // G f   — the root operator; a rule holds at every event
LTL.not(f)                 // !f
LTL.and(f, g)              // f & g
LTL.or(f, g)               // f | g
LTL.implies(f, g)          // f -> g

LTL.prev(f)                // Y f   — f held at the previous event; false at the first
LTL.once(f)                // O f   — f has held at some point up to now
LTL.historically(f)        // H f   — f has held at every event up to now
LTL.since(f, g)            // f S g — g held, and f has held at every event after it

LTL.next(f)                // X f   — f holds at the following event
LTL.eventually(f, { within: 5 })  // F<=5 f

Written out, SEC_01 from your first rule is:

const SEC_01 = {
  id: 'SEC-01',
  description: 'restartService may not run before queryMetrics has returned',
  formula: LTL.always(LTL.implies(P.toolCall('restartService'), LTL.once(P.toolResult('queryMetrics')))),
  mode: 'deny' as const,
}

Past and future are not symmetric

The past operators need no bound. once, historically, prev and since fold over what has already happened, in a fixed amount of state — one boolean each, updated per event. There is no history buffer, because the recurrence is the history.

The two future operators are bounded on purpose. The engine watches a finite prefix of a run, so an obligation has to be able to expire: eventually(f, { within: k }) opens a countdown that is either discharged or fails. An unbounded F would leave a rule permanently undecided, which is not a verdict.

This asymmetry is the single most useful thing to know about writing rules here. Properties phrased about the past are cheap and always decidable; properties phrased about the future cost a window you have to choose. Where you can phrase a property either way, phrase it about the past.

What construction refuses

Three structural rules, each throwing a ValidationError that names the path to the offending node.

always may only appear at the root. A property that holds at every event is the shape a rule already has. A nested always would mean something different from what almost everyone writing one intends.

eventually requires within. There is no unbounded F.

A future operator may not sit inside a past one. O (X f) asks whether something that has not happened yet already happened, which is not a question.

These fire at construction rather than at evaluation, so a malformed rule fails when the module loads rather than halfway through a run.