diff --git a/TypeSystem/flow-analysis/promotion_via_assignment_A07_t01.dart b/TypeSystem/flow-analysis/promotion_via_assignment_A07_t01.dart
new file mode 100644
index 0000000000..67a6fbdd96
--- /dev/null
+++ b/TypeSystem/flow-analysis/promotion_via_assignment_A07_t01.dart
@@ -0,0 +1,46 @@
+// 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 We say that a variable `x` is promotable via assignment of an
+/// expression of type `T` given variable model `VM` if
+/// - `VM = VariableModel(declared, promoted, tested, assigned, unassigned,
+///     captured)`
+/// - and captured is false
+/// - and `S` is the current type of `x` in `VM`
+/// - and `T <: S` and not `S <: T`
+/// - and `T` is a type of interest for `x` in `tested`
+///
+/// @description Checks that a variable is not promotable if `T` is not a
+/// subtype of `S`. Test extension types.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+extension type ET1(int v) {}
+extension type ET2(int v) implements Object {}
+extension type ET3(int v) implements int {}
+
+test1(Object? o) {
+  if (o is ET1) {}
+  o = 42;
+  o.expectStaticType<Exactly<Object>>();
+}
+
+test2(Object? o) {
+  if (o is ET2) {}
+  o = 42;
+  o.expectStaticType<Exactly<Object>>();
+}
+
+test3(Object? o) {
+  if (o is ET3) {}
+  o = 42;
+  o.expectStaticType<Exactly<Object>>();
+}
+
+main() {
+  test1(1);
+  test2(2);
+  test3(3);
+}
diff --git a/TypeSystem/flow-analysis/promotion_via_assignment_A07_t02.dart b/TypeSystem/flow-analysis/promotion_via_assignment_A07_t02.dart
new file mode 100644
index 0000000000..da8046c36b
--- /dev/null
+++ b/TypeSystem/flow-analysis/promotion_via_assignment_A07_t02.dart
@@ -0,0 +1,46 @@
+// 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 We say that a variable `x` is promotable via assignment of an
+/// expression of type `T` given variable model `VM` if
+/// - `VM = VariableModel(declared, promoted, tested, assigned, unassigned,
+///     captured)`
+/// - and captured is false
+/// - and `S` is the current type of `x` in `VM`
+/// - and `T <: S` and not `S <: T`
+/// - and `T` is a type of interest for `x` in `tested`
+///
+/// @description Checks that a variable is not promotable if `T` is not a
+/// subtype of `S`. Test extension types.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+extension type ET1(int v) {}
+extension type ET2(int v) implements Object {}
+extension type ET3(int v) implements int {}
+
+test1(num o) {
+  if (o is ET1) {}
+  o = 42;
+  o.expectStaticType<Exactly<num>>();
+}
+
+test2(num o) {
+  if (o is ET2) {}
+  o = 42;
+  o.expectStaticType<Exactly<num>>();
+}
+
+test3(num o) {
+  if (o is ET3) {}
+  o = 42;
+  o.expectStaticType<Exactly<num>>();
+}
+
+main() {
+  test1(1);
+  test2(2);
+  test3(3);
+}
diff --git a/TypeSystem/flow-analysis/promotion_via_type_test_A05_t01.dart b/TypeSystem/flow-analysis/promotion_via_type_test_A05_t01.dart
new file mode 100644
index 0000000000..4b1aab9efa
--- /dev/null
+++ b/TypeSystem/flow-analysis/promotion_via_type_test_A05_t01.dart
@@ -0,0 +1,47 @@
+// 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 We say that a variable `x` is promotable via type test with type
+/// `T` given variable model `VM` if
+/// - `VM = VariableModel(declared, promoted, tested, assigned, unassigned,
+///     captured)`
+/// - and `captured` is `false`
+/// - and `S` is the current type of `x` in `VM`
+/// - and not `S <: T`
+/// - and `T <: S` or (`S` is `X extends R` and `T <: R`) or (`S` is `X & R` and
+///   `T <: R`)
+///
+/// @description Checks that a variable is not promotable if `T` is not a
+/// subtype of `S`. Test extension types.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+extension type ET1(num v) {}
+extension type ET2(num v) implements Object {}
+extension type ET3(num v) implements num {}
+
+test1(ET1 et) {
+  if (et is int) {
+    et.expectStaticType<Exactly<ET1>>();
+  }
+}
+
+test2(ET2 et) {
+  if (et is int) {
+    et.expectStaticType<Exactly<ET2>>();
+  }
+}
+
+test3(ET3 et) {
+  if (et is int) {
+    et.expectStaticType<Exactly<ET3>>();
+  }
+}
+
+main() {
+  test1(ET1(0));
+  test2(ET2(0));
+  test3(ET3(0));
+}
diff --git a/TypeSystem/flow-analysis/promotion_via_type_test_A05_t02.dart b/TypeSystem/flow-analysis/promotion_via_type_test_A05_t02.dart
new file mode 100644
index 0000000000..9519c2c050
--- /dev/null
+++ b/TypeSystem/flow-analysis/promotion_via_type_test_A05_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 We say that a variable `x` is promotable via type test with type
+/// `T` given variable model `VM` if
+/// - `VM = VariableModel(declared, promoted, tested, assigned, unassigned,
+///     captured)`
+/// - and `captured` is `false`
+/// - and `S` is the current type of `x` in `VM`
+/// - and not `S <: T`
+/// - and `T <: S` or (`S` is `X extends R` and `T <: R`) or (`S` is `X & R` and
+///   `T <: R`)
+///
+/// @description Checks that a variable is not promotable if `T` is not a
+/// subtype of `S`. Test extension types.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+extension type ET1(int v) {}
+extension type ET2(int v) implements Object {}
+extension type ET3(int v) implements int {}
+
+test1() {
+  num n = 42;
+  if (n is ET1) {
+    n.expectStaticType<Exactly<num>>();
+  }
+}
+
+test2() {
+  num n = 42;
+  if (n is ET2) {
+    n.expectStaticType<Exactly<num>>();
+  }
+}
+
+test3() {
+  num n = 42;
+  if (n is ET3) {
+    n.expectStaticType<Exactly<ET3>>(); // Promotable in this case
+  }
+}
+
+main() {
+  test1();
+  test2();
+  test3();
+}