diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
index b76fb1a3..01ccd1c3 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -476,6 +476,27 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             Rvalue::UnaryOp(op, operand) => {
                 let operand_ty = self.operand_type(operand);
 
+                // PtrMetadata extracts the length from a fat-pointer slice (&[T]).
+                // In the model, &[T] is &immut TupleType([Box<Array<Int,T>>, Box<Int>]),
+                // so the length is (*operand).1.
+                if op == mir::UnOp::PtrMetadata {
+                    if let rty::Type::Pointer(ref ptr) = operand_ty.ty {
+                        if matches!(ptr.kind, rty::PointerKind::Ref(rty::RefKind::Immut))
+                            && operand_ty
+                                .ty
+                                .as_pointer()
+                                .unwrap()
+                                .elem
+                                .ty
+                                .as_tuple()
+                                .is_some()
+                        {
+                            return operand_ty.deref().tuple_proj(1).deref();
+                        }
+                    }
+                    unimplemented!("PtrMetadata on {:?}", operand_ty.ty);
+                }
+
                 let mut builder = PlaceTypeBuilder::default();
                 let (operand_ty, operand_term) = builder.subsume(operand_ty);
                 match (&operand_ty, op) {
@@ -535,63 +556,93 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 builder.build(rty::PointerType::immut_to(ty).into(), chc::Term::box_(term))
             }
             Rvalue::Aggregate(kind, fields) => {
-                // elaboration: all fields are boxed
-                let field_tys: Vec<_> = fields
-                    .into_iter()
-                    .map(|operand| self.operand_type(operand).boxed())
-                    .collect();
                 match *kind {
-                    mir::AggregateKind::Adt(did, variant_idx, args, _, _)
-                        if self.tcx.def_kind(did) == DefKind::Enum =>
-                    {
-                        let enum_def = self.ctx.get_or_register_enum_def(did);
-                        let variant_def = &enum_def.variants[variant_idx];
-                        let variant_rtys = variant_def
-                            .field_tys
-                            .clone()
+                    mir::AggregateKind::Array(mir_elem_ty) => {
+                        // Elements go directly into the array — do not box them.
+                        let elem_ptys: Vec<_> = fields
                             .into_iter()
-                            .map(|ty| rty::RefinedType::unrefined(ty.vacuous()));
-
-                        let rty_args: IndexVec<_, _> = args
-                            .types()
-                            .map(|ty| {
-                                self.type_builder
-                                    .for_template(&mut self.ctx)
-                                    .with_scope(&self.env)
-                                    .build_refined(ty)
-                            })
+                            .map(|operand| self.operand_type(operand))
                             .collect();
-                        for (field_pty, mut variant_rty) in
-                            field_tys.clone().into_iter().zip(variant_rtys)
-                        {
-                            variant_rty.instantiate_ty_params(rty_args.clone());
-                            let cs = self
-                                .env
-                                .relate_sub_refined_type(&field_pty.into(), &variant_rty.boxed());
-                            self.ctx.extend_clauses(cs);
-                        }
-
-                        let sort_args: Vec<_> =
-                            rty_args.iter().map(|rty| rty.ty.to_sort()).collect();
-                        let ty = rty::EnumType::new(enum_def.name.clone(), rty_args).into();
-
                         let mut builder = PlaceTypeBuilder::default();
-                        let mut field_terms = Vec::new();
-                        for field_ty in field_tys {
-                            let (_, field_term) = builder.subsume(field_ty);
-                            field_terms.push(field_term);
+                        let elem_ty = elem_ptys.first().map_or_else(
+                            || self.type_builder.build(mir_elem_ty).vacuous(),
+                            |p| p.ty.clone(),
+                        );
+                        let base_idx = builder.push_existential(chc::Sort::array(
+                            chc::Sort::int(),
+                            elem_ty.to_sort(),
+                        ));
+                        let mut arr_term: chc::Term<PlaceTypeVar> = chc::Term::var(base_idx.into());
+                        for (i, pty) in elem_ptys.into_iter().enumerate() {
+                            let (_, elem_term) = builder.subsume(pty);
+                            arr_term = arr_term.store(chc::Term::int(i as i64), elem_term);
                         }
                         builder.build(
-                            ty,
-                            chc::Term::datatype_ctor(
-                                enum_def.name,
-                                sort_args,
-                                variant_def.name.clone(),
-                                field_terms,
-                            ),
+                            rty::ArrayType::new(rty::Type::int(), elem_ty).into(),
+                            arr_term,
                         )
                     }
-                    _ => PlaceType::tuple(field_tys),
+                    other => {
+                        // elaboration: all fields are boxed
+                        let field_tys: Vec<_> = fields
+                            .into_iter()
+                            .map(|operand| self.operand_type(operand).boxed())
+                            .collect();
+                        match other {
+                            mir::AggregateKind::Adt(did, variant_idx, args, _, _)
+                                if self.tcx.def_kind(did) == DefKind::Enum =>
+                            {
+                                let enum_def = self.ctx.get_or_register_enum_def(did);
+                                let variant_def = &enum_def.variants[variant_idx];
+                                let variant_rtys = variant_def
+                                    .field_tys
+                                    .clone()
+                                    .into_iter()
+                                    .map(|ty| rty::RefinedType::unrefined(ty.vacuous()));
+
+                                let rty_args: IndexVec<_, _> = args
+                                    .types()
+                                    .map(|ty| {
+                                        self.type_builder
+                                            .for_template(&mut self.ctx)
+                                            .with_scope(&self.env)
+                                            .build_refined(ty)
+                                    })
+                                    .collect();
+                                for (field_pty, mut variant_rty) in
+                                    field_tys.clone().into_iter().zip(variant_rtys)
+                                {
+                                    variant_rty.instantiate_ty_params(rty_args.clone());
+                                    let cs = self.env.relate_sub_refined_type(
+                                        &field_pty.into(),
+                                        &variant_rty.boxed(),
+                                    );
+                                    self.ctx.extend_clauses(cs);
+                                }
+
+                                let sort_args: Vec<_> =
+                                    rty_args.iter().map(|rty| rty.ty.to_sort()).collect();
+                                let ty = rty::EnumType::new(enum_def.name.clone(), rty_args).into();
+
+                                let mut builder = PlaceTypeBuilder::default();
+                                let mut field_terms = Vec::new();
+                                for field_ty in field_tys {
+                                    let (_, field_term) = builder.subsume(field_ty);
+                                    field_terms.push(field_term);
+                                }
+                                builder.build(
+                                    ty,
+                                    chc::Term::datatype_ctor(
+                                        enum_def.name,
+                                        sort_args,
+                                        variant_def.name.clone(),
+                                        field_terms,
+                                    ),
+                                )
+                            }
+                            _ => PlaceType::tuple(field_tys),
+                        }
+                    }
                 }
             }
             Rvalue::Cast(
@@ -608,6 +659,27 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 };
                 PlaceType::with_ty_and_term(func_ty.vacuous(), chc::Term::null())
             }
+            Rvalue::Cast(
+                mir::CastKind::PointerCoercion(mir_ty::adjustment::PointerCoercion::Unsize, _),
+                operand,
+                _ty,
+            ) => {
+                // &[T; N] → &[T]: build the slice model (Array<Int,T>, N).
+                // Read MIR type before consuming operand.
+                let src_mir_ty = operand.ty(&self.local_decls, self.tcx);
+                let mir_ty::TyKind::Ref(_, inner_mir_ty, _) = src_mir_ty.kind() else {
+                    unimplemented!("Unsize coercion of non-reference: {:?}", src_mir_ty)
+                };
+                let mir_ty::TyKind::Array(_, len_const) = inner_mir_ty.kind() else {
+                    unimplemented!("Unsize coercion of non-array reference: {:?}", inner_mir_ty)
+                };
+                let n = len_const
+                    .try_to_target_usize(self.tcx)
+                    .expect("array length must be a known constant");
+                let arr_pty = self.operand_type(operand).deref();
+                let n_pty = PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(n as i64));
+                PlaceType::tuple(vec![arr_pty.boxed(), n_pty.boxed()]).immut()
+            }
             Rvalue::Discriminant(place) => {
                 let place = self.elaborate_place(&place);
                 let ty = self.env.place_type(place);
@@ -622,6 +694,32 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 let (_, term) = builder.subsume(ty);
                 builder.build(rty::Type::Int, chc::Term::datatype_discr(sym, term))
             }
+            Rvalue::Len(place) => {
+                let model_place = self.elaborate_place(&place);
+                let place_ty = self.env.place_type(model_place);
+                match &place_ty.ty {
+                    rty::Type::Tuple(_) => {
+                        // Slice model: TupleType([Box<Array<Int,T>>, Box<Int>])
+                        // Length is element 1 (boxed Int): project then deref the box
+                        place_ty.tuple_proj(1).deref()
+                    }
+                    rty::Type::Array(_) => {
+                        // Static array [T; N]: length is the const N from the MIR type
+                        let mir_ty = place.ty(&self.local_decls, self.tcx).ty;
+                        let mir_ty::TyKind::Array(_, len_const) = mir_ty.kind() else {
+                            unimplemented!(
+                                "Rvalue::Len: Array model type but MIR type is {:?}",
+                                mir_ty
+                            )
+                        };
+                        let n = len_const
+                            .try_to_target_usize(self.tcx)
+                            .expect("array length must be a known constant");
+                        PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(n as i64))
+                    }
+                    _ => unimplemented!("Rvalue::Len for model type: {:?}", place_ty.ty),
+                }
+            }
             _ => unimplemented!(
                 "rvalue={:?} ({:?})",
                 rvalue,
diff --git a/src/refine/env.rs b/src/refine/env.rs
index d9c3dfbc..d4d2ed1f 100644
--- a/src/refine/env.rs
+++ b/src/refine/env.rs
@@ -1051,6 +1051,7 @@ enum Path {
     Deref(Box<Path>),
     TupleProj(Box<Path>, usize),
     Downcast(Box<Path>, VariantIdx, FieldIdx),
+    Index(Box<Path>, Local),
 }
 
 impl<'tcx> From<Place<'tcx>> for Path {
@@ -1067,6 +1068,7 @@ impl<'tcx> From<Place<'tcx>> for Path {
                     };
                     Path::Downcast(Box::new(path), variant_idx, field_idx)
                 }
+                Some(PlaceElem::Index(local)) => Path::Index(Box::new(path), local),
                 None => break,
                 _ => unimplemented!(),
             };
