ltl

LTL runtime verification for Mastra agent and workflow traces — a logic analyzer for agents. State a temporal property once and get three things from it: the ability to stop a violating side effect before it happens, live verdict telemetry while runs execute, and verdicts over recorded traces in CI.

const rule = Presets.requireBefore('restartService', 'queryMetrics', { mode: 'deny' })
// G(toolCall(restartService) -> O toolResult(queryMetrics))

That one rule refuses the call at the interception point and hands the agent the reason, catches the same thing in CI over recorded traces, and lights up the step it stopped in the demo. Nothing is restated in three places.

Quickstart

npm install @rhysbalevicius/ltl-core @rhysbalevicius/ltl-mastra
npm install --save-dev @rhysbalevicius/ltl-cli

Write the property once:

import { Checks, LTL, P, Presets } from '@rhysbalevicius/ltl-core'
import type { MonitorSpec } from '@rhysbalevicius/ltl-core'

export const SPEC: MonitorSpec = {
  rules: [
    Presets.requireBefore('restartService', 'queryMetrics', { id: 'SEC-01', mode: 'deny' }),
    { id: 'SAFE-01', description: 'purgeLogs never runs', formula: LTL.always(LTL.not(P.toolCall('purgeLogs'))), mode: 'observe' },
  ],
  checks: [Checks.callBudget({ max: 8 })],
}

Put it in front of the tools your agent already has:

import { createMonitor } from '@rhysbalevicius/ltl-core'
import { createTraceSource, guardTools } from '@rhysbalevicius/ltl-mastra'

const monitor = createMonitor(SPEC)
const source = createTraceSource({ runId: 'run-1' })

const guarded = guardTools(monitor, { queryMetrics, restartService, purgeLogs }, {
  source,
  onDecision: (decision) => logger.warn('ltl', decision),
})

SEC-01 now refuses a restart the agent cannot justify and returns the reason as the tool's result, so the model reads it and does the missing work. onDecision fires once per interception — including for the calls that were refused and therefore never happened — which is where a deployment's verdicts belong.

The documentation walks the same path with the output at each step, and carries the full consumer API reference.

Enforcement modes

A rule carries a mode, and the mode is the only thing that changes between watching and stopping.

Mode	At the interception point	Use it when
observe	The call runs; the verdict is recorded.	A rule is new and has to earn trust before it is switched on.
deny	The call is refused and the violation is returned as the tool's result.	An agent could reasonably do something else instead. This is the mode that composes with a model.
suspend	The workflow pauses through its own suspension primitive; a human's answer resumes it.	A person has to decide, and the decision may take longer than the process lives.
abort	The run is cancelled and the guard throws where the side effect would have been.	Nothing downstream should happen, and nobody is going to be asked.

A refused call leaves no event in the trace, because it never happened. That is what makes budgets and repetition checks count real work — and it is why a rule that is only observing is the one that shows up in CI.

Writing a rule

Three layers, one AST. Each is the implementation of the one above it rather than a description of it.

// Layer 3 — English presets
Presets.requireHumanBefore(P.stepStart('applyRemediation'), { mode: 'suspend' })

// Layer 2 — Dwyer patterns
Patterns.response(P.toolCall(), P.toolResult(), { within: 4 })

// Layer 1 — combinators
LTL.always(LTL.not(P.toolCall('purgeLogs')))

Counting and repetition properties are native checks rather than formulas, and they join the same rule set:

Checks.loop({ n: 3 })
Checks.callBudget({ max: 8 })

Guarding a run

const monitor = createMonitor({ rules: [SEC_01, HITL_01], checks: [Checks.callBudget({ max: 8 })] })

const tools = guardTools(monitor, { queryMetrics, restartService })
const workflow = guardWorkflow(monitor, incidentWorkflow)

const run = await workflow.createRun()
observeRun(monitor, run, { guardedSteps: guardedStepIds(workflow), onFinish: report })

observeRun fills what the guards cannot see — the boundaries of unguarded steps and the run's own ending — and onFinish is where end-of-run resolution arrives, which is the only place unresolved can come from.

Why temporal logic

Most rules worth writing are about order, not about one event — metrics read before a restart, no edit after publish, a reply within k steps. Linear temporal logic is the standard notation for that: G at every point, O at some earlier point, F<=k within the next k events.

• Safety — nothing bad happens. Broken at one identifiable event, and that event is the one before the side effect. This is the family deny and suspend above can stop.
• Liveness — something good eventually happens. No finite trace refutes it, so every eventually here carries a bound: run the clock out and it is a violation, get killed before the deadline and it is unresolved.

Either has to be checked while the agent runs, because the order of its actions is the output, not the source.

Static analysis

