Extending the engine

Read how it works first.

Adding a preset

The cheapest change: a preset is a named call to a pattern. Nothing else in the engine learns about it.

In packages/core/src/presets.ts:

requireAfter: (action: ToolRef, follow: ToolRef, options: PresetOptions = {}): Rule => {
  const a = resolve(action, (name) => P.toolCall(name))
  const f = resolve(follow, (name) => P.toolCall(name))
  return rule(
    'require-after',
    [a.label, f.label],
    `${f.label} must run after ${a.label}`,
    Patterns.response(a.formula, f.formula, { within: DEFAULT_WITHIN }),
    options,
  )
},

rule generates the id and applies the caller’s overrides; resolve is what lets a caller pass either a tool name or a proposition. Enforcement is never switched on in a preset — a mode arrives only when the caller asks for one.

Add a test in test/presets.test.ts asserting the printed form and the generated id, plus one satisfying and one violating trace. The printed form is what a reader sees in a report, so pin it exactly.

Adding a pattern

A pattern composes combinators. In packages/core/src/patterns.ts:

alternation: (first: FormulaInput, second: FormulaInput): Formula =>
  LTL.always(LTL.implies(LTL.atom(second), LTL.once(LTL.atom(first)))),

Two things to get right. Build it by calling the combinators rather than constructing AST nodes by hand, so construction-time validation applies. And decide whether the pattern needs a window: anything that says “eventually” does, because the engine watches a finite prefix.

Add it to test/patterns.test.ts with the printed form and both outcomes. The helper there throws when a rule produces no verdict at all, so a pattern that reports nothing fails rather than passing as satisfied.

Adding a native check

A check is a counter with its own state, folded into the monitor as an ordinary property. Use one when the property is about how many or how often — expressing that in temporal logic produces a formula nobody can read.

In packages/core/src/check.ts:

toolBudget: (options: ToolBudgetOptions): Check => {
  const { tool, max } = options
  return define<{ calls: number; violated: boolean }>({
    family: 'tool-budget',
    parts: [tool, String(max)],
    label: `toolBudget(${tool}, max=${max})`,
    description: `at most ${max} calls to ${tool} in a run`,
    options,
    initial: { calls: 0, violated: false },
    step: (state, event) => {
      if (!isCall(event, tool)) return state
      const calls = state.calls + 1
      return { calls, violated: calls > max }
    },
  })
},

define handles the id, the verdict shape and the mode. Your step must be pure and must return a new state — the monitor’s purity invariant runs through it, and a check that mutates will break peek.

Checks are invisible to static analysis: a counter is not a proposition, so packages/analyze ignores them when reasoning and replays them when validating a witness. That is the right split and it needs nothing from you.

Add it to test/checks.test.ts, and add it to the property-test spec in test/monitor.test.ts so the purity invariant covers its counters too.

Adding an operator

The expensive one. An operator touches the type, the constructor, the validator, the printer, the compiler, the transition, the serializer and the analysis encoder — and every one of those is load-bearing.

1. formula.ts — the node type, and add its kind to FORMULA_KINDS.
2. ltl.ts — the constructor. Decide what it refuses: always is root-only, eventually demands a bound, and a future operator may not sit inside a past one. If yours is a future operator, add it to FUTURE_KINDS; past, PAST_KINDS.
3. describe.ts — how it prints, including when it needs parentheses. Attribution reads the printer’s spans, so a subterm that prints one way at the top level and another nested will break highlighting.
4. automaton.ts — the transition. Past-definite operators get a recurrence over one boolean; bounded-future operators get an obligation with a residual and a countdown. If yours is neither, it does not belong in this engine.
5. schema.ts — the serialized form and the parse case, so it survives a round trip through JSON.
6. packages/analyze/src/encode.ts — the constraint form. Without it the analyses will be wrong about any rule using the operator, rather than silent about it.

The test that decides whether you got it right is packages/analyze/test/agreement.test.ts: it reads every trace the alphabet can express, at every length up to four, both through the engine and through the constraints, and compares. Add your operator to its formula list. If the two disagree anywhere, one of the two implementations is wrong and you will know immediately.

Then test/describe.test.ts for the printed form, test/schema.test.ts for the round trip, and test/automaton.test.ts for the transition itself.

If the operator is unbounded

Do not add it. F and U without a bound cannot be decided on a finite prefix, and the engine’s entire shape — obligations with countdowns, a verdict at every event, unresolved as a real status — follows from the decision not to have them. Formula progression for unbounded liveness is a deliberate later item, not an oversight.

Before you open a pull request

pnpm run ci

That runs the dependency rule, typecheck, every test, the build and the packaging check. The dependency rule is stricter than it looks: it reads every file in every unit, not just src and test, and it distinguishes static from dynamic imports.