diff --git a/internal/ltl/evaluator.go b/internal/ltl/evaluator.go
index f0b6c2b..2d07194 100644
--- a/internal/ltl/evaluator.go
+++ b/internal/ltl/evaluator.go
@@ -336,6 +336,12 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		}
 		return violatedWith(concrete, "pure false")
 
+	case ErrorFormula:
+		// A thrown predicate substituted into a residual at the trace
+		// boundary. Reducing it re-reports the same failure rather than
+		// crashing the run.
+		return violatedByError(concrete, concrete.Message)
+
 	case ThunkFormula:
 		result, err := concrete.predicate()
 		if err != nil {
diff --git a/internal/ltl/finalize_test.go b/internal/ltl/finalize_test.go
index 54a6953..4ae5456 100644
--- a/internal/ltl/finalize_test.go
+++ b/internal/ltl/finalize_test.go
@@ -262,3 +262,23 @@ func TestCollapse_UnnamedPredicatesDoNotMerge(t *testing.T) {
 		t.Errorf("origin = %d, want 2", witness.Step)
 	}
 }
+
+// TestReduce_ErrorFormulaViolates: the verifier substitutes an ErrorFormula for
+// the residual of a property whose predicate threw, and that residual is fed
+// back into the evaluator on the next step. Reducing one used to panic.
+func TestReduce_ErrorFormulaViolates(t *testing.T) {
+	evaluator := NewEvaluator(Always(ErrorFormula{Message: "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.Reason != "boom" {
+		t.Errorf("Reason = %q, want %q", witness.Reason, "boom")
+	}
+	if !witness.IsError {
+		t.Error("IsError = false, want true")
+	}
+}