@@ -1099,6 +1101,29 @@ where
                 self.path_type(path)
                     .downcast(*variant_idx, *field_idx, &self.enum_defs)
             }
+            Path::Index(path, idx_local) => {
+                let inner_pty = self.path_type(path);
+                let idx_pty = self.local_type(*idx_local);
+                // Normalize to an Array PlaceType:
+                //   slice model (Tuple) → get field 0 (Box<Array>) then deref
+                //   static array (Array) → already an Array
+                let arr_pty = match inner_pty.ty.clone() {
+                    rty::Type::Tuple(_) => inner_pty.tuple_proj(0).deref(),
+                    rty::Type::Array(_) => inner_pty,
+                    ty => unimplemented!("PlaceElem::Index on non-array/slice type: {:?}", ty),
+                };
+                let rty::Type::Array(arr_ty) = arr_pty.ty.clone() else {
+                    unreachable!("expected Array type after index normalization")
+                };
+                let elem_refined_ty = *arr_ty.elem;
+                let mut builder = refine::PlaceTypeBuilder::default();
+                let (_, arr_term) = builder.subsume(arr_pty);
+                let (_, idx_term) = builder.subsume(idx_pty);
+                let (elem_ty, value_var_ex) = builder.subsume_rty(elem_refined_ty);
+                let elem_term = crate::chc::Term::var(value_var_ex.into());
+                builder.push_formula(elem_term.clone().equal_to(arr_term.select(idx_term)));
+                builder.build(elem_ty, elem_term)
+            }
         }
     }
 
