diff --git a/spec/lang/step/expressions.md b/spec/lang/step/expressions.md
index ca7544ca..54a7edd5 100644
--- a/spec/lang/step/expressions.md
+++ b/spec/lang/step/expressions.md
@@ -264,5 +264,16 @@ impl<M: Memory> Machine<M> {
         let ptr = self.ptr_offset_inbounds(root.ptr, offset.bytes())?;
         ret((Place { ptr, ..root }, field_ty))
     }
+
+    fn eval_place(&mut self, PlaceExpr::Downcast { root, variant_idx }: PlaceExpr) -> NdResult<(Place<M>, Type)> {
+        let (root, ty) = self.eval_place(root)?;
+        // We only need to downcast the enum type into the variant data type
+        // since all the enum data must have the same size with offset 0 (invariant).
+        let var_ty = match ty {
+            Type::Enum { variants, .. } => variants[variant_idx].ty,
+            _ => panic!("enum downcast on non-enum"),
+        };
+        ret((root, var_ty))
+    }
 }
 ```
diff --git a/spec/lang/syntax.md b/spec/lang/syntax.md
index 5fb79312..583d490c 100644
--- a/spec/lang/syntax.md
+++ b/spec/lang/syntax.md
@@ -175,6 +175,14 @@ pub enum PlaceExpr {
         #[specr::indirection]
         index: ValueExpr,
     },
+    /// Enum variant downcast.
+    Downcast {
+        /// The base enum to project to the specific variant.
+        #[specr::indirection]
+        root: PlaceExpr,
+        /// The variant index to project to.
+        variant_idx: Int,
+    },
 }
 ```
 
diff --git a/spec/lang/well-formed.md b/spec/lang/well-formed.md
index c103b64e..e10b0227 100644
--- a/spec/lang/well-formed.md
+++ b/spec/lang/well-formed.md
@@ -313,6 +313,14 @@ impl PlaceExpr {
                     _ => throw!(),
                 }
             }
+            Downcast { root, variant_idx } => {
+                let root = root.check_wf::<T>(locals, prog)?;
+                match root {
+                    // A valid downcast points to an existing variant.
+                    Type::Enum { variants, .. } => variants.get(variant_idx)?.ty,
+                    _ => throw!(),
+                }
+            }
         })
     }
 }
