diff --git a/TypeSystem/flow-analysis/reachability_switch_A06_t01.dart b/TypeSystem/flow-analysis/reachability_switch_A06_t01.dart
new file mode 100644
index 0000000000..b5096d35d4
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_switch_A06_t01.dart
@@ -0,0 +1,72 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion switch statement: If `N` is a switch statement of the form
+/// `switch (E) {alternatives}` then:
+/// - Let `before(E) = before(N)`.
+/// - For each `C` in `alternatives` with statement body `S`:
+///   - If `C` is labelled let
+///     `before(S) = conservativeJoin(after(E), assignedIn(N), capturedIn(N))`
+///     otherwise let `before(S) = after(E)`.
+///  - If the cases are exhaustive, then let `after(N) = break(N)` otherwise let
+///    `after(N) = join(after(E), break(N))`.
+///
+/// @description Checks that if a type `T` is made a type of interest in `E`
+/// for a variable `s` then `s` can be promoted in `alternatives` and `after(N)`
+/// @author sgrekhov22@gmail.com
+/// @issue 60479
+/// @issue 60539
+
+class S {}
+
+class T extends S {
+  int answer() => 42;
+}
+
+void test1() {
+  S s = S();
+  switch (s is T ? 1 : 2) { // Make `T` a type of interest
+    case 1:
+      s = T();
+      s.answer();
+    case 2:
+  }
+}
+
+void test2() {
+  S s = S();
+  switch (s is T ? 1 : 2) { // Make `T` a type of interest
+    label: case 1:
+      s = T();
+      s.answer();
+    case 2:
+  }
+}
+
+void test3() {
+  S s = S();
+  switch (s is T) {
+    case true:
+    case false:
+  }
+  s = T();
+  s.answer();
+}
+
+void test4() {
+  S s = S();
+  switch (s is T) {
+    label: case true:
+    case false:
+  }
+  s = T();
+  s.answer();
+}
+
+main() {
+  test1();
+  test2();
+  test3();
+  test4();
+}
diff --git a/TypeSystem/flow-analysis/reachability_switch_A06_t02.dart b/TypeSystem/flow-analysis/reachability_switch_A06_t02.dart
new file mode 100644
index 0000000000..18b04319a7
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_switch_A06_t02.dart
@@ -0,0 +1,50 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion switch statement: If `N` is a switch statement of the form
+/// `switch (E) {alternatives}` then:
+/// - Let `before(E) = before(N)`.
+/// - For each `C` in `alternatives` with statement body `S`:
+///   - If `C` is labelled let
+///     `before(S) = conservativeJoin(after(E), assignedIn(N), capturedIn(N))`
+///     otherwise let `before(S) = after(E)`.
+///  - If the cases are exhaustive, then let `after(N) = break(N)` otherwise let
+///    `after(N) = join(after(E), break(N))`.
+///
+/// @description Checks that if a type `T` is made a type of interest in `E`
+/// for a variable `s` then `s` can be promoted in `after(N)`.
+/// @author sgrekhov22@gmail.com
+/// @issue 60479
+/// @issue 60539
+
+class S {}
+
+class T extends S {
+  int answer() => 42;
+}
+
+test1() {
+  S s = S();
+  switch (s is T) {
+    case true:
+    case false:
+  }
+  s = T();
+  s.answer();
+}
+
+test2() {
+  S s = S();
+  switch (s is T ? 1 : 2) {
+    label: case 1:
+    case 2:
+  }
+  s = T();
+  s.answer();
+}
+
+main() {
+  test1();
+  test2();
+}
diff --git a/TypeSystem/flow-analysis/reachability_switch_A06_t03.dart b/TypeSystem/flow-analysis/reachability_switch_A06_t03.dart
new file mode 100644
index 0000000000..eb22e92325
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_switch_A06_t03.dart
@@ -0,0 +1,86 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion switch statement: If `N` is a switch statement of the form
+/// `switch (E) {alternatives}` then:
+/// - Let `before(E) = before(N)`.
+/// - For each `C` in `alternatives` with statement body `S`:
+///   - If `C` is labelled let
+///     `before(S) = conservativeJoin(after(E), assignedIn(N), capturedIn(N))`
+///     otherwise let `before(S) = after(E)`.
+///  - If the cases are exhaustive, then let `after(N) = break(N)` otherwise let
+///    `after(N) = join(after(E), break(N))`.
+///
+/// @description Checks that if a type `T` is made a type of interest in `E`
+/// for a variable `s` then `s` cannot be promoted in other `alternatives`.
+/// @author sgrekhov22@gmail.com
+
+class S {}
+
+class T extends S {
+  int answer() => 42;
+}
+
+test1() {
+  S s = S();
+  switch (42) {
+    case 1:
+      s = T();
+      s.answer();
+//      ^^^^^^
+// [analyzer] unspecified
+// [cfe] unspecified
+    case 2:
+      if (s is T) {} // Make `T` a type of interest
+  }
+}
+
+test2() {
+  S s = S();
+  switch (42) {
+    label: case 1:
+      s = T();
+      s.answer();
+//      ^^^^^^
+// [analyzer] unspecified
+// [cfe] unspecified
+    case 2:
+      if (s is T) {} // Make `T` a type of interest
+  }
+}
+
+test3() {
+  S s = S();
+  switch (42) {
+    case 1:
+      if (s is T) {}
+    case 2:
+      s = T();
+      s.answer();
+//      ^^^^^^
+// [analyzer] unspecified
+// [cfe] unspecified
+  }
+}
+
+test4() {
+  S s = S();
+  switch (42) {
+    label: case 1:
+      if (s is T) {}
+    case 2:
+      s = T();
+      s.answer();
+//      ^^^^^^
+// [analyzer] unspecified
+// [cfe] unspecified
+  }
+}
+
+main() {
+  print(test1);
+  print(test2);
+  print(test3);
+  print(test4);
+}
diff --git a/TypeSystem/flow-analysis/reachability_switch_expression_A04_t01.dart b/TypeSystem/flow-analysis/reachability_switch_expression_A04_t01.dart
new file mode 100644
index 0000000000..ccaa7d1b73
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_switch_expression_A04_t01.dart
@@ -0,0 +1,48 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion switch expression: If `N` is a switch expression of the form
+/// `switch (E) {alternatives}` then:
+/// - Let `before(E) = split(before(N))`.
+/// - For each case `Cj` in `alternatives` with expression `Ej`, for `j` in
+///   `1 .. k`:
+///   - Let `before(Ej) = after(E)`.
+/// - Let `after(N) = join(after(E1), after(E2), .. after(Ek))`.
+/// TODO (sgrekhov): there is no switch expression in the flow analysis spec yet
+/// (April 2025). Update the assertion after spec update.
+///
+/// @description Checks that if a type `T` is made a type of interest in `E`
+/// for a variable `s` then `s` can be promoted in `alternatives` and `after(N)`
+/// @author sgrekhov22@gmail.com
+/// @issue 60479
+/// @issue 60539
+
+class S {}
+
+class T extends S {
+  int answer() => 42;
+}
+
+void test1() {
+  S s = S();
+  var x = switch (s is T ? 1 : 2) { // Make `T` a type of interest
+    1 => [s = T(), s.answer()],
+    _ =>  []
+  };
+}
+
+void test2() {
+  S s = S();
+  var x = switch (s is T) {
+    true => 1,
+    _ =>  0
+  };
+  s = T();
+  s.answer();
+}
+
+main() {
+  test1();
+  test2();
+}
diff --git a/TypeSystem/flow-analysis/reachability_switch_expression_A04_t02.dart b/TypeSystem/flow-analysis/reachability_switch_expression_A04_t02.dart
new file mode 100644
index 0000000000..91e33a7e89
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_switch_expression_A04_t02.dart
@@ -0,0 +1,48 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion switch expression: If `N` is a switch expression of the form
+/// `switch (E) {alternatives}` then:
+/// - Let `before(E) = split(before(N))`.
+/// - For each case `Cj` in `alternatives` with expression `Ej`, for `j` in
+///   `1 .. k`:
+///   - Let `before(Ej) = after(E)`.
+/// - Let `after(N) = join(after(E1), after(E2), .. after(Ek))`.
+/// TODO (sgrekhov): there is no switch expression in the flow analysis spec yet
+/// (April 2025). Update the assertion after spec update.
+///
+/// @description Checks that if a type `T` is made a type of interest in
+/// `alternatives` for a variable `s` then `s` can be promoted in `alternatives`
+/// and `after(N)`.
+/// @author sgrekhov22@gmail.com
+/// @issue 60479
+/// @issue 60539
+
+class S {}
+
+class T extends S {
+  int answer() => 42;
+}
+
+void test1() {
+  S s = S();
+  var x = switch (42) {
+    1 => [s is T, s = T(), s.answer()],
+    _ => []
+  };
+}
+
+void test2() {
+  S s = S();
+  var x = switch (42) {
+    _ =>  s is T // Make `T` a type of interest
+  };
+  s = T();
+  s.answer();
+}
+
+main() {
+  test1();
+  test2();
+}
diff --git a/TypeSystem/flow-analysis/reachability_switch_expression_A04_t03.dart b/TypeSystem/flow-analysis/reachability_switch_expression_A04_t03.dart
new file mode 100644
index 0000000000..961367ebe2
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_switch_expression_A04_t03.dart
@@ -0,0 +1,51 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion switch expression: If `N` is a switch expression of the form
+/// `switch (E) {alternatives}` then:
+/// - Let `before(E) = split(before(N))`.
+/// - For each case `Cj` in `alternatives` with expression `Ej`, for `j` in
+///   `1 .. k`:
+///   - Let `before(Ej) = after(E)`.
+/// - Let `after(N) = join(after(E1), after(E2), .. after(Ek))`.
+/// TODO (sgrekhov): there is no switch expression in the flow analysis spec yet
+/// (April 2025). Update the assertion after spec update.
+///
+/// @description Checks that if a type `T` is made a type of interest for `s` in
+/// an alternative then there is no guarantee that `T` is a type of interest for
+/// `s` in any other alternative.
+/// @author sgrekhov22@gmail.com
+
+class S {}
+
+class T extends S {
+  int answer() => 42;
+}
+
+test1() {
+  S s = S();
+  var x = switch (42) {
+    1 => [s = T(), s.answer()],
+//                   ^^^^^^
+// [analyzer] unspecified
+// [cfe] unspecified
+    _ => [s is T ? 1: 2] // Make `T` a type of interest
+  };
+}
+
+test2() {
+  S s = S();
+  var x = switch (42) {
+    1 => [s is T ? 1: 2],
+    _ => [s = T(), s.answer()],
+//                   ^^^^^^
+// [analyzer] unspecified
+// [cfe] unspecified
+  };
+}
+
+main() {
+  print(test1);
+  print(test2);
+}