Overview

ltl analyze reasons about a rule set before anything runs. It lives in an optional package because it carries a solver, and the solver is never on the runtime path: a monitor transition is microseconds, a solver call is milliseconds, and watching a finite prefix needs no solver at all.

npm install --save-dev @rhysbalevicius/ltl-analyze

The binary reaches it by dynamic import only when an analysis is asked for. Without it installed, ltl analyze says so in a sentence.

The four questions

ltl analyze vacuity rules.ts
ltl analyze consistency rules.ts
ltl analyze witness rules.ts SEC-01
ltl analyze verify rules.ts --workflow workflow.ts

Findings exit 1; a request that could not be answered exits 2.

vacuity	Which rules pass for the wrong reasons.
consistency	Whether the rules can hold together at all.
witness	The shortest trace that breaks one rule while the others hold.
verify	Which rules a workflow declaration already guarantees, and which it cannot.

What it is honest about

Every trace it reports has been replayed through the engine. A witness is decoded into real events, run through the monitor, and kept only if the engine reproduces the claim. A mistake in the encoding becomes a refusal rather than a wrong answer — which is the only basis on which a linter earns the right to say “this rule can never fire”.

Findings are always real; their absence is not a proof. Regular expressions and custom predicates are not translated into the solver’s language. Each becomes a free boolean, which makes the analysis permissive: it may miss a conflict, and it will never invent one.

The horizon is finite. Everything is decided over traces of a bounded length, sized from the widest window the rules declare, and reported in the output. --horizon N sets it explicitly. A conflict that only appears on a longer trace is one this will not see.

Native checks are replayed, not encoded. A counter over whole events is not a proposition. Checks take no part in the reasoning, but a candidate witness that trips one is rejected, so anything reported still satisfies the whole spec.

As a library

import { consistency, vacuity, verify, witness } from '@rhysbalevicius/ltl-analyze'

const report = await consistency(spec)
if (!report.consistent) throw new Error(`conflicting rules: ${report.conflict?.join(', ')}`)

verify is synchronous; the other three open and close a solver session around the call. The session owns worker threads, so if you drive the lower-level API directly, close it — openSolver() returns { solve, close }, and a process that forgets to call close will not exit.