Checks

“At most eight calls” is expressible as a formula. It is eight nested operators, and nobody can read it. So counting and repetition are separate primitives that join the same rule set and are reported identically — same verdict shape, same modes, same row in a summary.

createMonitor({
  rules: [SEC_01],
  checks: [
    Checks.loop({ n: 3 }),                          // loop(n=3)
    Checks.duplicateCall({ window: 5 }),            // duplicateCall(window=5)
    Checks.callBudget({ max: 8 }),                  // callBudget(max=8)
    Checks.callBudget({ tool: 'search', max: 2 }),  // callBudget(search, max=2)
  ],
})

Check	Fires when
loop({ n })	The same call with the same arguments repeats n times in a row.
duplicateCall({ window })	The same call with the same arguments repeats within window events.
callBudget({ max })	The run exceeds max tool calls.

Each takes an optional tool to scope it to one tool, and the same id, description and mode options a rule takes. tool accepts the tool itself as well as its name:

Checks.callBudget({ tool: queryMetrics, max: 2 })

which is the safer form wherever the symbol is in scope.

What “the same call” means

Repetition keys on the call’s signature: its name plus a hash of its arguments. That is what makes the distinction worth having — an agent that queries three different services three times is working, and an agent that queries the same service three times with the same window is stuck.

The hash arrives on the event as meta.payloadHash, computed by the adapter where the validated arguments are in hand.

What a refused call does not count towards

Nothing. A denied call never happened, so it contributes no event, no sequence number, and no increment to a budget or a repetition counter. A budget that counted refused work would be counting nothing, and an agent that kept retrying a blocked call would exhaust its budget on calls that never ran. The event model is where that invariant is stated properly.

Why they are invisible to analysis

A counter over whole events is not a proposition, so static analysis does not encode checks into its constraints. It does replay them: a candidate witness that trips a check is rejected, so anything the analyser reports still satisfies the whole spec. That is the right split and it needs nothing from you.