witness

ltl analyze witness rules.ts SEC-01

  2 events break SEC-01 while every other rule holds:
      0  tool.call restartService
      1  tool.result

Horizons are tried from short to long, so the fixture is as small as the property allows. Everything the other rules require is asserted alongside, so the trace is one the rest of the set would have permitted rather than a counterexample that could never occur.

ltl analyze witness rules.ts SEC-01 --out fixture.jsonl

writes it as a trace file you can commit.

The two ways to use this

As a review tool. Read the witness for a rule you have just written. If the shortest way to break it surprises you, the rule does not say what you think it says — and reading two events is faster than reasoning about a formula.

As a fixture generator. A rule with no negative case in the corpus is a rule nothing has tested. --out gives you one that is minimal by construction and consistent with every other rule you have.

What makes it trustworthy

The witness is decoded into real events and run back through the engine before it is reported. If the engine does not reproduce the claim, the analysis refuses rather than printing it. That replay is the whole basis on which a solver is allowed to make assertions about a runtime system.