Artifacts

ltl check writes two kinds of file, both stamped formatVersion: 1. They are the contract between the checker and anything that reads its output — the demo on this site, a dashboard, a bot that comments on a pull request.

<trace>.verdicts.jsonl

One JSON object per line: the full verdict stream for one trace, in the order the monitor produced it.

type VerdictEvent = {
  runId: string
  seq: number
  rule: { id: string; description: string }
  status: 'satisfied' | 'violated' | 'pending' | 'unresolved'
  leaning?: 'satisfy' | 'violate'
  cause?: { event: TraceEvent; subformula: string }
  mode: 'observe' | 'deny' | 'suspend' | 'abort'
}

Three things about reading this stream:

Verdicts are emitted on transition, not per event. A rule’s status at an event is whatever the most recent verdict for it said, starting from satisfied. A rule with no verdicts at all held throughout.

The last verdicts carry the last event’s seq. End-of-run resolution is reported at the position of the final event, so several verdicts can share a seq. Folding the stream in order gives the right answer: the last value at a position wins, and the result agrees with the matrix.

leaning appears only on pending. It is the presumption — which way the obligation would fall if the run ended here. unresolved appears only after the run has ended.

cause.subformula is always a substring of the rule’s printed form, so it can be located and highlighted in the text without guessing. cause.event is the whole event that caused the failure, which is why a verdict stream is readable on its own without the trace beside it.

summary.json

type Summary = {
  formatVersion: number
  rules: readonly RuleManifestEntry[]
  traces: readonly TraceManifestEntry[]
  matrix: { rules: readonly string[]; traces: readonly string[]; cells: readonly (readonly VerdictStatus[])[] }
  counts: Record<VerdictStatus, number>
  contentHash: string
}

rules

type RuleManifestEntry = {
  id: string
  description: string
  mode: 'observe' | 'deny' | 'suspend' | 'abort'
  text: string           // the printed form, always present
  formula?: FormulaJson  // the serialized form, when the rule has one
}

Native checks appear here too, with their label as text. mode is the mode the engine would actually enforce — read from a monitor rather than recomputed, so it accounts for onViolation and enforce. formula is absent for a rule written with a custom predicate, which is code rather than data; text identifies it either way.

traces

type TraceManifestEntry = {
  id: string
  runId: string
  events: number
  outcome: 'completed' | 'errored' | 'canceled'
  verdicts: string   // path to this trace's verdict stream, relative to summary.json
}

verdicts resolves from wherever summary.json landed, including when the streams sit beside their own traces in different directories. id is unique within a summary: two traces called run.jsonl in different directories are named apart, because the id keys the verdict streams.

outcome is read from the trace’s own closing event. A trace with no run.finish counts as canceled.

matrix

cells[ruleIndex][traceIndex] is that rule’s terminal status for that trace, with rules and traces giving the axes. This is the same value the corresponding verdict stream ends on, and any consumer that links a cell to an event depends on that agreement.

counts

Over matrix cells rather than over the verdict stream: “how many rule-and-trace pairs went wrong”, not “how many transitions were emitted”. A long trace does not look worse than a short one.

contentHash

sha256: over the rule manifest and every trace. It changes when a trace changes, when the rule set changes, and when a rule keeps its id but changes meaning — so verdicts that no longer match their inputs are detectable rather than silently stale.

Compatibility

formatVersion is stamped on both artifacts and exported as FORMAT_VERSION. A reader should check it and say so when it does not recognise the value, rather than rendering half a document that looks authoritative.

Fields may be added within a version. A reader should ignore ones it does not know — that is how a rule set written against a newer adapter still loads on an older engine.