diff --git a/tooling/minitest/src/tests/enum_downcast.rs b/tooling/minitest/src/tests/enum_downcast.rs
new file mode 100644
index 00000000..768dccb0
--- /dev/null
+++ b/tooling/minitest/src/tests/enum_downcast.rs
@@ -0,0 +1,85 @@
+use crate::*;
+
+/// Ill-formed: Downcasting to an out-of-bounds variant.
+#[test]
+fn out_of_bounds_downcast() {
+    let u8_t = int_ty(Signedness::Unsigned, size(1));
+    let enum_ty = enum_ty(&[enum_variant(u8_t, &[])], Discriminator::Known(0.into()), size(1), align(1));
+    let locals = &[enum_ty, u8_t];
+    let stmts = &[
+        storage_live(0),
+        storage_live(1),
+        assign(local(1), load(downcast(local(0), 1))), // ill-formed here, variant 1 doesn't exist
+    ];
+    let prog = small_program(locals, stmts);
+    assert_ill_formed(prog);
+}
+
+/// Works: Both assigning to and from a downcast.
+#[test]
+fn valid_downcast() {
+    let u8_t = int_ty(Signedness::Unsigned, size(1));
+    let enum_ty = enum_ty(&[enum_variant(u8_t, &[])], Discriminator::Known(0.into()), size(1), align(1));
+    let locals = &[enum_ty, u8_t];
+    let stmts = &[
+        storage_live(0),
+        storage_live(1),
+        assign(downcast(local(0), 0), const_int(42u8)),
+        assign(local(1), load(downcast(local(0), 0))),
+    ];
+    let prog = small_program(locals, stmts);
+    assert_stop(prog);
+}
+
+
+/// UB: Assigning to first byte of variant 0 doesn't init both data bytes of variant 1.
+#[test]
+fn downcasts_give_different_place() {
+    // setup enum where the first two bytes are data (u8 / u16) and the third byte is the tag.
+    let u8_t = int_ty(Signedness::Unsigned, size(1));
+    let variant1 = enum_variant(tuple_ty(&[(size(1), u8_t)], size(4), align(2)), &[(size(2), 0u8)]);
+    let u16_t = int_ty(Signedness::Unsigned, size(2));
+    let variant2 = enum_variant(tuple_ty(&[(size(0), u16_t)], size(4), align(2)), &[(size(2), 1u8)]);
+    let discriminator = Discriminator::Unknown {
+        offset: size(2),
+        fallback: GcCow::new(Discriminator::Invalid),
+        children: [(0, Discriminator::Known(0.into())), (1, Discriminator::Known(1.into()))].into_iter().collect()
+    };
+    let enum_ty = enum_ty(&[variant1, variant2], discriminator, size(4), align(2));
+
+    let locals = &[enum_ty, u16_t];
+    let stmts = &[
+        storage_live(0),
+        storage_live(1),
+        assign(field(downcast(local(0), 0), 0), const_int(42u8)),
+        assign(local(1), load(field(downcast(local(0), 1), 0))), // UB here, only the lower byte is initialized
+    ];
+    let prog = small_program(locals, stmts);
+    assert_ub(prog, "load at type Int(IntType { signed: Unsigned, size: Size(2 bytes) }) but the data in memory violates the validity invariant");
+}
+
+/// Works: Assigning to both bytes of variant 1 allows reads from variant 0.
+#[test]
+fn downcasts_give_different_place2() {
+    // setup enum where the first two bytes are data (u8 / u16) and the third byte is the tag.
+    let u8_t = int_ty(Signedness::Unsigned, size(1));
+    let variant1 = enum_variant(tuple_ty(&[(size(1), u8_t)], size(4), align(2)), &[(size(2), 0)]);
+    let u16_t = int_ty(Signedness::Unsigned, size(2));
+    let variant2 = enum_variant(tuple_ty(&[(size(0), u16_t)], size(4), align(2)), &[(size(2), 1)]);
+    let discriminator = Discriminator::Unknown {
+        offset: size(2),
+        fallback: GcCow::new(Discriminator::Invalid),
+        children: [(0, Discriminator::Known(0.into())), (1, Discriminator::Known(1.into()))].into_iter().collect()
+    };
+    let enum_ty = enum_ty(&[variant1, variant2], discriminator, size(4), align(2));
+
+    let locals = &[enum_ty, u8_t];
+    let stmts = &[
+        storage_live(0),
+        storage_live(1),
+        assign(field(downcast(local(0), 1), 0), const_int(42u16)),
+        assign(local(1), load(field(downcast(local(0), 0), 0))),
+    ];
+    let prog = small_program(locals, stmts);
+    assert_stop(prog);
+}
diff --git a/tooling/minitest/src/tests/mod.rs b/tooling/minitest/src/tests/mod.rs
index b97503e6..16388e5f 100644
--- a/tooling/minitest/src/tests/mod.rs
+++ b/tooling/minitest/src/tests/mod.rs
@@ -6,6 +6,7 @@ mod concurrency;
 mod data_race;
 mod dereferenceable;
 mod div_zero;
+mod enum_downcast;
 mod enum_representation;
 mod heap_intrinsics;
 mod ill_formed;
diff --git a/tooling/miniutil/src/build/expr.rs b/tooling/miniutil/src/build/expr.rs
index 56c7aef7..d8997a03 100644
--- a/tooling/miniutil/src/build/expr.rs
+++ b/tooling/miniutil/src/build/expr.rs
@@ -216,6 +216,14 @@ pub fn index(root: PlaceExpr, index: ValueExpr) -> PlaceExpr {
     }
 }
 
+/// An enum downcast into the variant at the specified index.
+pub fn downcast(root: PlaceExpr, variant_idx: impl Into<Int>) -> PlaceExpr {
+    PlaceExpr::Downcast {
+        root: GcCow::new(root),
+        variant_idx: variant_idx.into(),
+    }
+}
+
 /// A place suited for zero-sized accesses.
 pub fn zst_place() -> PlaceExpr {
     let ptr = ValueExpr::Constant(Constant::InvalidPointer(1.into()), <*const ()>::get_type());
diff --git a/tooling/miniutil/src/fmt/expr.rs b/tooling/miniutil/src/fmt/expr.rs
index a7197535..3fdae0ad 100644
--- a/tooling/miniutil/src/fmt/expr.rs
+++ b/tooling/miniutil/src/fmt/expr.rs
@@ -53,6 +53,12 @@ pub(super) fn fmt_place_expr(p: PlaceExpr, comptypes: &mut Vec<CompType>) -> Fmt
             // This can be considered atomic due to the same reasoning as for PlaceExpr::Field, see above.
             FmtExpr::Atomic(format!("{root}[{index}]"))
         }
+        PlaceExpr::Downcast { root, variant_idx } => {
+            let root = fmt_place_expr(root.extract(), comptypes).to_atomic_string();
+            // This is not atomic as `local(1) as variant 3.0` illustrates. (Field 0 of downcast)
+            // We can't do it nicely like in the Rust MIR ({root} as {variant name}) since we have no variant names.
+            FmtExpr::NonAtomic(format!("{root} as variant {variant_idx}"))
+        }
     }
 }