diff --git a/TypeSystem/flow-analysis/reachability_A12_t01.dart b/TypeSystem/flow-analysis/reachability_A12_t01.dart
index a6b33985f1..8ea59eaecd 100644
--- a/TypeSystem/flow-analysis/reachability_A12_t01.dart
+++ b/TypeSystem/flow-analysis/reachability_A12_t01.dart
@@ -5,10 +5,14 @@
 /// @assertion instance check If `N` is an expression of the form `E1 is S`
 /// where the static type of `E1` is `T` then:
 /// - Let `before(E1) = before(N)`
-/// - Let `true(N) = promote(E1, S, after(E1))`
-/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = unreachable(after(E1))`.
+///   - Let `false(N) = after(E1)`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, S, after(E1))`
+///   - Let `false(N) = promote(E1, factor(T, S), after(E1))`
 ///
-/// @description Checks that for expression of the form `E1 is S`
+/// @description Checks that for expression of the form `E1 is S`,
 /// `true(N) = promote(E1, S, after(E1))` and
 /// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
 /// the case `T` is `R?` and `Null <: S`.
diff --git a/TypeSystem/flow-analysis/reachability_A12_t02.dart b/TypeSystem/flow-analysis/reachability_A12_t02.dart
index b0df00ef5f..76651a191a 100644
--- a/TypeSystem/flow-analysis/reachability_A12_t02.dart
+++ b/TypeSystem/flow-analysis/reachability_A12_t02.dart
@@ -5,10 +5,14 @@
 /// @assertion instance check If `N` is an expression of the form `E1 is S`
 /// where the static type of `E1` is `T` then:
 /// - Let `before(E1) = before(N)`
-/// - Let `true(N) = promote(E1, S, after(E1))`
-/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = unreachable(after(E1))`.
+///   - Let `false(N) = after(E1)`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, S, after(E1))`
+///   - Let `false(N) = promote(E1, factor(T, S), after(E1))`
 ///
-/// @description Checks that for expression of the form `E1 is S`
+/// @description Checks that for expression of the form `E1 is S`,
 /// `true(N) = promote(E1, S, after(E1))` and
 /// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
 /// the case `T` is `R?` and `S` is not subtype of `Null`.
diff --git a/TypeSystem/flow-analysis/reachability_A12_t03.dart b/TypeSystem/flow-analysis/reachability_A12_t03.dart
index 0163cefa70..1f8b6cb111 100644
--- a/TypeSystem/flow-analysis/reachability_A12_t03.dart
+++ b/TypeSystem/flow-analysis/reachability_A12_t03.dart
@@ -5,10 +5,14 @@
 /// @assertion instance check If `N` is an expression of the form `E1 is S`
 /// where the static type of `E1` is `T` then:
 /// - Let `before(E1) = before(N)`
-/// - Let `true(N) = promote(E1, S, after(E1))`
-/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = unreachable(after(E1))`.
+///   - Let `false(N) = after(E1)`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, S, after(E1))`
+///   - Let `false(N) = promote(E1, factor(T, S), after(E1))`
 ///
-/// @description Checks that for expression of the form `E1 is S`
+/// @description Checks that for expression of the form `E1 is S`,
 /// `true(N) = promote(E1, S, after(E1))` and
 /// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
 /// the case `T` is `FutureOr<R>` and `Future<R> <: S`.
diff --git a/TypeSystem/flow-analysis/reachability_A12_t04.dart b/TypeSystem/flow-analysis/reachability_A12_t04.dart
index 563660c61f..f811948cfb 100644
--- a/TypeSystem/flow-analysis/reachability_A12_t04.dart
+++ b/TypeSystem/flow-analysis/reachability_A12_t04.dart
@@ -5,10 +5,14 @@
 /// @assertion instance check If `N` is an expression of the form `E1 is S`
 /// where the static type of `E1` is `T` then:
 /// - Let `before(E1) = before(N)`
-/// - Let `true(N) = promote(E1, S, after(E1))`
-/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = unreachable(after(E1))`.
+///   - Let `false(N) = after(E1)`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, S, after(E1))`
+///   - Let `false(N) = promote(E1, factor(T, S), after(E1))`
 ///
-/// @description Checks that for expression of the form `E1 is S`
+/// @description Checks that for expression of the form `E1 is S`,
 /// `true(N) = promote(E1, S, after(E1))` and
 /// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
 /// the case `T` is `FutureOr<R>` and `R <: S`.
