diff --git a/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move b/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move
index fd40cee0fb6..353a17d7fe8 100644
--- a/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move
@@ -26,6 +26,12 @@ spec aptos_framework::big_ordered_map {
     spec new_with_config {
         pragma verify = false;
         pragma opaque;
+        aborts_if inner_max_degree != 0
+            && (inner_max_degree < 4 || (inner_max_degree as u64) > 4096);
+        aborts_if leaf_max_degree != 0
+            && (leaf_max_degree < 3 || (leaf_max_degree as u64) > 4096);
+        ensures spec_len(result) == 0;
+        ensures forall k: K: !spec_contains_key(result, k);
     }
 
     spec new {
@@ -35,11 +41,17 @@ spec aptos_framework::big_ordered_map {
     spec new_with_reusable {
         pragma verify = false;
         pragma opaque;
+        aborts_if false;
+        ensures spec_len(result) == 0;
+        ensures forall k: K: !spec_contains_key(result, k);
     }
 
     spec new_with_type_size_hints {
         pragma verify = false;
         pragma opaque;
+        aborts_if false;
+        ensures spec_len(result) == 0;
+        ensures forall k: K: !spec_contains_key(result, k);
     }
 
     spec borrow {
@@ -65,12 +77,43 @@ spec aptos_framework::big_ordered_map {
     spec remove {
         pragma opaque;
         pragma verify = false;
-        aborts_if [abstract] !spec_contains_key(self, key);
-        ensures [abstract] !spec_contains_key(self, key);
-        ensures [abstract] spec_get(old(self), key) == result;
-        ensures [abstract] spec_len(old(self)) == spec_len(self) + 1;
-        ensures [abstract] forall k: K where k != key: spec_contains_key(self, k) ==> spec_get(self, k) == spec_get(old(self), k);
-        ensures [abstract] forall k: K where k != key: spec_contains_key(old(self), k) == spec_contains_key(self, k);
+        aborts_if !spec_contains_key(self, key);
+        ensures !spec_contains_key(self, key);
+        ensures spec_get(old(self), key) == result;
+        ensures spec_len(old(self)) == spec_len(self) + 1;
+        ensures spec_unchanged_except_at(self, old(self), key);
+        // ensures forall k: K where k != key: spec_contains_key(self, k) ==> spec_get(self, k) == spec_get(old(self), k);
+        // ensures forall k: K where k != key: spec_contains_key(old(self), k) == spec_contains_key(self, k);
+    }
+
+    spec fun spec_unchanged_except_at<K: drop + copy + store, V: store>(
+        new_map: BigOrderedMap<K, V>, old_map: BigOrderedMap<K, V>, key: &K
+    ): bool {
+        (forall k: K where k != key:
+            spec_contains_key(new_map, k) == spec_contains_key(old_map, k))
+        && (forall k: K where k != key && spec_contains_key(old_map, k):
+            spec_get(new_map, k) == spec_get(old_map, k))
+    }
+
+    spec remove_or_none<K: drop + copy + store, V: store>(
+        self: &mut BigOrderedMap<K, V>, key: &K
+    ): Option<V> {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if false;
+        // Hit: key was present
+        ensures spec_contains_key(old(self), key) ==> (
+            option::is_some(result)
+            && option::spec_borrow(result) == spec_get(old(self), key)
+            && !spec_contains_key(self, key)
+            && spec_len(self) == spec_len(old(self)) - 1
+        );
+        // Miss: key was absent — map unchanged
+        ensures !spec_contains_key(old(self), key) ==> (
+            option::is_none(result)
+            && spec_len(self) == spec_len(old(self))
+        );
+        ensures spec_unchanged_except_at(self, old(self), key);
     }
 
     spec is_empty {
@@ -80,31 +123,63 @@ spec aptos_framework::big_ordered_map {
     spec iter_is_end {
         pragma opaque;
         pragma verify = false;
+        aborts_if false;
+        ensures result == (self is IteratorPtr::End<K>);
     }
 
     spec iter_borrow {
         pragma opaque;
         pragma verify = false;
+        aborts_if iter_is_end(self, map);
+        ensures result == spec_get(map, self.key);
     }
 
+    // Body also asserts constant_kv_size OR bcs::constant_serialized_size<V>().is_some()
+    // which is not expressible from spec context. Caller-side, iter_is_end is what's discharged.
     spec iter_borrow_mut {
         pragma opaque;
         pragma verify = false;
+        aborts_if iter_is_end(self, map);
+        ensures result == spec_get(map, self.key);
     }
 
     spec iter_is_begin {
         pragma opaque;
         pragma verify = false;
-    }
-
+        aborts_if false;
+        // self is End: returns true iff map is empty (End acts as both begin and end on []).
+        ensures (self is IteratorPtr::End<K>) ==> (result <==> spec_len(map) == 0);
+        // self is Some: returns true iff self.key is the smallest key currently in map.
+        ensures !(self is IteratorPtr::End<K>) ==> (result <==>
+            (spec_contains_key(map, self.key)
+                && (forall k: K where spec_contains_key(map, k) && k != self.key:
+                    std::cmp::compare(self.key, k) == std::cmp::Ordering::Less)));
+    }
+
+    // Returns the iterator pointing to the smallest key K in self with K >= input
+    // key (compare not Less), or End if no such key exists.
     spec internal_lower_bound {
         pragma opaque;
         pragma verify = false;
+        aborts_if false;
+        // End iff no key >= input exists (all keys are Less than input).
+        ensures iter_is_end(result, self) <==>
+            (forall k: K where spec_contains_key(self, k):
+                std::cmp::compare(k, key) == std::cmp::Ordering::Less);
+        // Otherwise, result.key is in the map, >= input, and the smallest such.
+        ensures !iter_is_end(result, self) ==> spec_contains_key(self, result.key);
+        ensures !iter_is_end(result, self) ==>
+            std::cmp::compare(result.key, key) != std::cmp::Ordering::Less;
+        ensures !iter_is_end(result, self) ==>
+            (forall k: K where spec_contains_key(self, k) && std::cmp::compare(k, key) != std::cmp::Ordering::Less:
+                std::cmp::compare(result.key, k) != std::cmp::Ordering::Greater);
     }
 
     spec iter_borrow_key {
         pragma opaque;
         pragma verify = false;
+        aborts_if self is IteratorPtr::End<K>;
+        ensures result == self.key;
     }
 
     spec allocate_spare_slots {
@@ -130,32 +205,30 @@ spec aptos_framework::big_ordered_map {
     spec keys {
         pragma verify = false;
         pragma opaque;
-        ensures [abstract] forall k: K: vector::spec_contains(result, k) <==> spec_contains_key(self, k);
+        ensures forall k: K: vector::spec_contains(result, k) <==> spec_contains_key(self, k);
     }
 
     spec new_from<K: drop + copy + store, V: store>(keys: vector<K>, values: vector<V>): BigOrderedMap<K, V> {
         pragma opaque;
         pragma verify = false;
-        aborts_if [abstract] exists i in 0..len(keys), j in 0..len(keys) where i != j : keys[i] == keys[j];
-        aborts_if [abstract] len(keys) != len(values);
-        ensures [abstract] forall k: K {spec_contains_key(result, k)} : vector::spec_contains(keys,k) <==> spec_contains_key(result, k);
-        ensures [abstract] forall i in 0..len(keys) : spec_get(result, keys[i]) == values[i];
-        ensures [abstract] spec_len(result) == len(keys);
+        aborts_if exists i in 0..len(keys), j in 0..len(keys) where i != j : keys[i] == keys[j];
+        aborts_if len(keys) != len(values);
+        ensures forall k: K {spec_contains_key(result, k)} : vector::spec_contains(keys,k) <==> spec_contains_key(result, k);
+        ensures forall i in 0..len(keys) : spec_get(result, keys[i]) == values[i];
+        ensures spec_len(result) == len(keys);
     }
 
     spec upsert {
         pragma opaque;
         pragma verify = false;
-        ensures [abstract] !spec_contains_key(old(self), key) ==> option::is_none(result);
-        ensures [abstract] spec_contains_key(self, key);
-        ensures [abstract] spec_get(self, key) == value;
-        ensures [abstract] spec_contains_key(old(self), key) ==> ((option::is_some(result)) && (option::spec_borrow(result) == spec_get(old(
+        ensures !spec_contains_key(old(self), key) ==> option::is_none(result);
+        ensures spec_contains_key(self, key);
+        ensures spec_get(self, key) == value;
+        ensures spec_contains_key(old(self), key) ==> ((option::is_some(result)) && (option::spec_borrow(result) == spec_get(old(
             self), key)));
-        ensures [abstract] !spec_contains_key(old(self), key) ==> spec_len(old(self)) + 1 == spec_len(self);
-        ensures [abstract] spec_contains_key(old(self), key) ==> spec_len(old(self)) == spec_len(self);
-        ensures [abstract] forall k: K: spec_contains_key(old(self), k) && k != key ==> spec_get(old(self), k) == spec_get(self, k);
-        ensures [abstract] forall k: K: spec_contains_key(old(self), k) ==> spec_contains_key(self, k);
-        ensures [abstract] forall k: K: spec_contains_key(self, k) ==> (k == key || spec_contains_key(old(self), k));
+        ensures !spec_contains_key(old(self), key) ==> spec_len(old(self)) + 1 == spec_len(self);
+        ensures spec_contains_key(old(self), key) ==> spec_len(old(self)) == spec_len(self);
+        ensures spec_unchanged_except_at(self, old(self), key);
     }
 
     spec add_all {
@@ -166,38 +239,70 @@ spec aptos_framework::big_ordered_map {
     spec borrow_front<K: drop + copy + store, V: store>(self: &BigOrderedMap<K, V>): (K, &V) {
         pragma opaque;
         pragma verify = false;
-        ensures [abstract] spec_contains_key(self, result_1);
-        ensures [abstract] spec_get(self, result_1) == result_2;
-        ensures [abstract] forall k: K where k != result_1: spec_contains_key(self, k) ==>
+        ensures spec_contains_key(self, result_1);
+        ensures spec_get(self, result_1) == result_2;
+        ensures forall k: K where k != result_1: spec_contains_key(self, k) ==>
         std::cmp::compare(result_1, k) == std::cmp::Ordering::Less;
     }
 
+    spec front_key<K: drop + copy + store, V: store>(self: &BigOrderedMap<K, V>): K {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if spec_len(self) == 0;
+        ensures spec_contains_key(self, result);
+        ensures forall k: K where k != result: spec_contains_key(self, k) ==>
+            std::cmp::compare(result, k) == std::cmp::Ordering::Less;
+    }
+
     spec borrow_back {
         pragma opaque;
         pragma verify = false;
-        ensures [abstract] spec_contains_key(self, result_1);
-        ensures [abstract] spec_get(self, result_1) == result_2;
-        ensures [abstract] forall k: K where k != result_1: spec_contains_key(self, k) ==>
+        ensures spec_contains_key(self, result_1);
+        ensures spec_get(self, result_1) == result_2;
+        ensures forall k: K where k != result_1: spec_contains_key(self, k) ==>
         std::cmp::compare(result_1, k) == std::cmp::Ordering::Greater;
     }
 
+    spec back_key<K: drop + copy + store, V: store>(self: &BigOrderedMap<K, V>): K {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if spec_len(self) == 0;
+        ensures spec_contains_key(self, result);
+        ensures forall k: K where k != result: spec_contains_key(self, k) ==>
+            std::cmp::compare(result, k) == std::cmp::Ordering::Greater;
+    }
+
     spec pop_front<K: drop + copy + store, V: store>(self: &mut BigOrderedMap<K, V>): (K, V) {
         pragma opaque;
         pragma verify = false;
+        ensures spec_contains_key(old(self), result_1);
+        ensures result_2 == spec_get(old(self), result_1);
+        ensures !spec_contains_key(self, result_1);
+        ensures spec_len(self) == spec_len(old(self)) - 1;
+        ensures spec_unchanged_except_at(self, old(self), result_1);
+        ensures forall k: K where spec_contains_key(old(self), k) && k != result_1:
+            std::cmp::compare(result_1, k) == std::cmp::Ordering::Less;
     }
 
-    spec pop_back {
+    spec pop_back<K: drop + copy + store, V: store>(self: &mut BigOrderedMap<K, V>): (K, V) {
         pragma opaque;
         pragma verify = false;
+        ensures spec_contains_key(old(self), result_1);
+        ensures result_2 == spec_get(old(self), result_1);
+        ensures !spec_contains_key(self, result_1);
+        ensures spec_len(self) == spec_len(old(self)) - 1;
+        ensures spec_unchanged_except_at(self, old(self), result_1);
+        ensures forall k: K where spec_contains_key(old(self), k) && k != result_1:
+            std::cmp::compare(result_1, k) == std::cmp::Ordering::Greater;
     }
 
     spec prev_key<K: drop + copy + store, V: store>(self: &BigOrderedMap<K, V>, key: &K): Option<K> {
         pragma opaque;
         pragma verify = false;
-        ensures [abstract] result == std::option::spec_none() <==>
+        ensures result == std::option::spec_none() <==>
         (forall k: K {spec_contains_key(self, k)} where spec_contains_key(self, k)
         && k != key: std::cmp::compare(key, k) == std::cmp::Ordering::Less);
-        ensures [abstract] result.is_some() <==>
+        ensures result.is_some() <==>
             spec_contains_key(self, option::spec_borrow(result)) &&
             (std::cmp::compare(option::spec_borrow(result), key) == std::cmp::Ordering::Less)
             && (forall k: K {spec_contains_key(self, k), std::cmp::compare(option::spec_borrow(result), k), std::cmp::compare(key, k)} where k != option::spec_borrow(result): ((spec_contains_key(self, k) &&
@@ -209,10 +314,10 @@ spec aptos_framework::big_ordered_map {
     spec next_key<K: drop + copy + store, V: store>(self: &BigOrderedMap<K, V>, key: &K): Option<K>  {
         pragma opaque;
         pragma verify = false;
-        ensures [abstract] result == std::option::spec_none() <==>
+        ensures result == std::option::spec_none() <==>
         (forall k: K {spec_contains_key(self, k)} where spec_contains_key(self, k) && k != key:
         std::cmp::compare(key, k) == std::cmp::Ordering::Greater);
-        ensures [abstract] result.is_some() <==>
+        ensures result.is_some() <==>
             spec_contains_key(self, option::spec_borrow(result)) &&
             (std::cmp::compare(option::spec_borrow(result), key) == std::cmp::Ordering::Greater)
             && (forall k: K {spec_contains_key(self, k)} where k != option::spec_borrow(result): ((spec_contains_key(self, k) &&
@@ -224,36 +329,106 @@ spec aptos_framework::big_ordered_map {
     spec internal_find {
         pragma opaque;
         pragma verify = false;
+        aborts_if false;
+        ensures iter_is_end(result, self) <==> !spec_contains_key(self, key);
+        ensures !iter_is_end(result, self) ==> result.key == key;
     }
 
     spec internal_new_begin_iter {
         pragma opaque;
         pragma verify = false;
+        aborts_if false;
+        ensures iter_is_end(result, self) <==> spec_len(self) == 0;
+        ensures !iter_is_end(result, self) ==> spec_contains_key(self, result.key);
+        // result.key is the smallest key in the map.
+        ensures !iter_is_end(result, self) ==>
+            (forall k: K where spec_contains_key(self, k) && k != result.key:
+                std::cmp::compare(result.key, k) == std::cmp::Ordering::Less);
     }
 
     spec internal_new_end_iter {
         pragma opaque;
         pragma verify = false;
+        aborts_if false;
+        ensures result is IteratorPtr::End<K>;
     }
 
     spec iter_next {
         pragma opaque;
         pragma verify = false;
+        aborts_if iter_is_end(self, map);
     }
 
     spec iter_prev {
         pragma opaque;
         pragma verify = false;
+        aborts_if iter_is_begin(self, map);
     }
 
     spec compute_length {
         pragma verify = false;
         pragma opaque;
-        ensures [abstract] result == spec_len(self);
+        ensures result == spec_len(self);
     }
 
     spec iter_modify {
         pragma opaque;
         pragma verify = false;
+        aborts_if iter_is_end(self, map);
+        // iter_modify mutates the value at self.key via the closure. Containment is
+        // unchanged for every key; values for keys other than self.key are preserved.
+        ensures spec_contains_key(map, self.key);
+        ensures spec_len(map) == spec_len(old(map));
+        ensures spec_unchanged_except_at(map, old(map), self.key);
+    }
+
+    spec internal_find_with_path {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if false;
+        ensures iter_is_end(result.iterator, self) <==> !spec_contains_key(self, key);
+        ensures !iter_is_end(result.iterator, self) ==> result.iterator.key == key;
+    }
+
+    spec iter_with_path_get_iter {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if false;
+        ensures result == self.iterator;
+    }
+
+    spec iter_remove {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if iter_is_end(self.iterator, map);
+        ensures result == spec_get(old(map), self.iterator.key);
+        ensures !spec_contains_key(map, self.iterator.key);
+        ensures spec_len(map) == spec_len(old(map)) - 1;
+        ensures spec_unchanged_except_at(map, old(map), self.iterator.key);
+    }
+
+    spec internal_leaf_new_begin_iter {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if false;
+    }
+
+    spec internal_leaf_iter_is_end {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if false;
+    }
+
+    spec internal_leaf_borrow_value {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if false;
+        ensures result == self.value;
+    }
+
+    spec internal_leaf_iter_borrow_entries_and_next_leaf_index {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if internal_leaf_iter_is_end(self);
     }
 }
diff --git a/aptos-move/framework/aptos-framework/sources/transaction_context.spec.move b/aptos-move/framework/aptos-framework/sources/transaction_context.spec.move
index 79869d5d7e7..326184e191d 100644
--- a/aptos-move/framework/aptos-framework/sources/transaction_context.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/transaction_context.spec.move
@@ -116,10 +116,18 @@ spec aptos_framework::transaction_context {
     spec monotonically_increasing_counter_internal(timestamp_us: u64): u128 {
         //TODO: temporary mockup
         pragma opaque;
+        aborts_if [abstract] false;
     }
 
     spec monotonically_increasing_counter_internal_for_test_only(): u128 {
         //TODO: temporary mockup
         pragma opaque;
+        aborts_if [abstract] false;
+    }
+
+    spec monotonically_increasing_counter(): u128 {
+        pragma opaque;
+        // Assume that the monotonically increasing counter is always increasing.
+        aborts_if [abstract] false;
     }
 }
diff --git a/aptos-move/framework/aptos-stdlib/sources/math64.move b/aptos-move/framework/aptos-stdlib/sources/math64.move
index 9b89acbe809..3043ea35e1e 100644
--- a/aptos-move/framework/aptos-stdlib/sources/math64.move
+++ b/aptos-move/framework/aptos-stdlib/sources/math64.move
@@ -87,6 +87,9 @@ module aptos_std::math64 {
                 res += n;
             };
             n >>= 1;
+        } spec {
+            invariant (res as u64) + 2 * (n as u64) <= 64;
+            invariant n == 0 ==> (res as u64) <= 63;
         };
         res
     }
diff --git a/aptos-move/framework/aptos-stdlib/sources/math_fixed.spec.move b/aptos-move/framework/aptos-stdlib/sources/math_fixed.spec.move
index 1442eb30553..bff9f0dbf9e 100644
--- a/aptos-move/framework/aptos-stdlib/sources/math_fixed.spec.move
+++ b/aptos-move/framework/aptos-stdlib/sources/math_fixed.spec.move
@@ -4,6 +4,8 @@ spec aptos_std::math_fixed {
     /// No loop in the body, so callers can inline without havocing.
     spec sqrt(x: FixedPoint32): FixedPoint32 {
         aborts_if false;
+        // Zero input → zero output, directly from math128::sqrt's ensures.
+        ensures x.get_raw_value() == 0 ==> result.get_raw_value() == 0;
     }
 
     /// `mul_div` aborts when z is zero or when x * y / z overflows u64.
diff --git a/aptos-move/framework/cached-packages/src/head.mrb b/aptos-move/framework/cached-packages/src/head.mrb
index c93fc27c245..c767e605a65 100644
Binary files a/aptos-move/framework/cached-packages/src/head.mrb and b/aptos-move/framework/cached-packages/src/head.mrb differ
diff --git a/aptos-move/framework/move-stdlib/sources/string.spec.move b/aptos-move/framework/move-stdlib/sources/string.spec.move
index 140b8e728fc..78f688043bf 100644
--- a/aptos-move/framework/move-stdlib/sources/string.spec.move
+++ b/aptos-move/framework/move-stdlib/sources/string.spec.move
@@ -24,6 +24,12 @@ spec std::string {
         String{bytes}
     }
 
+    spec utf8(bytes: vector<u8>): String {
+        pragma opaque;
+        aborts_if !spec_internal_check_utf8(bytes);
+        ensures result == spec_utf8(bytes);
+    }
+
     spec module {
         fun spec_internal_check_utf8(v: vector<u8>): bool;
         fun spec_internal_is_char_boundary(v: vector<u8>, i: u64): bool;
diff --git a/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl b/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl
index 5cbf7569f91..693799fe5ef 100644
--- a/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl
+++ b/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl
@@ -226,6 +226,43 @@ procedure {:inline 1} $1_vector_insert{{S}}(m: $Mutation (Vec ({{T}})), i: int,
     }
 }
 
+// `vector::move_range(from, removal_position, length, to, insert_position)` extracts the
+// half-open range `[removal_position, removal_position+length)` from `from` and splices it
+// into `to` at `insert_position`, shifting `to[insert_position..]` to the right. Move enforces
+// that `from` and `to` are distinct (no aliasing of mutable references).
+procedure {:inline 1} $1_vector_move_range{{S}}(
+    from: $Mutation (Vec ({{T}})),
+    removal_position: int,
+    length: int,
+    to: $Mutation (Vec ({{T}})),
+    insert_position: int
+) returns (from': $Mutation (Vec ({{T}})), to': $Mutation (Vec ({{T}})))
+{
+    var from_v: Vec ({{T}});
+    var to_v: Vec ({{T}});
+    var middle: Vec ({{T}});
+    from_v := $Dereference(from);
+    to_v := $Dereference(to);
+    // The `< 0` checks are defensive — Move's u64 arguments are non-negative by typing,
+    // but Boogie ints can be arbitrary so we guard explicitly. Matches the convention
+    // used in `$1_vector_insert` above.
+    if (removal_position < 0
+        || length < 0
+        || removal_position + length > LenVec(from_v)
+        || insert_position < 0
+        || insert_position > LenVec(to_v)) {
+        call $ExecFailureAbort();
+        return;
+    }
+    middle := SliceVec(from_v, removal_position, removal_position + length);
+    from' := $UpdateMutation(from,
+        ConcatVec(SliceVec(from_v, 0, removal_position),
+                  SliceVec(from_v, removal_position + length, LenVec(from_v))));
+    to' := $UpdateMutation(to,
+        ConcatVec(SliceVec(to_v, 0, insert_position),
+                  ConcatVec(middle, SliceVec(to_v, insert_position, LenVec(to_v)))));
+}
+
 procedure {:inline 1} $1_vector_length{{S}}(v: Vec ({{T}})) returns (l: int) {
     l := LenVec(v);
 }