diff --git a/internal/verifier/marshal.go b/internal/verifier/marshal.go
index d738e84..18b2ac6 100644
--- a/internal/verifier/marshal.go
+++ b/internal/verifier/marshal.go
@@ -353,9 +353,20 @@ func lastActionFields(action *Action) []actionField {
 	if action.Applied {
 		applied = true
 	}
+	// A relaunch between two readings is not "no action happened", which is
+	// what dropping the action reported instead: the app restarted after an
+	// action that did run. Only the positive report is a fact the runner can
+	// vouch for, so the other side is null rather than false: a target whose
+	// foreground the runner cannot read (web, iOS) never relaunches the app and
+	// still cannot promise it never restarted.
+	var relaunched any
+	if action.Relaunched {
+		relaunched = true
+	}
 	fields := []actionField{
 		{key: "kind", value: string(action.Kind)},
 		{key: "applied", value: applied},
+		{key: "relaunched", value: relaunched},
 	}
 	if action.On != "" {
 		fields = append(fields, actionField{key: "on", value: action.On})
diff --git a/internal/verifier/types.go b/internal/verifier/types.go
index 125703b..09d2c5c 100644
--- a/internal/verifier/types.go
+++ b/internal/verifier/types.go
@@ -38,6 +38,12 @@ type Action struct {
 	// when the apply call failed and nothing can say whether the action
 	// reached the app. The spec is told which of the two it is.
 	Applied bool
+	// Relaunched, like Applied, is meaningful only on state.lastAction: the
+	// runner brought the app back to the foreground after this action, so the
+	// two readings the spec compares straddle a restart. The action still
+	// happened; what a property cannot assume across it is that app state ran
+	// continuously from one reading to the next.
+	Relaunched bool
 }
 
 // LogEntry mirrors a logcat line captured between steps.
diff --git a/pkg/spec/src/types.ts b/pkg/spec/src/types.ts
index c28fd05..9d3cdf8 100644
--- a/pkg/spec/src/types.ts
+++ b/pkg/spec/src/types.ts
@@ -109,8 +109,17 @@ export interface ExceptionRecord {
  * tap landed. Null is unknown, not "it did not happen" (`state.lastAction` is
  * itself null for that), so a property attributing an effect to this action
  * has to decline unless `applied` is true.
+ *
+ * `relaunched` is true when the runner had to bring the app back to the
+ * foreground after this action, so the previous reading and the current one
+ * straddle a restart. The action itself still happened; what a property cannot
+ * assume across it is that app state ran continuously between the two readings,
+ * and one demanding an effect of this action has to decline. Null is "not
+ * reported", which is weaker than "the app never restarted": a target whose
+ * foreground the runner cannot read never relaunches the app and cannot promise
+ * that either.
  */
-export type LastAction = Action & { applied: true | null };
+export type LastAction = Action & { applied: true | null; relaunched: true | null };
 
 export interface State {
   snapshots: Snapshots;