diff --git a/internal/verifier/bindings.go b/internal/verifier/bindings.go
index f8facbe..6d67b0e 100644
--- a/internal/verifier/bindings.go
+++ b/internal/verifier/bindings.go
@@ -14,9 +14,10 @@ type extractorState struct {
 
 type formulaState struct {
 	predicate goja.Callable
-	// err latches the first goja error returned by predicate. The thunk
-	// returns false on error so the LTL evaluator marks the property
-	// violated; PredicateError surfaces the underlying cause.
+	// err holds the goja error from this thunk's most recent invocation, or
+	// nil if the latest call succeeded. The thunk returns false on error so
+	// the LTL evaluator marks the property violated; PredicateError surfaces
+	// the underlying cause for the current step.
 	err error
 }
 
diff --git a/internal/verifier/worker.go b/internal/verifier/worker.go
index 24fd683..d7ae7e4 100644
--- a/internal/verifier/worker.go
+++ b/internal/verifier/worker.go
@@ -254,6 +254,7 @@ func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict {
 	for name, evaluator := range v.evaluators {
 		verdicts[name] = evaluator.ObserveAt(stepTime)
 	}
+	v.refreshPredicateErrors()
 	return verdicts
 }
 
@@ -302,15 +303,32 @@ func (v *Verifier) formulaThunk(index int) func() bool {
 		formula := v.formulas[index]
 		result, err := formula.predicate(goja.Undefined())
 		if err != nil {
-			if formula.err == nil {
-				formula.err = err
-			}
+			formula.err = err
 			return false
 		}
+		formula.err = nil
 		return result.ToBoolean()
 	}
 }
 
+// refreshPredicateErrors re-invokes every registered predicate so that
+// formula.err reflects the current step rather than a latched first-step
+// throw. EvaluateProperties short-circuits once a property has latched to
+// violated, so without this refresh the runner's per-step "predicate error"
+// log freezes on whatever the predicate threw at step 1. The refreshed errors
+// have no effect on verdicts.
+func (v *Verifier) refreshPredicateErrors() {
+	for _, formula := range v.formulas {
+		result, err := formula.predicate(goja.Undefined())
+		if err != nil {
+			formula.err = err
+			continue
+		}
+		_ = result
+		formula.err = nil
+	}
+}
+
 // PredicateError returns the first goja error raised by any thunk in the
 // named property's formula tree, or nil if none fired. Callers typically
 // consult this after EvaluateProperties reports a violation to distinguish