diff --git a/std.rs b/std.rs
index 132e3859..d53fed3a 100644
--- a/std.rs
+++ b/std.rs
@@ -188,6 +188,15 @@ mod thrust_models {
                 unimplemented!()
             }
         }
+
+        pub struct Slice<T: ?Sized>(pub Array<Int, T>, pub Int);
+
+        impl<T, U> PartialEq<U> for Slice<T> where U: super::Model<Ty = Self> {
+            #[thrust::ignored]
+            fn eq(&self, _other: &U) -> bool {
+                unimplemented!()
+            }
+        }
     }
 
     impl Model for model::Int {
@@ -310,6 +319,18 @@ mod thrust_models {
         type Ty = model::Vec<T>;
     }
 
+    impl<T: Model> Model for [T] {
+        type Ty = model::Slice<<T as Model>::Ty>;
+    }
+
+    impl<T: ?Sized> Model for model::Slice<T> {
+        type Ty = model::Slice<T>;
+    }
+
+    impl<T: Model, const N: usize> Model for [T; N] {
+        type Ty = model::Array<model::Int, <T as Model>::Ty>;
+    }
+
     impl<T> Model for Option<T> where T: Model {
         type Ty = Option<<T as Model>::Ty>;
     }
@@ -740,3 +761,43 @@ fn _extern_spec_partialord_gt<T>(x: &T, y: &T) -> bool
 {
     PartialOrd::gt(x, y)
 }
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == slice.1)]
+fn _extern_spec_slice_len<T>(slice: &[T]) -> usize
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::len(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(index < slice.1)]
+#[thrust_macros::ensures(*result == slice.0[index])]
+fn _extern_spec_slice_index<T>(slice: &[T], index: usize) -> &T
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T] as std::ops::Index<usize>>::index(slice, index)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(index < (*slice).1)]
+#[thrust_macros::ensures(
+    *result == (*slice).0[index] &&
+    !result == (!slice).0[index] &&
+    !slice == thrust_models::model::Slice((*slice).0.store(index, !result), (*slice).1)
+)]
+fn _extern_spec_slice_index_mut<T>(slice: &mut [T], index: usize) -> &mut T
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T] as std::ops::IndexMut<usize>>::index_mut(slice, index)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == (slice.1 == 0))]
+fn _extern_spec_slice_is_empty<T>(slice: &[T]) -> bool
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::is_empty(slice)
+}
diff --git a/tests/ui/fail/array_literal_1.rs b/tests/ui/fail/array_literal_1.rs
new file mode 100644
index 00000000..1fa49d74
--- /dev/null
+++ b/tests/ui/fail/array_literal_1.rs
@@ -0,0 +1,9 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [1i32, 2, 3];
+    let s: &[i32] = &arr;
+    let v = s[0];
+    assert!(v == 99);
+}
diff --git a/tests/ui/fail/array_literal_2.rs b/tests/ui/fail/array_literal_2.rs
new file mode 100644
index 00000000..99ccdb15
--- /dev/null
+++ b/tests/ui/fail/array_literal_2.rs
@@ -0,0 +1,8 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [0i32, 0, 0, 0];
+    let s: &[i32] = &arr;
+    let _ = s[4];
+}
diff --git a/tests/ui/fail/slice_1.rs b/tests/ui/fail/slice_1.rs
new file mode 100644
index 00000000..5635f546
--- /dev/null
+++ b/tests/ui/fail/slice_1.rs
@@ -0,0 +1,14 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.1 == 0)]
+fn empty_slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let s = empty_slice();
+    let _ = s[0];
+}
diff --git a/tests/ui/fail/slice_2.rs b/tests/ui/fail/slice_2.rs
new file mode 100644
index 00000000..8229a5a2
--- /dev/null
+++ b/tests/ui/fail/slice_2.rs
@@ -0,0 +1,14 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.1 >= 2)]
+fn two_elem_slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let s = two_elem_slice();
+    let _ = s[2];
+}
diff --git a/tests/ui/pass/array_literal_1.rs b/tests/ui/pass/array_literal_1.rs
new file mode 100644
index 00000000..4a563891
--- /dev/null
+++ b/tests/ui/pass/array_literal_1.rs
@@ -0,0 +1,9 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [1i32, 2, 3];
+    let s: &[i32] = &arr;
+    let v = s[0];
+    assert!(v == 1);
+}
diff --git a/tests/ui/pass/array_literal_2.rs b/tests/ui/pass/array_literal_2.rs
new file mode 100644
index 00000000..abbc05e6
--- /dev/null
+++ b/tests/ui/pass/array_literal_2.rs
@@ -0,0 +1,8 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [0i32, 0, 0, 0];
+    let s: &[i32] = &arr;
+    let _ = s[3];
+}
diff --git a/tests/ui/pass/slice_1.rs b/tests/ui/pass/slice_1.rs
new file mode 100644
index 00000000..7c7d0d3e
--- /dev/null
+++ b/tests/ui/pass/slice_1.rs
@@ -0,0 +1,15 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.1 > 0)]
+fn nonempty_slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let s = nonempty_slice();
+    assert!(s.len() > 0);
+    let _ = s[0];
+}
diff --git a/tests/ui/pass/slice_2.rs b/tests/ui/pass/slice_2.rs
new file mode 100644
index 00000000..ab0ab992
--- /dev/null
+++ b/tests/ui/pass/slice_2.rs
@@ -0,0 +1,15 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.1 >= 2)]
+fn two_elem_slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let s = two_elem_slice();
+    let _ = s[0];
+    let _ = s[1];
+}