diff --git a/source/vstd/std_specs/control_flow.rs b/source/vstd/std_specs/control_flow.rs
index 30c707f764..d46717f1de 100644
--- a/source/vstd/std_specs/control_flow.rs
+++ b/source/vstd/std_specs/control_flow.rs
@@ -15,6 +15,11 @@ pub struct ExControlFlow<B, C>(ControlFlow<B, C>);
 #[verifier::external_body]
 pub struct ExInfallible(Infallible);
 
+pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
+    requires
+        false,
+;
+
 pub assume_specification<T, E>[ Result::<T, E>::branch ](result: Result<T, E>) -> (cf: ControlFlow<
     <Result<T, E> as Try>::Residual,
     <Result<T, E> as Try>::Output,
diff --git a/source/vstd/std_specs/core.rs b/source/vstd/std_specs/core.rs
index 16f516e606..2514adb6e6 100644
--- a/source/vstd/std_specs/core.rs
+++ b/source/vstd/std_specs/core.rs
@@ -103,6 +103,21 @@ pub trait ExMetaSized {
     type ExternalTraitSpecificationFor: core::marker::MetaSized;
 }
 
+#[verifier::external_trait_specification]
+#[verifier::external_trait_extension(DefaultSpec via DefaultSpecImpl)]
+pub trait ExDefault: Sized {
+    type ExternalTraitSpecificationFor: core::default::Default;
+
+    spec fn obeys_default_spec() -> bool;
+
+    spec fn default_spec() -> Self;
+
+    fn default() -> (r: Self)
+        ensures
+            Self::obeys_default_spec() ==> r == Self::default_spec(),
+    ;
+}
+
 pub assume_specification<T>[ core::mem::swap::<T> ](a: &mut T, b: &mut T)
     ensures
         *a == *old(b),
@@ -211,3 +226,35 @@ pub fn index_set<T, Idx, E>(container: &mut T, index: Idx, val: E) where
 #[verifier::external_body]
 #[verifier::accept_recursive_types(T)]
 pub struct ExAssertParamIsClone<T: Clone + PointeeSized>(core::clone::AssertParamIsClone<T>);
+
+macro_rules! impl_default_spec {
+    ($t:ty, $default_value:expr) => {
+        verus_! {
+            pub assume_specification [ <$t as core::default::Default>::default ]() -> (r: $t);
+
+            impl DefaultSpecImpl for $t {
+                open spec fn obeys_default_spec() -> bool {
+                    true
+                }
+
+                open spec fn default_spec() -> Self {
+                    $default_value
+                }
+            }
+        }
+    };
+}
+
+impl_default_spec!(u8, 0u8);
+impl_default_spec!(u16, 0u16);
+impl_default_spec!(u32, 0u32);
+impl_default_spec!(u64, 0u64);
+impl_default_spec!(u128, 0u128);
+impl_default_spec!(usize, 0usize);
+impl_default_spec!(i8, 0i8);
+impl_default_spec!(i16, 0i16);
+impl_default_spec!(i32, 0i32);
+impl_default_spec!(i64, 0i64);
+impl_default_spec!(i128, 0i128);
+impl_default_spec!(isize, 0isize);
+impl_default_spec!(bool, false);
diff --git a/source/vstd/std_specs/slice.rs b/source/vstd/std_specs/slice.rs
index b15dfa079f..dfc5d8c838 100644
--- a/source/vstd/std_specs/slice.rs
+++ b/source/vstd/std_specs/slice.rs
@@ -1,14 +1,269 @@
 use super::super::prelude::*;
+use super::cmp::{OrdSpec, PartialEqSpec, PartialOrdSpec};
 use super::core::IndexSetTrustedSpec;
 use super::core::TrustedSpecSealed;
 
+use core::cmp::Ordering;
 use core::slice::Iter;
 
 use verus as verus_;
 
 verus_! {
 
-impl<T, const N: usize> TrustedSpecSealed for [T; N] {}
+pub open spec fn is_sorted_spec<T: PartialOrd>(s: Seq<T>) -> bool {
+    forall|i: int, j: int|
+        #![trigger s[i].partial_cmp_spec(&s[j])]
+        0 <= i < j < s.len() ==> s[i].partial_cmp_spec(&s[j]) == Some(Ordering::Less)
+            || s[i].partial_cmp_spec(&s[j]) == Some(Ordering::Equal)
+}
+
+pub open spec fn is_sorted_by_spec<'a, T: 'a, F: FnMut(&'a T, &'a T) -> bool>(
+    s: Seq<T>,
+    f: F,
+) -> bool {
+    forall|i: int, j: int, b: bool|
+        #![trigger f.ensures((&s[i], &s[j]), b)]
+        0 <= i < j < s.len() ==> f.ensures((&s[i], &s[j]), b) ==> b
+}
+
+pub open spec fn is_sorted_by_pivot_spec<'a, T: 'a, F: FnMut(&'a T) -> Ordering>(
+    s: Seq<T>,
+    f: F,
+) -> bool {
+    // The sequence is partitioned into [Less*, Equal*, Greater*]
+    forall|i: int, j: int, ord1: Ordering, ord2: Ordering|
+        #![trigger f.ensures((&s[i],), ord1), f.ensures((&s[j],), ord2)]
+        0 <= i < j < s.len() && f.ensures((&s[i],), ord1) && f.ensures(
+            (&s[j],),
+            ord2,
+        )
+        // Ordering itself is total.
+         ==> ord1.cmp_spec(&ord2) != Ordering::Greater
+}
+
+pub open spec fn is_sorted_by_key_spec<'a, T: 'a, F: FnMut(&'a T) -> K, K: PartialOrd>(
+    s: Seq<T>,
+    f: F,
+) -> bool {
+    forall|i: int, j: int, k1: K, k2: K|
+        #![trigger f.ensures((&s[i],), k1), f.ensures((&s[j],), k2)]
+        0 <= i < j < s.len() && f.ensures((&s[i],), k1) && f.ensures(
+            (&s[j],),
+            k2,
+        )
+        // K is partially ordered.
+         ==> k1.partial_cmp_spec(&k2) == Some(Ordering::Less) || k1.partial_cmp_spec(&k2) == Some(
+            Ordering::Equal,
+        )
+}
+
+pub assume_specification<T: PartialOrd>[ <[T]>::is_sorted ](s: &[T]) -> (r: bool)
+    ensures
+        r == is_sorted_spec(s@),
+;
+
+pub assume_specification<'a, T, F: FnMut(&'a T, &'a T) -> bool>[ <[T]>::is_sorted_by ](
+    s: &'a [T],
+    compare: F,
+) -> (r: bool)
+    ensures
+        r == is_sorted_by_spec(s@, compare),
+;
+
+pub assume_specification<'a, T, F: FnMut(&'a T) -> K, K: PartialOrd>[ <[T]>::is_sorted_by_key ](
+    s: &'a [T],
+    compare: F,
+) -> (r: bool)
+    ensures
+        r == is_sorted_by_key_spec(s@, compare),
+;
+
+/// Binary searches this slice for a given element.
+///
+/// Please be extra careful that if the slice is not properly sorted, the result is
+/// unspecified and meaningless.
+///
+/// See [here](https://doc.rust-lang.org/stable/core/primitive.slice.html#method.binary_search).
+pub assume_specification<T: Ord>[ <[T]>::binary_search ](s: &[T], x: &T) -> (r: Result<
+    usize,
+    usize,
+>)
+    ensures
+        is_sorted_spec(s@) ==> match r {
+            Ok(index) => {
+                &&& 0 <= index < s.len()
+                &&& s[index as int] == *x
+            },
+            Err(insert_index) => {
+                &&& 0 <= insert_index <= s.len()
+                &&& forall|i: int|
+                    #![trigger s[i].cmp_spec(x)]
+                    0 <= i < s.len() ==> {
+                        if i < insert_index {
+                            s[i].cmp_spec(x) != Ordering::Greater
+                        } else {
+                            s[i].cmp_spec(x) != Ordering::Less
+                        }
+                    }
+            },
+        },
+;
+
+/// Binary searches this slice with a comparator function.
+///
+/// Similar to `binary_search`, but allows the caller to provide a custom comparator function
+/// that compares each element to the desired pivot value.
+pub assume_specification<'a, T, F: FnMut(&'a T) -> Ordering>[ <[T]>::binary_search_by ](
+    s: &'a [T],
+    f: F,
+) -> (r: Result<usize, usize>)
+    ensures
+        is_sorted_by_pivot_spec(s@, f) ==> match r {
+            Ok(index) => {
+                &&& 0 <= index < s.len()
+                &&& forall|ord: Ordering|
+                    #![trigger f.ensures((&s[index as int],), ord)]
+                    f.ensures((&s[index as int],), ord) ==> ord == Ordering::Equal
+            },
+            Err(insert_index) => {
+                &&& 0 <= insert_index <= s.len()
+                &&& forall|i: int, ord: Ordering|
+                    #![trigger f.ensures((&s[i],), ord)]
+                    0 <= i < s.len() && i < insert_index && f.ensures((&s[i],), ord) ==> ord
+                        != Ordering::Greater
+                &&& forall|i: int, ord: Ordering|
+                    #![trigger f.ensures((&s[i],), ord)]
+                    0 <= i < s.len() && i >= insert_index && f.ensures((&s[i],), ord) ==> ord
+                        != Ordering::Less
+            },
+        },
+;
+
+/// Binary searches this slice with a key extraction function.
+pub assume_specification<'a, T, B: Ord, F: FnMut(&'a T) -> B>[ <[T]>::binary_search_by_key ](
+    s: &'a [T],
+    b: &B,
+    f: F,
+) -> (r: Result<usize, usize>)
+    ensures
+        is_sorted_by_key_spec(s@, f) ==> match r {
+            Ok(index) => {
+                &&& 0 <= index < s.len()
+                &&& forall|key: B|
+                    #![trigger f.ensures((&s[index as int],), key)]
+                    f.ensures((&s[index as int],), key) ==> key.cmp_spec(b) == Ordering::Equal
+            },
+            Err(insert_index) => {
+                &&& 0 <= insert_index <= s.len()
+                &&& forall|i: int, key: B|
+                    #![trigger f.ensures((&s[i],), key)]
+                    0 <= i < s.len() && i < insert_index && f.ensures((&s[i],), key)
+                        ==> key.cmp_spec(b) != Ordering::Greater
+                &&& forall|i: int, key: B|
+                    #![trigger f.ensures((&s[i],), key)]
+                    0 <= i < s.len() && i >= insert_index && f.ensures((&s[i],), key)
+                        ==> key.cmp_spec(b) != Ordering::Less
+            },
+        },
+;
+
+pub assume_specification<T: PartialEq>[ <[T]>::contains ](s: &[T], x: &T) -> (r: bool)
+    ensures
+        r <==> exists|i: int| 0 <= i < s.len() && #[trigger] s[i].eq_spec(x),
+;
+
+pub assume_specification<T: PartialEq>[ <[T]>::starts_with ](s: &[T], needle: &[T]) -> (r: bool)
+    ensures
+        r <==> {
+            &&& needle@.len() <= s@.len()
+            &&& forall|i: int| 0 <= i < needle@.len() ==> #[trigger] s[i].eq_spec(&needle[i])
+        },
+;
+
+pub assume_specification<T: PartialEq>[ <[T]>::ends_with ](s: &[T], needle: &[T]) -> (r: bool)
+    ensures
+        r <==> {
+            &&& needle@.len() <= s@.len()
+            &&& forall|i: int|
+                0 <= i < needle@.len() ==> s[(s@.len() - needle@.len()) + i].eq_spec(&needle[i])
+        },
+;
+
+pub assume_specification<T>[ <[T]>::swap ](s: &mut [T], i: usize, j: usize)
+    requires
+        0 <= i < old(s).len(),
+        0 <= j < old(s).len(),
+    ensures
+        s@ =~= old(s)@.update(i as int, old(s)@[j as int]).update(j as int, old(s)@[i as int]),
+;
+
+pub assume_specification<T>[ <[T]>::reverse ](s: &mut [T])
+    ensures
+        s@ =~= old(s)@.reverse(),
+;
+
+pub assume_specification<T>[ <[T]>::first ](s: &[T]) -> (r: Option<&T>)
+    ensures
+        r == if s@.len() == 0 {
+            None
+        } else {
+            Some(&s@.first())
+        },
+;
+
+pub assume_specification<T>[ <[T]>::last ](s: &[T]) -> (r: Option<&T>)
+    ensures
+        r == if s@.len() == 0 {
+            None
+        } else {
+            Some(&s@.last())
+        },
+;
+
+pub assume_specification<T>[ <[T]>::split_at_checked ](s: &[T], mid: usize) -> (r: Option<
+    (&[T], &[T]),
+>)
+    ensures
+        mid <= s@.len() ==> {
+            &&& r matches Some((left, right)) && {
+                &&& left@ =~= s@.subrange(0, mid as int)
+                &&& right@ =~= s@.subrange(mid as int, s@.len() as int)
+            }
+        },
+        mid > s@.len() ==> r matches None::<(&[T], &[T])>,
+;
+
+pub assume_specification<T>[ <[T]>::split_at ](s: &[T], mid: usize) -> (r: (&[T], &[T]))
+    ensures
+        mid <= s@.len() ==> {
+            &&& r.0@ =~= s@.subrange(0, mid as int)
+            &&& r.1@ =~= s@.subrange(mid as int, s@.len() as int)
+        },
+;
+
+pub assume_specification<T>[ <[T]>::rotate_left ](s: &mut [T], mid: usize)
+    ensures
+        mid <= s@.len() ==> s@ =~= old(s)@.subrange(mid as int, s@.len() as int) + old(s)@.subrange(
+            0,
+            mid as int,
+        ),
+;
+
+pub assume_specification<T>[ <[T]>::rotate_right ](s: &mut [T], mid: usize)
+    ensures
+        mid <= s@.len() ==> s@ =~= old(s)@.subrange((s@.len() - mid as int), s@.len() as int) + old(
+            s,
+        )@.subrange(0, (s@.len() - mid as int)),
+;
+
+pub assume_specification<T, const N: usize>[ <[[T; N]]>::as_flattened ](s: &[[T; N]]) -> (r: &[T])
+    ensures
+        r@ =~= Seq::new(s@.len() as nat, |i: int| s@[i]@).flatten(),
+;
+
+impl<T, const N: usize> TrustedSpecSealed for [T; N] {
+
+}
 
 impl<T, const N: usize> IndexSetTrustedSpec<usize> for [T; N] {
     open spec fn spec_index_set_requires(&self, index: usize) -> bool {
@@ -20,7 +275,9 @@ impl<T, const N: usize> IndexSetTrustedSpec<usize> for [T; N] {
     }
 }
 
-impl<T> TrustedSpecSealed for [T] {}
+impl<T> TrustedSpecSealed for [T] {
+
+}
 
 impl<T> IndexSetTrustedSpec<usize> for [T] {
     open spec fn spec_index_set_requires(&self, index: usize) -> bool {
@@ -32,11 +289,6 @@ impl<T> IndexSetTrustedSpec<usize> for [T] {
     }
 }
 
-pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
-    requires
-        false,
-;
-
 // The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
 // so we specify that type here.
 #[verifier::external_type_specification]