diff --git a/TypeSystem/flow-analysis/reachability_A12_t05.dart b/TypeSystem/flow-analysis/reachability_A12_t05.dart
new file mode 100644
index 0000000000..7c8a9aa537
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A12_t05.dart
@@ -0,0 +1,32 @@
+// 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 instance check If `N` is an expression of the form `E1 is S`
+/// where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = unreachable(after(E1))`.
+///   - Let `false(N) = after(E1)`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, S, after(E1))`
+///   - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+///
+/// @description Checks that if `T` is a bottom type then
+/// `true(N) = unreachable(after(E1))`.
+/// @author sgrekhov22@gmail.com
+
+test(x) {
+  late int i;
+  if (x is Never) {
+    i = 42;
+  }
+  i; // Definitely unassigned.
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test);
+}
diff --git a/TypeSystem/flow-analysis/reachability_A12_t06.dart b/TypeSystem/flow-analysis/reachability_A12_t06.dart
new file mode 100644
index 0000000000..99880d6be5
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A12_t06.dart
@@ -0,0 +1,29 @@
+// 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 instance check If `N` is an expression of the form `E1 is S`
+/// where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = unreachable(after(E1))`.
+///   - Let `false(N) = after(E1)`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, S, after(E1))`
+///   - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+///
+/// @description Checks that if `T` is a bottom type then `false(N) = after(E1)`.
+/// @author sgrekhov22@gmail.com
+
+test(x) {
+  int i;
+  if (x is Never) {
+  } else {
+    i = 42;
+  }
+  i; // Definitely assigned.
+}
+
+main() {
+  test(null);
+}
diff --git a/TypeSystem/flow-analysis/reachability_A23_t01.dart b/TypeSystem/flow-analysis/reachability_A23_t01.dart
new file mode 100644
index 0000000000..6be7817f5b
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A23_t01.dart
@@ -0,0 +1,30 @@
+// 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 negated instance check If `N` is an expression of the form
+/// `E1 is! S` where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is! S`,
+/// `true(N) = promote(E1, factor(T, S), after(E1))` and
+/// `false(N) = promote(E1, S, after(E1))`. Test `factor(T, S)` for the case
+/// `T` is `R?` and `Null <: S`.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+main() {
+  int? i = 2 > 1 ? null : 42;
+  if (i is! Null) {
+    i.expectStaticType<Exactly<int>>();
+  } else {
+    Null n = i;
+  }
+}
diff --git a/TypeSystem/flow-analysis/reachability_A23_t02.dart b/TypeSystem/flow-analysis/reachability_A23_t02.dart
new file mode 100644
index 0000000000..d4a3660589
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A23_t02.dart
@@ -0,0 +1,30 @@
+// 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 negated instance check If `N` is an expression of the form
+/// `E1 is! S` where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is! S`,
+/// `true(N) = promote(E1, factor(T, S), after(E1))` and
+/// `false(N) = promote(E1, S, after(E1))`. Test `factor(T, S)` for the case
+/// `T` is `R?` and `S` is not subtype of `Null`.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+main() {
+  int? i = 2 > 1 ? null : 42;
+  if (i is! int) {
+    i.expectStaticType<Exactly<Null>>();
+  } else {
+    i.expectStaticType<Exactly<int>>();
+  }
+}
diff --git a/TypeSystem/flow-analysis/reachability_A23_t03.dart b/TypeSystem/flow-analysis/reachability_A23_t03.dart
new file mode 100644
index 0000000000..3a1b236b31
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A23_t03.dart
@@ -0,0 +1,37 @@
+// 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 negated instance check If `N` is an expression of the form
+/// `E1 is! S` where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is! S`,
+/// `true(N) = promote(E1, factor(T, S), after(E1))` and
+/// `false(N) = promote(E1, S, after(E1))`. Test `factor(T, S)` for the case
+/// `T` is `FutureOr<R>` and `Future<R> <: S`.
+/// @author sgrekhov22@gmail.com
+
+import 'dart:async';
+import '../../Utils/static_type_helper.dart';
+
+class C {}
+
+test(FutureOr<C> foc) async {
+  if (foc is! Future<C>) {
+    foc.expectStaticType<Exactly<C>>();
+  } else {
+    foc.expectStaticType<Exactly<Future<C>>>();
+  }
+}
+
+main() {
+  test(C());
+  test(Future<C>.value(C()));
+}
diff --git a/TypeSystem/flow-analysis/reachability_A23_t04.dart b/TypeSystem/flow-analysis/reachability_A23_t04.dart
new file mode 100644
index 0000000000..5f4f7ff1ce
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A23_t04.dart
@@ -0,0 +1,37 @@
+// 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 negated instance check If `N` is an expression of the form
+/// `E1 is! S` where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is! S`,
+/// `true(N) = promote(E1, factor(T, S), after(E1))` and
+/// `false(N) = promote(E1, S, after(E1))`. Test `factor(T, S)` for
+/// the case `T` is `FutureOr<R>` and `R <: S`.
+/// @author sgrekhov22@gmail.com
+
+import 'dart:async';
+import '../../Utils/static_type_helper.dart';
+
+class C {}
+
+test(FutureOr<C> foc) async {
+  if (foc is! C) {
+    foc.expectStaticType<Exactly<Future<C>>>();
+  } else {
+    foc.expectStaticType<Exactly<C>>();
+  }
+}
+
+main() {
+  test(C());
+  test(Future<C>.value(C()));
+}
diff --git a/TypeSystem/flow-analysis/reachability_A23_t05.dart b/TypeSystem/flow-analysis/reachability_A23_t05.dart
new file mode 100644
index 0000000000..e1394786b7
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A23_t05.dart
@@ -0,0 +1,28 @@
+// 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 negated instance check If `N` is an expression of the form
+/// `E1 is! S` where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that if `T` is a bottom type then `true(N) = after(E1)`.
+/// @author sgrekhov22@gmail.com
+
+test(x) {
+  int i;
+  if (x is! Never) {
+    i = 42;
+  }
+  i; // Definitely assigned.
+}
+
+main() {
+  test(null);
+}
diff --git a/TypeSystem/flow-analysis/reachability_A23_t06.dart b/TypeSystem/flow-analysis/reachability_A23_t06.dart
new file mode 100644
index 0000000000..45c0551dad
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A23_t06.dart
@@ -0,0 +1,33 @@
+// 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 negated instance check If `N` is an expression of the form
+/// `E1 is! S` where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - If `T` is a bottom type, then:
+///   - Let `true(N) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that if `T` is a bottom type then
+/// `false(N) = promote(E1, factor(T, S), after(E1))`.
+/// @author sgrekhov22@gmail.com
+
+test(x) {
+  late int i;
+  if (x is! Never) {
+  } else {
+    i = 42;
+  }
+  i; // Definitely unassigned.
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test);
+}