UX refactor (#52)

* feat(ltl): bound fields on AlwaysFormula and named thunks Add StepBound/Duration/Deadline to AlwaysFormula as the dual of bounded Eventually, give ThunkFormula a Name for stable identity, add ThunkNamed, and surface both in describe() and MarshalJSON. * feat(ltl): negation normal form pass nnf/pushNot rewrite a formula so every Not wraps only a Thunk or Error leaf, dualizing Always<->Eventually and preserving bounds. * feat(ltl): NNF in NewEvaluator, bounded-always, Finalize, collapse Apply nnf on construction, reduce bounded Always symmetric to bounded Eventually (vacuous holds once the window closes), add Finalize to resolve undischarged liveness obligations to Violated at run end, and collapse structurally-identical pending obligations. * test(ltl): property-based NNF laws Lock double-negation identity, Always/Eventually duality with bound preservation, leaf pushdown, and not(always true) reaching Violated. * test(ltl): Finalize, bounded eventually, latch, collapse Property tests for monotonic violation latch and eventually-within violating iff n consecutive false, plus Finalize and collapse cases. * feat(inspect): within clause on always residual node A negated bounded eventually serializes as a bounded always; render its bound instead of dropping it. * feat(ltl): witness violations and (bool,error) predicate thunks * test(ltl): migrate thunk call sites to (bool,error) * feat(ltl): flag thrown-predicate witnesses with IsError * refactor(verifier): replace predicate err side-channel with violation witness * test(verifier): witness API for thrown predicates * feat(trace): witnesses map and skipped-verification marker on Step * feat(runner): thread violation witnesses, finalize, skip marker into trace * test(ltl): lock violation witness reason, IsError, and step * test(verifier): finalize surfaces unmet eventually with witness * fix(ltl): eliminate implies and bounded-always false-negatives Rewrite a -> b to (not a) or b in NNF so a pending temporal antecedent can no longer defer the whole implication and drop a consequent that was false at the current step. Carry a pending inner past a bounded-Always window close instead of dropping it to holds, so a deferred obligation is resolved by a later step or Finalize. * test(ltl): lock implies and bounded-always false-negative regressions * fix(web-runtime): seed PRNG for reproducible runs and align weighted pick * feat(testrun): inject seed into web bundle via SANDERLING_SEED define * test: cover web-runtime seeded PRNG, weighted pick, and seed define wiring * test(spec): add Go math/rand/v2 PCG oracle and golden fixture * feat(spec): bit-exact PCG port of Go math/rand/v2 * test(spec): assert pcg.ts matches the PCG golden fixture * feat(spec): shared input corpus and press-key pools * feat(spec): action-tree types and Host interface * feat(spec): verb support matrix and warn-once helper * feat(spec): deterministic shared action picker * test(spec): verb matrix and warn-once semantics * test(spec): picker draw-order and determinism * refactor(spec): actions.ts returns pure GeneratorNode data trees * refactor(spec): wire from() sampling through the picker rng * feat(spec): shared runtime-entry installs next-action over pick.ts * feat(spec): export LongPress/Scroll/longPresses/scrolls factories * test(spec): assert data-tree shapes for action factories * test(spec): runtime-entry serializeAction wire-contract round-trip * refactor(spec): bridge data-tree nodes to the legacy goja picker tags * fix(spec): web runtime walks the spec's globalThis.actions data tree * test(spec): tolerate legacy bridge fields on builtin nodes * refactor(spec): installRuntime accepts a lazy root resolver The web bundle imports the runtime before the spec, so the action root on globalThis.actions only exists after the spec evaluates. Accept a function form so the goja and web hosts resolve the root per tick. * refactor(spec): web-runtime becomes the WEB Host, delegates to shared picker Delete the duplicate picker (resolveGenerator/pickWeighted/randomTap/ randomInput/randomSwipe/randomPressKey/pickFromArray, the mulberry32 PRNG, and the snake_case serializeAction) plus the __sanderling__ action factory binds. web-runtime now implements Host (platform/seedHi/seedLo from the injected 64-bit seed via BigInt, queryCandidates over the live DOM with a per-tick cache, reportUnsupported) and calls installRuntime so both engines run pick.ts over the same Pcg. Swipe/longPress/scroll follow the verbs.ts matrix instead of silently returning null. Keeps the DOM helpers (selector translation, queryElement, elementHandle, buildState, sanitize, extractors) and the global locking. Net -214 lines (741 -> 527). * test(spec): cover the WEB Host surface and seed precision Replace the deleted-picker tests with Host coverage: platform()==web, seedHi() parsing a 64-bit seed without Number precision loss, seedLo()==0, reportUnsupported warning, the installed next-action/extractor globals, and queryCandidates verb routing + per-tick caching over a querySelectorAll stub. * refactor(spec): picker emits native selector + scroll endpoints, setup precedence * feat(spec): goja runtime entry wires the shared picker over the Go host * feat(bundler): optional RuntimeFile prepends a runtime-entry import via stdin * feat(testrun): bundle the goja runtime entry so the verifier runs the shared picker * refactor(spec): drop the legacy goja bridge fields from action factories * feat(spec): serialize selector-only string targets for the runner to re-resolve * refactor(verifier): one DecodeAction reads the unified flat wire contract * refactor(verifier): goja host + shared picker replace the duplicate Go picker * refactor(runner): decode V8 actions via the unified DecodeAction; wire goja runtime * test(verifier): author specs through the shared picker path * test(runner): bundle authored specs with the goja runtime entry * feat(verifier): collect unsupported verbs for the run report * refactor(runner): collapse WebDriver forks behind ActionSource/ExtractorSource * feat(testrun): surface unsupported verbs in run report * test(verifier): cross-runtime goja/node parity gate on the shared picker * test(verifier): unsupported verbs collected deduped in first-seen order * test(runner): summary reports no unsupported verbs on a clean run * test(spec): golden-fixture cross-runtime parity gate for the node picker Replace the env-driven parity harness with a shared scenario module and a committed golden the node picker asserts independently. The goja side asserts the same golden, so neither runtime invokes the other at test time. * test(verifier): assert goja picker against the same cross-runtime golden Drop the node-subprocess coupling: the goja side now installs a stub __sanderlingHost__ with the fixed candidate list and asserts the committed golden, matching pkg/spec/test/parity.test.ts. * refactor(spec): rename pressKey generator export to pressKeys * refactor(spec): update barrel re-exports for pressKeys * test(spec): update pressKeys generator export name * docs(spec): rename pressKey generator to pressKeys * refactor(spec): extract samplerRng into shared sampler-rng module * feat(spec): add fluent seeded value generators (strings/integers/emails/edgeCaseText) * test(spec): cover fluent value generators determinism and chaining * refactor(bundler): inject globalThis trailer from spec named exports * refactor(bundler): reuse registration trailer in web bundler * test(bundler): cover named-export globalThis registration * feat(spec): add named() to Extracted handle type * feat(web-runtime): named() and cross-extractor read guard * feat(verifier): named() and cross-extractor read guard in goja * test(verifier): cross-extractor read guard and named() * test(web-runtime): export runtime and extractors for tests * test(web-runtime): named() and cross-extractor read guard * refactor(folio): drop manual globalThis trailer (bundler injects it) * refactor(folio): seed txn amounts via integers().between(1,500) * refactor(folio-web): drop manual globalThis trailer (bundler injects it) * fix(folio-web): seed card/txn-type selection via from().generate() for reproducible runs * refactor(folio-web): weight valid generators against edgeCaseText for names/amounts * refactor(folio-web): name extractors so violation witnesses are readable * fix(web-runtime): propagate extractor getter throws and unpoison locked global Stop swallowing getter errors in evaluateExtractors so the cross-extractor read guard aborts loudly, matching goja's PushSnapshot. Make the __sanderling__ lock configurable (still non-writable) so a shared test process can reinstall a fake. * test(spec): install fake runtime via defineProperty to survive locked global * test(web-runtime): assert uncaught cross-extractor read aborts evaluateExtractors * feat(runner): add MaxSteps bound to Options * test(runner): MaxSteps stops after exactly N steps * test(driverpb): drop proto getter round-trip tautology * test(sidecar): drop stub-mode placeholder tautology tests * test(mock): drop default-field-value assertion test * test(ltl): drop Verdict.String tautology tests * refactor(runner): extract RenderSummary for snapshot testing * test(runner): golden snapshots for trace stream and violation summary * feat(web-runtime): capture uncaught errors into state.exceptions * test(integration): add throwing and counter web fixtures * test(integration): add specs for the web fixtures * test(integration): drive web fixtures through the real pipeline in headless Chrome * chore(make): add test-browser target for the Chrome-driven suite * ci: run the Chrome-driven browser suite in a separate job * refactor(test): relocate browser suite to test/browser * refactor(permissions): delete dead internal/permissions package * refactor(test): rename package to browser_test * refactor(sidecarassets): rename internal/sidecar to internal/sidecarassets * chore(make): point test-browser at test/browser * docs(decisions): record internal/permissions deletion * refactor(doctor): use sidecarassets package * refactor(testrun): use sidecarassets package * fix(test): resolve testdata relative to browser_test.go * refactor(verifier): remove dead __sanderlingIndex compat alias * refactor(bundler): use encoding/json for JS string literals * docs(action-space): use vendor-neutral native driver wording * refactor(hierarchy): scrub backend tool name from comments * refactor(driver): scrub backend tool name from comments * refactor(driver): add DoubleTap and DoubleTapSelector to DeviceDriver * refactor(sidecar): implement DoubleTap with the sub-100ms inter-tap gap * refactor(chrome): implement DoubleTap as two taps with the gap * refactor(mock): record DoubleTap and DoubleTapSelector actions * refactor(runner): delegate double-tap to driver, drop gesture timing * test(runner): assert double-tap delegates to driver DoubleTap * docs(cmd): add package docs to CLI and developer tools * docs(driver): add package docs to driver interface and chrome backend * docs(driver): add package docs to mock and sidecar backends * docs(platform): add package docs to android and ios device prep * docs: add package docs to bundler and inspect * docs(ltl): add package doc to temporal logic evaluator * docs: add package docs to runner and testrun pipeline * docs: add package docs to trace and verifier * docs(sidecarassets): add package doc for embedded JAR loader * fix(chrome): add disable-dev-shm-usage so Chrome starts in CI * test(chrome): gate real-Chrome driver tests behind the browser tag * chore(make): run chrome driver tests in the browser job * fix(web-runtime): guard global error listeners for non-browser hosts The module registered window error/unhandledrejection listeners at top level, which threw under Node (the spec-api test runner) where globalThis.addEventListener is absent. Register only when the API exists; the real browser run is unaffected. * ci(browser): re-enable unprivileged user namespaces for headless Chrome ubuntu-latest moved to 24.04, whose AppArmor restriction on unprivileged user namespaces stops headless Chrome from opening its DevTools socket even with --no-sandbox, surfacing as the driver's 'websocket url timeout'. Relax the sysctl for the job and add a direct launch check so a future breakage shows Chrome's own stderr rather than an opaque driver timeout. * ci(browser): pin stable Chrome for the driver tests setup-chrome's default latest pulled a dev Chromium (150) whose remote debugging socket never came up under chromedp, while plain --dump-dom worked. Pin the stable channel, which the driver is tested against. * feat(defaults): add scroll and rebalance action weights Use relative-integer weights (taps/typing co-primary 100, scrolls 50, swipes 25, doubleTaps 10); the picker normalizes by their total. Adds scrolls to defaultActions as a first-class reveal behavior. * feat(defaults): trim scroll action weight wiring * fix(build): point sidecar jar ignore and embed paths at sidecarassets * test(defaults): drop stale longPresses re-export assertion longPresses is opt-in vocabulary, no longer re-exported from defaults/actions.ts since e0d3b20; its builtin resolution is already covered by api.test.ts. Trim the defaults test to scrolls, which is an actual default export. * fix(chrome): raise DevTools websocket read timeout to 60s Chrome cold-start on a loaded CI runner can exceed chromedp's 20s default for reading the DevTools websocket URL, flaking the browser tests with "websocket url timeout reached". Give launch more headroom.
2026-10-02 11:07:10 +00:00 · 2026-06-02 09:52:53 +05:30
1 parent 88db9653e5
commit c5bb176be8
@@ -1,3 +1,4 @@
+// Package ltl evaluates linear temporal logic formulas incrementally over observed steps.
 package ltl

 import (
@@ -31,13 +32,27 @@ func (v Verdict) String() string {
 // violated) or carries them forward as residuals. Once a single obligation
 // violates, the overall verdict latches to Violated.
 type Evaluator struct {
-	root     Formula
-	pending  []Formula
-	violated bool
+	root      Formula
+	pending   []Formula
+	violated  bool
+	steps     int
+	violation *Violation
+}
+
+// Violation is the witness for a latched verdict: the failing sub-formula, a
+// human-readable reason, and the observation step it fired at. A thrown
+// predicate carries the goja error text as its reason and sets IsError; a plain
+// false carries "predicate false"; Finalize fills it for liveness obligations
+// that never discharged.
+type Violation struct {
+	Formula Formula
+	Reason  string
+	Step    int
+	IsError bool
 }

 func NewEvaluator(formula Formula) *Evaluator {
-	return &Evaluator{root: formula}
+	return &Evaluator{root: nnf(formula)}
 }

 // Observe evaluates the formula against the current state and returns the
@@ -52,6 +67,7 @@ func (e *Evaluator) ObserveAt(now time.Time) Verdict {
 	if e.violated {
 		return VerdictViolated
 	}
+	e.steps++

 	fresh := rootObligation(e.root)
 	obligations := append(e.pending, fresh)
@@ -65,18 +81,136 @@ func (e *Evaluator) ObserveAt(now time.Time) Verdict {
 		case statusViolated:
 			e.violated = true
 			e.pending = nil
+			e.violation = result.witness
+			if e.violation != nil {
+				e.violation.Step = e.steps
+			}
 			return VerdictViolated
 		case statusPending:
 			e.pending = append(e.pending, result.formula)
 		}
 	}

+	e.pending = collapse(e.pending)
+
 	if len(e.pending) > 0 {
 		return VerdictPending
 	}
 	return VerdictHolds
 }

+// collapse removes structurally-identical obligations, keeping the first
+// occurrence in order. Distinct predicates never merge because ThunkFormula's
+// name participates in its describe() key, so deduping cannot hide a violation.
+func collapse(obligations []Formula) []Formula {
+	if len(obligations) < 2 {
+		return obligations
+	}
+	seen := make(map[string]struct{}, len(obligations))
+	result := obligations[:0]
+	for _, obligation := range obligations {
+		key := obligation.describe()
+		if _, ok := seen[key]; ok {
+			continue
+		}
+		seen[key] = struct{}{}
+		result = append(result, obligation)
+	}
+	return result
+}
+
+// Finalize reports the terminal verdict for the run. Pending obligations that
+// can never be discharged by a future step (an unbounded eventually that never
+// fired, a strong next with no successor) resolve to Violated; safety
+// obligations that were never breached resolve to Holds.
+func (e *Evaluator) Finalize() Verdict {
+	if e.violated {
+		return VerdictViolated
+	}
+	for _, obligation := range e.pending {
+		if finalize(obligation) == statusViolated {
+			e.violated = true
+			e.pending = nil
+			e.violation = &Violation{
+				Formula: obligation,
+				Reason:  finalizeReason(obligation),
+				Step:    e.steps,
+			}
+			return VerdictViolated
+		}
+	}
+	return VerdictHolds
+}
+
+// Violation returns the witness for a latched violation, or nil if the
+// evaluator has not violated. The witness is set by ObserveAt at the step a
+// reduction first violated, or by Finalize for a liveness obligation that
+// never discharged.
+func (e *Evaluator) Violation() *Violation {
+	return e.violation
+}
+
+// finalizeReason describes why an undischarged obligation resolves to violated
+// at run end.
+func finalizeReason(formula Formula) string {
+	switch formula.(type) {
+	case EventuallyFormula:
+		return "eventually never satisfied"
+	case NextFormula:
+		return "next obligation unmet at run end"
+	case ThunkFormula:
+		return "obligation unmet at run end"
+	default:
+		return "liveness obligation unmet at run end"
+	}
+}
+
+// finalize collapses a pending obligation to its terminal status assuming no
+// further steps will occur.
+func finalize(formula Formula) residualStatus {
+	switch concrete := formula.(type) {
+	case PureFormula:
+		if concrete.Value {
+			return statusHolds
+		}
+		return statusViolated
+	case ThunkFormula:
+		return statusViolated
+	case EventuallyFormula:
+		return statusViolated
+	case NextFormula:
+		return statusViolated
+	case AlwaysFormula:
+		return statusHolds
+	case NowFormula:
+		return finalize(concrete.Inner)
+	case NotFormula:
+		switch finalize(concrete.Inner) {
+		case statusViolated:
+			return statusHolds
+		default:
+			return statusViolated
+		}
+	case AndFormula:
+		if finalize(concrete.Left) == statusViolated || finalize(concrete.Right) == statusViolated {
+			return statusViolated
+		}
+		return statusHolds
+	case OrFormula:
+		if finalize(concrete.Left) == statusHolds || finalize(concrete.Right) == statusHolds {
+			return statusHolds
+		}
+		return statusViolated
+	case ImpliesFormula:
+		if finalize(concrete.Antecedent) == statusViolated {
+			return statusHolds
+		}
+		return finalize(concrete.Consequent)
+	default:
+		return statusHolds
+	}
+}
+
 // Residual returns a single Formula describing what the evaluator still has
 // to prove after the most recent ObserveAt. PureFormula{true} means the
 // property holds for the run so far; PureFormula{false} means it has latched
@@ -119,10 +253,46 @@ const (
 type reduceResult struct {
 	status  residualStatus
 	formula Formula
+	witness *Violation
 }

-func holds() reduceResult    { return reduceResult{status: statusHolds} }
+func holds() reduceResult { return reduceResult{status: statusHolds} }
+
+// violated reports a violation without an attached witness. Used where the
+// failing sub-formula is recovered from a child result whose own witness is
+// carried up by violatedFrom.
 func violated() reduceResult { return reduceResult{status: statusViolated} }
+
+// violatedWith reports a violation that originates at the given sub-formula
+// with the given reason. The reason distinguishes a thrown predicate from a
+// plain false so callers (and the inspect UI) can render the cause.
+func violatedWith(formula Formula, reason string) reduceResult {
+	return reduceResult{
+		status:  statusViolated,
+		witness: &Violation{Formula: formula, Reason: reason},
+	}
+}
+
+// violatedByError reports a violation caused by a predicate that threw. The
+// witness keeps the error text as its reason and flags IsError so callers can
+// render it as a thrown-predicate error rather than a plain false.
+func violatedByError(formula Formula, reason string) reduceResult {
+	return reduceResult{
+		status:  statusViolated,
+		witness: &Violation{Formula: formula, Reason: reason, IsError: true},
+	}
+}
+
+// violatedFrom propagates a child violation, preferring the child's witness so
+// the deepest failing leaf survives. When the child carried no witness the
+// fallback formula and reason describe this level instead.
+func violatedFrom(child reduceResult, fallback Formula, reason string) reduceResult {
+	if child.witness != nil {
+		return reduceResult{status: statusViolated, witness: child.witness}
+	}
+	return violatedWith(fallback, reason)
+}
+
 func pending(f Formula) reduceResult {
 	return reduceResult{status: statusPending, formula: f}
 }
@@ -133,13 +303,17 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		if concrete.Value {
 			return holds()
 		}
-		return violated()
+		return violatedWith(concrete, "pure false")

 	case ThunkFormula:
-		if concrete.Func() {
+		result, err := concrete.Func()
+		if err != nil {
+			return violatedByError(concrete, err.Error())
+		}
+		if result {
 			return holds()
 		}
-		return violated()
+		return violatedWith(concrete, "predicate false")

 	case NowFormula:
 		return reduce(concrete.Inner, now)
@@ -162,10 +336,10 @@ func reduce(formula Formula, now time.Time) reduceResult {
 			return holds()
 		}
 		if concrete.HasStepBound && concrete.StepBound <= 1 {
-			return violated()
+			return violatedFrom(innerResult, concrete, "eventually bound exhausted")
 		}
 		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
-			return violated()
+			return violatedFrom(innerResult, concrete, "eventually deadline reached")
 		}
 		next := concrete
 		if concrete.HasStepBound {
@@ -174,18 +348,14 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		return pending(next)

 	case ImpliesFormula:
-		antecedent := reduce(concrete.Antecedent, now)
-		switch antecedent.status {
-		case statusHolds:
-			return reduce(concrete.Consequent, now)
-		case statusViolated:
-			return holds()
-		case statusPending:
-			return pending(ImpliesFormula{
-				Antecedent: antecedent.formula,
-				Consequent: concrete.Consequent,
-			})
-		}
+		// NewEvaluator runs nnf, which rewrites a -> b to (not a) or b, so this
+		// case is unreachable from a normal evaluator. A directly-constructed
+		// formula reduced here is evaluated through the same equivalence so a
+		// pending antecedent cannot drop the consequent.
+		return reduce(OrFormula{
+			Left:  pushNot(concrete.Antecedent),
+			Right: nnf(concrete.Consequent),
+		}, now)

 	case OrFormula:
 		left := reduce(concrete.Left, now)
@@ -194,7 +364,7 @@ func reduce(formula Formula, now time.Time) reduceResult {
 			return holds()
 		}
 		if left.status == statusViolated && right.status == statusViolated {
-			return violated()
+			return violatedFrom(left, concrete, "both disjuncts violated")
 		}
 		if left.status == statusViolated {
 			return pending(right.formula)
@@ -207,8 +377,11 @@ func reduce(formula Formula, now time.Time) reduceResult {
 	case AndFormula:
 		left := reduce(concrete.Left, now)
 		right := reduce(concrete.Right, now)
-		if left.status == statusViolated || right.status == statusViolated {
-			return violated()
+		if left.status == statusViolated {
+			return violatedFrom(left, concrete, "conjunct violated")
+		}
+		if right.status == statusViolated {
+			return violatedFrom(right, concrete, "conjunct violated")
 		}
 		if left.status == statusHolds && right.status == statusHolds {
 			return holds()
@@ -225,7 +398,7 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		inner := reduce(concrete.Inner, now)
 		switch inner.status {
 		case statusHolds:
-			return violated()
+			return violatedWith(concrete, "negated formula held")
 		case statusViolated:
 			return holds()
 		case statusPending:
@@ -233,11 +406,38 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		}

 	case AlwaysFormula:
+		// First-reduction deadline resolution mirrors EventuallyFormula so a
+		// relative duration becomes a stable absolute deadline.
+		if !concrete.HasDeadline && concrete.Duration > 0 {
+			concrete.Deadline = now.Add(concrete.Duration)
+			concrete.HasDeadline = true
+		}
 		innerResult := reduce(concrete.Inner, now)
 		if innerResult.status == statusViolated {
-			return violated()
+			return violatedFrom(innerResult, concrete, "always inner violated")
+		}
+		// A bounded Always is the dual of a bounded Eventually: once the window
+		// closes without a breach it is vacuously satisfied. A pending inner at
+		// the closing step is a deferred obligation (a strong next, or an inner
+		// liveness that has not discharged); it must be carried so a later step
+		// or Finalize resolves it, never dropped to holds.
+		if concrete.HasStepBound && concrete.StepBound <= 1 {
+			if innerResult.status == statusHolds {
+				return holds()
+			}
+			return pending(innerResult.formula)
+		}
+		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
+			if innerResult.status == statusHolds {
+				return holds()
+			}
+			return pending(innerResult.formula)
+		}
+		next := concrete
+		next.Inner = concrete.Inner
+		if concrete.HasStepBound {
+			next.StepBound = concrete.StepBound - 1
 		}
-		next := AlwaysFormula{Inner: concrete.Inner}
 		if innerResult.status == statusHolds {
 			return pending(next)
 		}
@@ -36,10 +36,10 @@ func TestPure_FalseImmediatelyViolates(t *testing.T) {
 func TestThunk_TransitionFromHoldToViolate(t *testing.T) {
 	values := []bool{true, true, false, true, true}
 	step := 0
-	evaluator := NewEvaluator(Always(Thunk(func() bool {
+	evaluator := NewEvaluator(Always(Thunk(func() (bool, error) {
 		current := values[step]
 		step++
-		return current
+		return current, nil
 	})))

 	wantSequence := []Verdict{
@@ -59,7 +59,7 @@ func TestThunk_TransitionFromHoldToViolate(t *testing.T) {

 func TestEvaluator_StickinessAfterViolation(t *testing.T) {
 	state := true
-	evaluator := NewEvaluator(Always(Thunk(func() bool { return state })))
+	evaluator := NewEvaluator(Always(Thunk(func() (bool, error) { return state, nil })))

 	if got := evaluator.Observe(); got != VerdictHolds {
 		t.Fatalf("step 1: got %v, want holds", got)
@@ -83,7 +83,7 @@ func TestEvaluator_TopLevelPureCountedAtEachStep(t *testing.T) {

 func TestEvaluator_TopLevelThunkRespectsObservation(t *testing.T) {
 	state := true
-	evaluator := NewEvaluator(Thunk(func() bool { return state }))
+	evaluator := NewEvaluator(Thunk(func() (bool, error) { return state, nil }))
 	if got := evaluator.Observe(); got != VerdictHolds {
 		t.Errorf("expected holds, got %v", got)
 	}
@@ -93,21 +93,12 @@ func TestEvaluator_TopLevelThunkRespectsObservation(t *testing.T) {
 	}
 }

-func TestVerdict_String(t *testing.T) {
-	if VerdictHolds.String() != "holds" {
-		t.Errorf("VerdictHolds.String() = %q", VerdictHolds.String())
-	}
-	if VerdictViolated.String() != "violated" {
-		t.Errorf("VerdictViolated.String() = %q", VerdictViolated.String())
-	}
-}
-
 func TestDescribe(t *testing.T) {
 	formula := Always(Pure(true))
 	if got := Describe(formula); !strings.Contains(got, "Always") || !strings.Contains(got, "Pure(true)") {
 		t.Errorf("Describe wrong: %q", got)
 	}
-	thunk := Always(Thunk(func() bool { return true }))
+	thunk := Always(Thunk(func() (bool, error) { return true, nil }))
 	if got := Describe(thunk); !strings.Contains(got, "Thunk") {
 		t.Errorf("Describe(thunk) wrong: %q", got)
 	}
@@ -0,0 +1,92 @@
+package ltl
+
+import (
+	"testing"
+	"time"
+)
+
+// thunkSeq returns a predicate that yields the given boolean per observation,
+// repeating the last value once the sequence is exhausted.
+func thunkSeq(values ...bool) func() (bool, error) {
+	step := 0
+	return func() (bool, error) {
+		value := values[len(values)-1]
+		if step < len(values) {
+			value = values[step]
+		}
+		step++
+		return value, nil
+	}
+}
+
+func runAndFinalize(formula Formula, steps int) (Verdict, *Evaluator) {
+	evaluator := NewEvaluator(formula)
+	var last Verdict
+	for index := range steps {
+		last = evaluator.ObserveAt(time.Unix(int64(index), 0))
+		if last == VerdictViolated {
+			return last, evaluator
+		}
+	}
+	return evaluator.Finalize(), evaluator
+}
+
+// Implies with a temporal antecedent must still evaluate the consequent at the
+// current step. Always(p) holds over the observed run, so a false consequent
+// Not(q) at the last step makes the implication violated. The pre-fix engine
+// deferred the whole implication and reported Holds.
+func TestImplies_TemporalAntecedent_ConsequentFalseViolates(t *testing.T) {
+	p := Thunk(thunkSeq(true, true, true))
+	q := Thunk(thunkSeq(false, false, true))
+	formula := Implies(Always(p), Not(q))
+	if verdict, _ := runAndFinalize(formula, 3); verdict != VerdictViolated {
+		t.Fatalf("Implies(Always(p),Not(q)) p=TTT q=FFT: got %v, want violated", verdict)
+	}
+}
+
+// Single-step witness of the same class: antecedent holds, consequent false.
+func TestImplies_TemporalAntecedent_SingleStepViolates(t *testing.T) {
+	formula := Implies(Always(Thunk(thunkSeq(true))), Not(Thunk(thunkSeq(true))))
+	if verdict, _ := runAndFinalize(formula, 1); verdict != VerdictViolated {
+		t.Fatalf("Implies(Always(true),Not(true)): got %v, want violated", verdict)
+	}
+}
+
+// A consequent inside an Or must not mask the violation either.
+func TestImplies_TemporalAntecedent_OrConsequentViolates(t *testing.T) {
+	formula := Implies(Always(Thunk(thunkSeq(true))), Or(Not(Thunk(thunkSeq(true))), Pure(false)))
+	if verdict, _ := runAndFinalize(formula, 1); verdict != VerdictViolated {
+		t.Fatalf("Implies(Always(true),Or(Not(true),false)): got %v, want violated", verdict)
+	}
+}
+
+// Control: a false antecedent makes the implication vacuously hold.
+func TestImplies_TemporalAntecedent_FalseAntecedentHolds(t *testing.T) {
+	p := Thunk(thunkSeq(true, true, false))
+	q := Thunk(thunkSeq(false, false, true))
+	formula := Implies(Always(p), Not(q))
+	if verdict, _ := runAndFinalize(formula, 3); verdict != VerdictHolds {
+		t.Fatalf("Implies(Always(p),Not(q)) p=TTF q=FFT: got %v, want holds", verdict)
+	}
+}
+
+// A bounded Always whose inner is a still-pending deferred Next obligation must
+// carry that obligation past the window, not drop it to holds. The pre-fix
+// window-close branch returned holds() unconditionally and lost the violation.
+func TestBoundedAlways_PendingInnerCarried(t *testing.T) {
+	inner := AlwaysFormula{Inner: Next(Thunk(thunkSeq(false))), StepBound: 1, HasStepBound: true}
+	formula := Always(inner)
+	if verdict, _ := runAndFinalize(formula, 3); verdict != VerdictViolated {
+		t.Fatalf("Always(boundedAlways(Next(false),1)): got %v, want violated", verdict)
+	}
+}
+
+// A bounded Always whose inner genuinely holds each step stays satisfied: the
+// fix must not turn a satisfied bounded window into a false positive.
+func TestBoundedAlways_HoldingInnerStillHolds(t *testing.T) {
+	inner := AlwaysFormula{Inner: Not(Thunk(thunkSeq(false))), StepBound: 1, HasStepBound: true}
+	formula := Always(inner)
+	if verdict, _ := runAndFinalize(formula, 3); verdict != VerdictHolds {
+		t.Fatalf("Always(boundedAlways(Not(false),1)): got %v, want holds", verdict)
+	}
+}
@@ -0,0 +1,161 @@
+package ltl
+
+import (
+	"testing"
+	"testing/quick"
+	"time"
+)
+
+func TestFinalize_UnboundedEventuallyUnmetIsViolated(t *testing.T) {
+	evaluator := NewEvaluator(Eventually(ThunkNamed("p", func() (bool, error) { return false, nil })))
+	for index := range 3 {
+		if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending {
+			t.Fatalf("step %d: got %v, want pending", index, got)
+		}
+	}
+	if got := evaluator.Finalize(); got != VerdictViolated {
+		t.Errorf("Finalize = %v, want violated", got)
+	}
+}
+
+func TestFinalize_FinalStepNextIsViolated(t *testing.T) {
+	evaluator := NewEvaluator(Next(ThunkNamed("p", func() (bool, error) { return true, nil })))
+	if got := evaluator.Observe(); got != VerdictPending {
+		t.Fatalf("step 1: got %v, want pending", got)
+	}
+	if got := evaluator.Finalize(); got != VerdictViolated {
+		t.Errorf("Finalize = %v, want violated", got)
+	}
+}
+
+func TestFinalize_HoldingRunStaysHolds(t *testing.T) {
+	evaluator := NewEvaluator(Always(Pure(true)))
+	evaluator.Observe()
+	if got := evaluator.Finalize(); got != VerdictHolds {
+		t.Errorf("Finalize = %v, want holds", got)
+	}
+}
+
+func TestFinalize_AlreadyViolatedStaysViolated(t *testing.T) {
+	evaluator := NewEvaluator(Always(Pure(false)))
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Fatalf("expected violated, got %v", got)
+	}
+	if got := evaluator.Finalize(); got != VerdictViolated {
+		t.Errorf("Finalize = %v, want violated", got)
+	}
+}
+
+func TestFinalize_BoundedAlwaysVacuouslyHolds(t *testing.T) {
+	// A bounded Always whose window never closed (still pending) is safe.
+	evaluator := NewEvaluator(EventuallyWithinSteps(Pure(false), 5))
+	evaluator.Observe()
+	// The negated form of this is a bounded Always; build it directly.
+	bounded := NewEvaluator(Always(Not(EventuallyWithinSteps(ThunkNamed("p", func() (bool, error) { return false, nil }), 5))))
+	bounded.Observe()
+	if got := bounded.Finalize(); got == VerdictViolated {
+		t.Errorf("bounded always should not finalize to violated, got %v", got)
+	}
+}
+
+// TestEventuallyWithin_ViolatesIffNConsecutiveFalse locks the bounded
+// eventually contract: with a step bound of n and an inner that is false for
+// the first n observations, the verdict violates exactly at step n, and with at
+// least one true observation inside the window it holds.
+func TestEventuallyWithin_ViolatesIffNConsecutiveFalse(t *testing.T) {
+	law := func(boundSeed uint8, trueAtSeed uint8) bool {
+		bound := int(boundSeed%5) + 1
+		// trueAt < 0 means inner is never true.
+		trueAt := int(trueAtSeed)%(bound+2) - 1
+		step := 0
+		inner := ThunkNamed("p", func() (bool, error) {
+			current := trueAt >= 0 && step == trueAt
+			return current, nil
+		})
+		evaluator := NewEvaluator(EventuallyWithinSteps(inner, bound))
+
+		satisfiedInWindow := trueAt >= 0 && trueAt < bound
+		var final Verdict = VerdictPending
+		for index := range bound {
+			step = index
+			final = evaluator.ObserveAt(time.Unix(int64(index), 0))
+			if final == VerdictHolds || final == VerdictViolated {
+				break
+			}
+		}
+
+		if satisfiedInWindow {
+			return final == VerdictHolds
+		}
+		return final == VerdictViolated
+	}
+	if err := quick.Check(law, nil); err != nil {
+		t.Error(err)
+	}
+}
+
+// TestViolationLatchIsMonotonic locks: once an evaluator reports Violated, every
+// subsequent observation (and Finalize) stays Violated regardless of inputs.
+func TestViolationLatchIsMonotonic(t *testing.T) {
+	law := func(seed uint64) bool {
+		values := make([]bool, 8)
+		for index := range values {
+			values[index] = (seed>>uint(index))&1 == 1
+		}
+		step := 0
+		evaluator := NewEvaluator(Always(ThunkNamed("p", func() (bool, error) {
+			current := values[step%len(values)]
+			step++
+			return current, nil
+		})))
+		seenViolated := false
+		for index := range 16 {
+			got := evaluator.ObserveAt(time.Unix(int64(index), 0))
+			if got == VerdictViolated {
+				seenViolated = true
+			} else if seenViolated {
+				return false
+			}
+		}
+		if seenViolated && evaluator.Finalize() != VerdictViolated {
+			return false
+		}
+		return true
+	}
+	if err := quick.Check(law, nil); err != nil {
+		t.Error(err)
+	}
+}
+
+func TestCollapse_IdenticalObligationsMerge(t *testing.T) {
+	merged := collapse([]Formula{
+		Next(Pure(true)),
+		Next(Pure(true)),
+		Next(Pure(true)),
+	})
+	if len(merged) != 1 {
+		t.Errorf("expected 1 obligation after collapse, got %d", len(merged))
+	}
+}
+
+func TestCollapse_DistinctPredicatesDoNotMerge(t *testing.T) {
+	merged := collapse([]Formula{
+		Eventually(ThunkNamed("p3", func() (bool, error) { return false, nil })),
+		Eventually(ThunkNamed("p4", func() (bool, error) { return false, nil })),
+	})
+	if len(merged) != 2 {
+		t.Errorf("distinct predicates must not merge, got %d", len(merged))
+	}
+}
+
+func TestCollapse_NamedThunkLeakBoundsPendingSet(t *testing.T) {
+	// Always(Eventually(sameThunk)): each step spawns an identical obligation.
+	// Without collapse the pending set grows unboundedly.
+	evaluator := NewEvaluator(Always(Eventually(ThunkNamed("p", func() (bool, error) { return false, nil }))))
+	for index := range 20 {
+		evaluator.ObserveAt(time.Unix(int64(index), 0))
+	}
+	if len(evaluator.pending) > 2 {
+		t.Errorf("pending set leaked to %d obligations", len(evaluator.pending))
+	}
+}
@@ -13,9 +13,9 @@ type Formula interface {
 	describe() string
 }

-// PredicateLabel lets a ThunkFormula carry a human-readable name for the
-// closure it wraps. Verifier wires this in when the spec gives the predicate
-// a property name; otherwise it stays empty and serializes without a name.
+// PredicateLabel lets a ThunkFormula expose the identity of the closure it
+// wraps. ThunkFormula satisfies it through its Name field; an empty name
+// serializes without a name.
 type PredicateLabel interface {
 	PredicateName() string
 }
@@ -33,18 +33,35 @@ func (e ErrorFormula) describe() string {
 	return fmt.Sprintf("Error(%q)", e.Message)
 }

+// AlwaysFormula obliges its inner formula to hold at every step. A bounded
+// Always (the dual of a bounded Eventually) holds for the steps inside its
+// window and is vacuously satisfied once the window closes. An unbounded
+// Always carries no bound fields and is checked at every observed step.
 type AlwaysFormula struct {
-	Inner Formula
+	Inner        Formula
+	StepBound    int
+	HasStepBound bool
+	Duration     time.Duration
+	Deadline     time.Time
+	HasDeadline  bool
 }

 type PureFormula struct {
 	Value bool
 }

+// ThunkFormula wraps an opaque predicate closure. Func returns the predicate's
+// boolean result and a non-nil error when the predicate threw; a thrown
+// predicate is a witnessed violation distinct from a plain false. Name carries
+// the predicate's identity so two distinct predicates produce distinct
+// describe() keys and are never merged during obligation collapse.
 type ThunkFormula struct {
-	Func func() bool
+	Func func() (bool, error)
+	Name string
 }

+func (t ThunkFormula) PredicateName() string { return t.Name }
+
 // NowFormula marks its inner formula for evaluation at the current step only.
 // Primarily used so that now(...).implies(...) parses unambiguously.
 type NowFormula struct {
@@ -96,7 +113,11 @@ func Always(inner Formula) Formula { return AlwaysFormula{Inner: inner} }

 func Pure(value bool) Formula { return PureFormula{Value: value} }

-func Thunk(function func() bool) Formula { return ThunkFormula{Func: function} }
+func Thunk(function func() (bool, error)) Formula { return ThunkFormula{Func: function} }
+
+func ThunkNamed(name string, function func() (bool, error)) Formula {
+	return ThunkFormula{Func: function, Name: name}
+}

 func Now(inner Formula) Formula { return NowFormula{Inner: inner} }

@@ -137,11 +158,27 @@ func (OrFormula) isFormula()         {}
 func (AndFormula) isFormula()        {}
 func (NotFormula) isFormula()        {}

-func (a AlwaysFormula) describe() string { return "Always(" + a.Inner.describe() + ")" }
-func (p PureFormula) describe() string   { return fmt.Sprintf("Pure(%t)", p.Value) }
-func (ThunkFormula) describe() string    { return "Thunk(...)" }
-func (n NowFormula) describe() string    { return "Now(" + n.Inner.describe() + ")" }
-func (n NextFormula) describe() string   { return "Next(" + n.Inner.describe() + ")" }
+func (a AlwaysFormula) describe() string {
+	parts := []string{a.Inner.describe()}
+	if a.HasStepBound {
+		parts = append(parts, fmt.Sprintf("steps=%d", a.StepBound))
+	}
+	if a.HasDeadline {
+		parts = append(parts, "deadline="+a.Deadline.Format(time.RFC3339Nano))
+	} else if a.Duration > 0 {
+		parts = append(parts, "within="+a.Duration.String())
+	}
+	return "Always(" + strings.Join(parts, ", ") + ")"
+}
+func (p PureFormula) describe() string { return fmt.Sprintf("Pure(%t)", p.Value) }
+func (t ThunkFormula) describe() string {
+	if t.Name != "" {
+		return "Thunk(" + t.Name + ")"
+	}
+	return "Thunk(...)"
+}
+func (n NowFormula) describe() string  { return "Now(" + n.Inner.describe() + ")" }
+func (n NextFormula) describe() string { return "Next(" + n.Inner.describe() + ")" }
 func (e EventuallyFormula) describe() string {
 	parts := []string{e.Inner.describe()}
 	if e.HasStepBound {
@@ -176,10 +213,20 @@ type withinNode struct {
 }

 func (a AlwaysFormula) MarshalJSON() ([]byte, error) {
-	return json.Marshal(struct {
-		Op  string  `json:"op"`
-		Arg Formula `json:"arg"`
-	}{"always", a.Inner})
+	payload := struct {
+		Op     string      `json:"op"`
+		Arg    Formula     `json:"arg"`
+		Within *withinNode `json:"within,omitempty"`
+	}{Op: "always", Arg: a.Inner}
+	switch {
+	case a.HasStepBound:
+		payload.Within = &withinNode{Amount: int64(a.StepBound), Unit: "steps"}
+	case a.Duration > 0:
+		payload.Within = &withinNode{Amount: a.Duration.Milliseconds(), Unit: "milliseconds"}
+	case a.HasDeadline:
+		payload.Within = &withinNode{Amount: a.Deadline.UnixMilli(), Unit: "deadline"}
+	}
+	return json.Marshal(payload)
 }

 func (n NowFormula) MarshalJSON() ([]byte, error) {
@@ -50,7 +50,7 @@ func TestAlways_Now_ViolatesImmediately(t *testing.T) {

 func TestAlways_Next_PendingThenViolated(t *testing.T) {
 	y := true
-	evaluator := NewEvaluator(Always(Next(Thunk(func() bool { return y }))))
+	evaluator := NewEvaluator(Always(Next(Thunk(func() (bool, error) { return y, nil }))))

 	if got := evaluator.Observe(); got != VerdictPending {
 		t.Errorf("step 1: got %v, want pending", got)
@@ -62,7 +62,7 @@ func TestAlways_Next_PendingThenViolated(t *testing.T) {
 }

 func TestAlways_Next_StaysPendingWhileInnerHolds(t *testing.T) {
-	evaluator := NewEvaluator(Always(Next(Thunk(func() bool { return true }))))
+	evaluator := NewEvaluator(Always(Next(Thunk(func() (bool, error) { return true, nil }))))
 	for index := range 3 {
 		if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending {
 			t.Errorf("step %d: got %v, want pending", index+1, got)
@@ -76,8 +76,8 @@ func TestAlways_NowImpliesEventuallyWithin_ViolatesWhenYLate(t *testing.T) {
 	xValues := []bool{true, false, false, false, false}
 	yValues := []bool{false, false, false, true, true}
 	step := 0
-	predX := Thunk(func() bool { return xValues[step] })
-	predY := Thunk(func() bool { return yValues[step] })
+	predX := Thunk(func() (bool, error) { return xValues[step], nil })
+	predY := Thunk(func() (bool, error) { return yValues[step], nil })

 	formula := Always(Implies(Now(predX), EventuallyWithinSteps(predY, 3)))
 	evaluator := NewEvaluator(formula)
@@ -107,8 +107,8 @@ func TestAlways_NowImpliesEventuallyWithin_HoldsWhenYInBound(t *testing.T) {
 	xValues := []bool{true, false, false}
 	yValues := []bool{false, false, true}
 	step := 0
-	predX := Thunk(func() bool { return xValues[step] })
-	predY := Thunk(func() bool { return yValues[step] })
+	predX := Thunk(func() (bool, error) { return xValues[step], nil })
+	predY := Thunk(func() (bool, error) { return yValues[step], nil })

 	formula := Always(Implies(Now(predX), EventuallyWithinSteps(predY, 3)))
 	evaluator := NewEvaluator(formula)
@@ -187,12 +187,6 @@ func TestNot_InvertsPure(t *testing.T) {
 	}
 }

-func TestVerdict_StringPending(t *testing.T) {
-	if got := VerdictPending.String(); got != "pending" {
-		t.Errorf("VerdictPending.String() = %q", got)
-	}
-}
-
 func TestMarshalJSON_AlwaysImpliesEventually(t *testing.T) {
 	formula := Always(Implies(Now(Pure(true)), EventuallyWithinSteps(Pure(false), 3)))
 	body, err := json.Marshal(formula)
@@ -231,7 +225,7 @@ func TestMarshalJSON_NextAndThunkAndError(t *testing.T) {
 	if string(body) != `{"op":"next","arg":{"op":"true"}}` {
 		t.Errorf("next marshal wrong: %s", body)
 	}
-	body, _ = json.Marshal(Thunk(func() bool { return true }))
+	body, _ = json.Marshal(Thunk(func() (bool, error) { return true, nil }))
 	if string(body) != `{"op":"predicate"}` {
 		t.Errorf("thunk marshal wrong: %s", body)
 	}
@@ -0,0 +1,87 @@
+package ltl
+
+// nnf rewrites a formula into negation normal form: every NotFormula is pushed
+// down until it wraps only an opaque leaf (a ThunkFormula or ErrorFormula).
+// Temporal operators are dualized along the way (Always <-> Eventually) so the
+// evaluator never has to reduce a negated temporal obligation, which it cannot
+// do soundly across steps.
+func nnf(formula Formula) Formula {
+	switch concrete := formula.(type) {
+	case NotFormula:
+		return pushNot(concrete.Inner)
+	case AlwaysFormula:
+		next := concrete
+		next.Inner = nnf(concrete.Inner)
+		return next
+	case EventuallyFormula:
+		next := concrete
+		next.Inner = nnf(concrete.Inner)
+		return next
+	case NextFormula:
+		return NextFormula{Inner: nnf(concrete.Inner)}
+	case NowFormula:
+		return NowFormula{Inner: nnf(concrete.Inner)}
+	case AndFormula:
+		return AndFormula{Left: nnf(concrete.Left), Right: nnf(concrete.Right)}
+	case OrFormula:
+		return OrFormula{Left: nnf(concrete.Left), Right: nnf(concrete.Right)}
+	case ImpliesFormula:
+		// a -> b is rewritten to (not a) or b so the consequent is always
+		// reduced live each step. Keeping it as ImpliesFormula let a pending
+		// (temporal) antecedent defer the whole implication and silently drop a
+		// consequent that was false at the current step.
+		return OrFormula{
+			Left:  pushNot(concrete.Antecedent),
+			Right: nnf(concrete.Consequent),
+		}
+	default:
+		return formula
+	}
+}
+
+// pushNot returns the negation normal form of NOT f.
+func pushNot(formula Formula) Formula {
+	switch concrete := formula.(type) {
+	case PureFormula:
+		return PureFormula{Value: !concrete.Value}
+	case ThunkFormula:
+		return NotFormula{Inner: concrete}
+	case ErrorFormula:
+		return NotFormula{Inner: concrete}
+	case NotFormula:
+		return nnf(concrete.Inner)
+	case AndFormula:
+		return OrFormula{Left: pushNot(concrete.Left), Right: pushNot(concrete.Right)}
+	case OrFormula:
+		return AndFormula{Left: pushNot(concrete.Left), Right: pushNot(concrete.Right)}
+	case ImpliesFormula:
+		return AndFormula{
+			Left:  nnf(concrete.Antecedent),
+			Right: pushNot(concrete.Consequent),
+		}
+	case NowFormula:
+		return NowFormula{Inner: pushNot(concrete.Inner)}
+	case NextFormula:
+		return NextFormula{Inner: pushNot(concrete.Inner)}
+	case AlwaysFormula:
+		return EventuallyFormula{
+			Inner:        pushNot(concrete.Inner),
+			StepBound:    concrete.StepBound,
+			HasStepBound: concrete.HasStepBound,
+			Duration:     concrete.Duration,
+			Deadline:     concrete.Deadline,
+			HasDeadline:  concrete.HasDeadline,
+		}
+	case EventuallyFormula:
+		return AlwaysFormula{
+			Inner:        pushNot(concrete.Inner),
+			StepBound:    concrete.StepBound,
+			HasStepBound: concrete.HasStepBound,
+			Duration:     concrete.Duration,
+			Deadline:     concrete.Deadline,
+			HasDeadline:  concrete.HasDeadline,
+		}
+	default:
+		return NotFormula{Inner: formula}
+	}
+}
@@ -0,0 +1,97 @@
+package ltl
+
+import (
+	"testing"
+	"testing/quick"
+	"time"
+)
+
+// leaf builds a small set of representative atomic formulas indexed by a seed.
+func leafFor(seed uint8) Formula {
+	switch seed % 3 {
+	case 0:
+		return Pure(true)
+	case 1:
+		return Pure(false)
+	default:
+		return ThunkNamed("p", func() (bool, error) { return true, nil })
+	}
+}
+
+func TestNNF_DoubleNegationIsIdentity(t *testing.T) {
+	law := func(seed uint8) bool {
+		leaf := leafFor(seed)
+		doubled := nnf(Not(Not(leaf)))
+		direct := nnf(leaf)
+		return doubled.describe() == direct.describe()
+	}
+	if err := quick.Check(law, nil); err != nil {
+		t.Error(err)
+	}
+}
+
+func TestNNF_NotAlwaysIsEventuallyNot(t *testing.T) {
+	law := func(seed uint8) bool {
+		leaf := leafFor(seed)
+		negated := nnf(Not(Always(leaf)))
+		expected := nnf(Eventually(Not(leaf)))
+		return negated.describe() == expected.describe()
+	}
+	if err := quick.Check(law, nil); err != nil {
+		t.Error(err)
+	}
+}
+
+func TestNNF_NotEventuallyIsAlwaysNot(t *testing.T) {
+	law := func(seed uint8) bool {
+		leaf := leafFor(seed)
+		negated := nnf(Not(Eventually(leaf)))
+		expected := nnf(Always(Not(leaf)))
+		return negated.describe() == expected.describe()
+	}
+	if err := quick.Check(law, nil); err != nil {
+		t.Error(err)
+	}
+}
+
+func TestNNF_BoundedEventuallyDualKeepsBound(t *testing.T) {
+	negated := nnf(Not(EventuallyWithinSteps(Pure(true), 4)))
+	always, ok := negated.(AlwaysFormula)
+	if !ok {
+		t.Fatalf("expected AlwaysFormula, got %T", negated)
+	}
+	if !always.HasStepBound || always.StepBound != 4 {
+		t.Errorf("bound not preserved: %+v", always)
+	}
+}
+
+func TestNNF_PushesNotToThunkLeaf(t *testing.T) {
+	formula := nnf(Always(Not(Always(ThunkNamed("p", func() (bool, error) { return true, nil })))))
+	always, ok := formula.(AlwaysFormula)
+	if !ok {
+		t.Fatalf("expected AlwaysFormula, got %T", formula)
+	}
+	eventually, ok := always.Inner.(EventuallyFormula)
+	if !ok {
+		t.Fatalf("expected inner EventuallyFormula, got %T", always.Inner)
+	}
+	not, ok := eventually.Inner.(NotFormula)
+	if !ok {
+		t.Fatalf("expected NotFormula leaf, got %T", eventually.Inner)
+	}
+	if _, ok := not.Inner.(ThunkFormula); !ok {
+		t.Errorf("expected Not to wrap a Thunk, got %T", not.Inner)
+	}
+}
+
+func TestNNF_NotAlwaysTrueViaEvaluatorReportsViolated(t *testing.T) {
+	evaluator := NewEvaluator(Always(Not(Always(ThunkNamed("p", func() (bool, error) { return true, nil })))))
+	for index := range 4 {
+		if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got == VerdictViolated {
+			t.Fatalf("step %d latched violated prematurely", index)
+		}
+	}
+	if got := evaluator.Finalize(); got != VerdictViolated {
+		t.Errorf("Finalize = %v, want violated", got)
+	}
+}
@@ -0,0 +1,80 @@
+package ltl
+
+import (
+	"errors"
+	"testing"
+	"time"
+)
+
+func TestViolation_PredicateFalseCarriesReasonAndStep(t *testing.T) {
+	values := []bool{true, false}
+	step := 0
+	evaluator := NewEvaluator(Always(ThunkNamed("p", func() (bool, error) {
+		current := values[step]
+		step++
+		return current, nil
+	})))
+	if got := evaluator.ObserveAt(time.Unix(0, 0)); got != VerdictHolds {
+		t.Fatalf("step 1: got %v, want holds", got)
+	}
+	if got := evaluator.ObserveAt(time.Unix(1, 0)); got != VerdictViolated {
+		t.Fatalf("step 2: got %v, want violated", got)
+	}
+	witness := evaluator.Violation()
+	if witness == nil {
+		t.Fatal("Violation = nil, want non-nil")
+	}
+	if witness.Reason != "predicate false" {
+		t.Errorf("Reason = %q, want %q", witness.Reason, "predicate false")
+	}
+	if witness.Step != 2 {
+		t.Errorf("Step = %d, want 2", witness.Step)
+	}
+	if witness.IsError {
+		t.Errorf("IsError = true, want false for a plain false")
+	}
+}
+
+func TestViolation_ThrownPredicateSetsIsError(t *testing.T) {
+	evaluator := NewEvaluator(Always(ThunkNamed("p", func() (bool, error) {
+		return false, errors.New("boom")
+	})))
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Fatalf("got %v, want violated", got)
+	}
+	witness := evaluator.Violation()
+	if witness == nil {
+		t.Fatal("Violation = nil, want non-nil")
+	}
+	if !witness.IsError {
+		t.Errorf("IsError = false, want true for a thrown predicate")
+	}
+	if witness.Reason != "boom" {
+		t.Errorf("Reason = %q, want %q", witness.Reason, "boom")
+	}
+}
+
+func TestViolation_FinalizeFillsWitness(t *testing.T) {
+	evaluator := NewEvaluator(Eventually(ThunkNamed("p", func() (bool, error) {
+		return false, nil
+	})))
+	evaluator.ObserveAt(time.Unix(0, 0))
+	if got := evaluator.Finalize(); got != VerdictViolated {
+		t.Fatalf("Finalize = %v, want violated", got)
+	}
+	witness := evaluator.Violation()
+	if witness == nil {
+		t.Fatal("Violation = nil after Finalize, want non-nil")
+	}
+	if witness.Reason != "eventually never satisfied" {
+		t.Errorf("Reason = %q, want %q", witness.Reason, "eventually never satisfied")
+	}
+}
+
+func TestViolation_NilBeforeViolation(t *testing.T) {
+	evaluator := NewEvaluator(Always(Pure(true)))
+	evaluator.Observe()
+	if got := evaluator.Violation(); got != nil {
+		t.Errorf("Violation = %+v, want nil for a holding run", got)
+	}
+}