diff --git a/internal/ltl/evaluator.go b/internal/ltl/evaluator.go
index 783df8c..aa6379d 100644
--- a/internal/ltl/evaluator.go
+++ b/internal/ltl/evaluator.go
@@ -34,10 +34,11 @@ type Evaluator struct {
 	root     Formula
 	pending  []Formula
 	violated bool
+	steps    int
 }
 
 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 +53,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)
@@ -71,12 +73,98 @@ func (e *Evaluator) ObserveAt(now time.Time) Verdict {
 		}
 	}
 
+	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
+			return VerdictViolated
+		}
+	}
+	return VerdictHolds
+}
+
+// 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
@@ -233,11 +321,30 @@ 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()
 		}
-		next := AlwaysFormula{Inner: concrete.Inner}
+		// A bounded Always is the dual of a bounded Eventually: once the window
+		// closes without a breach it is vacuously satisfied. At the last step in
+		// the window a pending inner cannot be deferred, so it resolves to holds.
+		if concrete.HasStepBound && concrete.StepBound <= 1 {
+			return holds()
+		}
+		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
+			return holds()
+		}
+		next := concrete
+		next.Inner = concrete.Inner
+		if concrete.HasStepBound {
+			next.StepBound = concrete.StepBound - 1
+		}
 		if innerResult.status == statusHolds {
 			return pending(next)
 		}