ltl analyze reasons about a rule set before anything runs, using a solver that never touches the runtime path. It lives in its own optional package because it carries one.

ltl analyze vacuity rules.ts          # rules that pass for the wrong reasons
ltl analyze consistency rules.ts      # whether the rules can all hold at once
ltl analyze witness rules.ts SEC-01   # the shortest trace that breaks one rule
ltl analyze verify rules.ts --workflow workflow.ts

Vacuity separates three ways a rule can be worthless: one no trace satisfies is broken, one whose antecedent the other rules make impossible holds vacuously, and one the rest of the set already forces adds nothing. Consistency answers whether the rules can hold together, and names the smallest group that cannot when they cannot. Witness synthesises the shortest trace that breaks one rule while every other rule holds — a test fixture, generated. Verify walks every step order a workflow declaration permits and checks the rules against each one; a rule that depends on which tool an agent picks, or on whether a human is asked, is reported as out of scope rather than quietly marked clean.

Every trace these produce is replayed through the engine before it is reported. A mistake in the encoding becomes a refusal rather than a wrong answer, which is what lets the analysis say "this rule can never fire" and be believed.

Verifying a rule set

The property is code, so the first place to check it is the test suite you already have. checkTrace folds the same monitor over a list of events and hands back the verdicts, with no file and no binary in the way:

expect(checkTrace(SPEC, events).filter((verdict) => verdict.status === 'violated')).toEqual([])

ltl check is for what outlives one test: a corpus of runs committed beside the rules, re-checked whenever the rules change. It answers a question about the rules rather than about a run — does this edit still catch what it caught, and still pass what it passed — which is why its traces are fixtures and why the recorder that captures them lives under @rhysbalevicius/ltl-mastra/testing rather than beside the guard. A deployment has no use for it: what a running system wants is the verdict at the moment it is decided, and onDecision is where that arrives.

ltl check is lenient by default: an obligation a killed run left open surfaces as unresolved in the summary but does not fail the build, because a run that simply stopped is not evidence that a property broke. --strict promotes it.

ltl check traces/ --rules rules.ts --out artifacts/

Exit codes: 0 clean, 1 violations (and unresolved under --strict), 2 usage or configuration error. Lint warnings go to stderr and never affect the exit code.

Two artifacts come out: one <trace>.verdicts.jsonl per trace, and a summary.json carrying the rules manifest, the rules-by-traces matrix, per-status counts, and a content hash over the rules and every trace so verdicts that no longer match their inputs are detectable. Both are documented under artifacts.

Packages

Package	Purpose
@rhysbalevicius/ltl-core	The engine. Pure TypeScript, zero runtime dependencies: event model, propositions, formula combinators, presets, native checks, monitor transition, verdict types.
@rhysbalevicius/ltl-mastra	The guard. The only published package that imports Mastra: tool wrapping, workflow-step wrapping, run observation, JSONL trace recording.
@rhysbalevicius/ltl-cli	The ltl binary. ltl check over recorded traces for CI, and ltl analyze when the analysis package is installed.
@rhysbalevicius/ltl-analyze	Optional static analysis over rule sets: vacuity, consistency, witness synthesis, and verification against a declared workflow graph. Carries z3, dynamically imported, CI-time only.
apps/demo	The demo: the agent and the workflow as graphs, with runs replayed or executed live against them. Not published.
apps/site	The documentation site, which embeds the demo. Not published.
examples	The scenarios the demo draws: the incident-response workflow, the on-call responder, the recorded corpus, and the live server. Not published.

Development

pnpm install
pnpm run ci        # dependency rule, typecheck, tests, build, packaging

pnpm demo          # record the corpus and check it, in the terminal
pnpm demo:web      # the demo page, replaying the recorded corpus
pnpm demo:live     # the same page with live runs, given ANTHROPIC_API_KEY
pnpm site          # the documentation site, with the demo embedded

pnpm run check:deps enforces the package dependency law: core depends on nothing, mastra/cli/analyze depend only on core, Mastra imports are confined to packages/mastra and examples, z3 to packages/analyze, React Flow and Tailwind to apps/demo and apps/site, and analyze is reachable only by dynamic import. pnpm run check:package packs each published package and verifies every path its manifest advertises is really in the tarball.

The recorded corpus is produced by scripted runs, so it is the same every time it is replayed and needs no credentials. pnpm demo:live puts a real model behind the same guards, which is where the order of events stops being something anyone wrote down.

The demo

An incident-response workflow and an on-call responder, drawn as graphs, with recorded runs replayed through them and a live mode that puts a real model behind the same guards. Nodes light up as a run moves; a refused call turns the path it reached for red; a rule pauses the step it guards and waits for a human. Run it locally or open the demo.

License

MIT