Why order matters

An agent’s order of operations is its output. Not the text it produces — the sequence of side effects it caused, and the sequence of things it read before causing them. A restart that happened before anyone looked at the metrics is a different event from the same restart afterwards, even though the call is identical.

Every guardrail system can answer questions about this call. The interesting properties are about the call in the context of the run, and those are the ones that are awkward to express any other way.

The version without a logic

You can write “restartService requires a prior queryMetrics” as a callback. It looks like this:

let queried = false

onToolResult('queryMetrics', () => { queried = true })
onToolCall('restartService', () => { if (!queried) throw new Error('...') })

That works. It stops being pleasant at the third rule, and it has already lost three things:

The property is not inspectable. You cannot ask whether this rule can ever fire, whether it conflicts with another rule, or what the shortest trace that breaks it looks like — because it is control flow, not a statement. Everything under static analysis exists because a formula is a value.

The state is yours to get right. queried is a variable you reset, or forget to reset, per run. The engine’s version is one boolean per subformula, derived, and partitioned by runId because it has to be.

Blame is a string you wrote. The engine’s version names the subterm that actually failed, and guarantees that name is a substring of the printed rule — so a report can highlight it rather than approximating it.

What the logic actually is

Four past operators and two bounded-future ones. The past operators fold over what has happened in constant state; the future ones open an obligation with a countdown. That is the entire mechanism, and it is the reason the same rule set can run live, replay a file, and be reasoned about by a solver.

The notation is not the point and you never have to write it — the presets name every property people actually want. The point is that a property is a value: something you can print, serialize, check for consistency, generate a counterexample for, and hand to a solver.

What it is not for

Anything that is really a question about one call. “The amount must be under a thousand” is a schema, and a schema is a better place for it. Reach for a temporal rule when the sentence you are trying to write contains the word before, after, until, never again, or within.