diff --git a/deque/deque.mbt b/deque/deque.mbt
index af931d3e6..f4afdae19 100644
--- a/deque/deque.mbt
+++ b/deque/deque.mbt
@@ -24,7 +24,7 @@ fn[A] new_deque(capacity : Int) -> Deque[A] {
 /// Computes the tail index (index of last element) on demand.
 /// Only valid when len > 0.
 fn[A] Deque::tail_index(self : Deque[A]) -> Int {
-  (self.head + self.len - 1) % self.buf.length()
+  deque_tail_index(self.head, self.len, self.buf.length())
 }
 
 ///|
@@ -576,7 +576,9 @@ pub fn[A] Deque::capacity(self : Deque[A]) -> Int {
 /// Reallocate the deque with a new capacity.
 fn[A] Deque::realloc(self : Deque[A]) -> Unit {
   let old_cap = self.buf.length()
-  let new_cap = if old_cap == 0 { 8 } else { old_cap * 2 }
+  // Doubling a larger capacity would overflow `Int`.
+  guard old_cap <= 0x3fff_ffff else { abort("Deque capacity overflow") }
+  let new_cap = deque_realloc_capacity(old_cap, self.len)
   let new_buf = self.unsafe_make_and_blit_to(new_cap, 0)
   self.head = 0
   self.buf = new_buf
@@ -596,7 +598,8 @@ pub fn[A] Deque::front(self : Deque[A]) -> A? {
   if self.len == 0 {
     None
   } else {
-    Some(self.buf[self.head])
+    let index = deque_element_index(self.head, self.len, self.buf.length(), 0)
+    Some(self.buf.unsafe_get(index))
   }
 }
 
@@ -614,7 +617,13 @@ pub fn[A] Deque::back(self : Deque[A]) -> A? {
   if self.len == 0 {
     None
   } else {
-    Some(self.buf[self.tail_index()])
+    let index = deque_element_index(
+      self.head,
+      self.len,
+      self.buf.length(),
+      self.len - 1,
+    )
+    Some(self.buf.unsafe_get(index))
   }
 }
 
@@ -635,9 +644,9 @@ pub fn[A] Deque::push_front(self : Deque[A], value : A) -> Unit {
   if self.len == self.buf.length() {
     self.realloc()
   }
-  let cap = self.buf.length()
-  self.head = (self.head - 1 + cap) % cap
-  self.buf[self.head] = value
+  let new_head = deque_push_front_core(self.head, self.len, self.buf.length())
+  self.buf.unsafe_set(new_head, value)
+  self.head = new_head
   self.len += 1
 }
 
@@ -658,9 +667,8 @@ pub fn[A] Deque::push_back(self : Deque[A], value : A) -> Unit {
   if self.len == self.buf.length() {
     self.realloc()
   }
-  let cap = self.buf.length()
-  let write_idx = (self.head + self.len) % cap
-  self.buf[write_idx] = value
+  let write_idx = deque_push_back_core(self.head, self.len, self.buf.length())
+  self.buf.unsafe_set(write_idx, value)
   self.len += 1
 }
 
@@ -680,9 +688,9 @@ pub fn[A] Deque::push_back(self : Deque[A], value : A) -> Unit {
 #alias(pop_front_exn, deprecated)
 pub fn[A] Deque::unsafe_pop_front(self : Deque[A]) -> Unit {
   guard self.len > 0 else { abort("The deque is empty!") }
+  let new_head = deque_pop_front_core(self.head, self.len, self.buf.length())
   set_null(self.buf, self.head)
-  let cap = self.buf.length()
-  self.head = (self.head + 1) % cap
+  self.head = new_head
   self.len -= 1
 }
 
@@ -733,7 +741,7 @@ test "unsafe_pop_front after many push_front" {
 #alias(pop_back_exn, deprecated)
 pub fn[A] Deque::unsafe_pop_back(self : Deque[A]) -> Unit {
   guard self.len > 0 else { abort("The deque is empty!") }
-  let tail_idx = self.tail_index()
+  let tail_idx = deque_pop_back_core(self.head, self.len, self.buf.length())
   set_null(self.buf, tail_idx)
   self.len -= 1
 }
@@ -771,10 +779,10 @@ pub fn[A] Deque::unsafe_pop_back(self : Deque[A]) -> Unit {
 /// ```
 pub fn[A] Deque::pop_front(self : Deque[A]) -> A? {
   guard self.len > 0 else { return None }
-  let value = self.buf[self.head]
+  let new_head = deque_pop_front_core(self.head, self.len, self.buf.length())
+  let value = self.buf.unsafe_get(self.head)
   set_null(self.buf, self.head)
-  let cap = self.buf.length()
-  self.head = (self.head + 1) % cap
+  self.head = new_head
   self.len -= 1
   Some(value)
 }
@@ -791,8 +799,8 @@ pub fn[A] Deque::pop_front(self : Deque[A]) -> A? {
 /// ```
 pub fn[A] Deque::pop_back(self : Deque[A]) -> A? {
   guard self.len > 0 else { return None }
-  let tail_idx = self.tail_index()
-  let value = self.buf[tail_idx]
+  let tail_idx = deque_pop_back_core(self.head, self.len, self.buf.length())
+  let value = self.buf.unsafe_get(tail_idx)
   set_null(self.buf, tail_idx)
   self.len -= 1
   Some(value)
@@ -815,11 +823,13 @@ pub fn[A] Deque::at(self : Deque[A], index : Int) -> A {
   if index < 0 || index >= self.len {
     index_out_of_bounds(self.len, index)
   }
-  if self.head + index < self.buf.length() {
-    self.buf[self.head + index]
-  } else {
-    self.buf[self.head + index - self.buf.length()]
-  }
+  let physical_index = deque_element_index(
+    self.head,
+    self.len,
+    self.buf.length(),
+    index,
+  )
+  self.buf.unsafe_get(physical_index)
 }
 
 ///|
@@ -840,11 +850,13 @@ pub fn[A] Deque::set(self : Deque[A], index : Int, value : A) -> Unit {
   if index < 0 || index >= self.len {
     index_out_of_bounds(self.len, index)
   }
-  if self.head + index < self.buf.length() {
-    self.buf[self.head + index] = value
-  } else {
-    self.buf[self.head + index - self.buf.length()] = value
-  }
+  let physical_index = deque_element_index(
+    self.head,
+    self.len,
+    self.buf.length(),
+    index,
+  )
+  self.buf.unsafe_set(physical_index, value)
 }
 
 ///|
@@ -2312,8 +2324,13 @@ pub fn[A] Deque::binary_search_by(
 /// Safe element access with bounds checking
 pub fn[A] Deque::get(self : Deque[A], index : Int) -> A? {
   if index >= 0 && index < self.len {
-    let physical_index = (self.head + index) % self.buf.length()
-    Some(self.buf[physical_index])
+    let physical_index = deque_element_index(
+      self.head,
+      self.len,
+      self.buf.length(),
+      index,
+    )
+    Some(self.buf.unsafe_get(physical_index))
   } else {
     None
   }
diff --git a/deque/deque_test.mbt b/deque/deque_test.mbt
index 59fb7ce2d..8d9e9b3e1 100644
--- a/deque/deque_test.mbt
+++ b/deque/deque_test.mbt
@@ -2798,3 +2798,40 @@ test "Deque::append/self_alias" {
   dq.append(dq)
   debug_inspect(dq.to_array(), content="[1, 2, 3, 1, 2, 3]")
 }
+
+///|
+test "deque operations match array model across wrap boundaries" {
+  for initial_capacity in [0, 1, 3, 5, 15] {
+    let deque = @deque.Deque([], capacity=initial_capacity)
+    let model : Array[Int] = []
+    for step in 0..<1300 {
+      let cycle = step / 13
+      match step % 13 {
+        0 | 1 | 4 => {
+          deque.push_back(step)
+          model.push(step)
+        }
+        2 | 5 => {
+          deque.push_front(step)
+          model.insert(0, step)
+        }
+        3 => {
+          let index = (cycle + initial_capacity) % (model.length() + 1)
+          deque.insert(index, step)
+          model.insert(index, step)
+        }
+        6 | 10 => @test.assert_eq(deque.pop_front(), Some(model.remove(0)))
+        7 | 12 => @test.assert_eq(deque.pop_back(), model.pop())
+        8 | 11 => {
+          let index = (cycle + initial_capacity) % model.length()
+          @test.assert_eq(deque.remove(index), model.remove(index))
+        }
+        _ => {
+          deque.rev_in_place()
+          model.rev_in_place()
+        }
+      }
+      @test.assert_eq(deque.to_array(), model)
+    }
+  }
+}
diff --git a/deque/index_ops.mbt b/deque/index_ops.mbt
new file mode 100644
index 000000000..fba2b22ab
--- /dev/null
+++ b/deque/index_ops.mbt
@@ -0,0 +1,222 @@
+// Copyright 2026 International Digital Economy Academy
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+///|
+/// The deque representation invariant guarantees these indices are in bounds.
+/// Keep these private so callers cannot bypass bounds checks.
+#inline
+fn[T] UninitializedArray::unsafe_get(
+  self : UninitializedArray[T],
+  index : Int,
+) -> T = "%fixedarray.unsafe_get"
+
+///|
+#inline
+fn[T] UninitializedArray::unsafe_set(
+  self : UninitializedArray[T],
+  index : Int,
+  value : T,
+) -> Unit = "%fixedarray.unsafe_set"
+
+///|
+/// Converts a zero-based logical offset from `head` to a physical buffer index.
+/// If the offset fits before the buffer end, `head + offset` is known to be less
+/// than `capacity`. Otherwise the wrapped branch subtracts the remaining space
+/// from `offset` and never evaluates that addition.
+#inline
+fn wrap_index(
+  head : Int,
+  offset : Int,
+  capacity : Int,
+) -> Int where {
+  proof_require: index_in_bounds(head, capacity),
+  proof_require: index_in_bounds(offset, capacity),
+  proof_ensure: result => {
+    circular_index_at_offset(head, offset, capacity, result)
+  },
+} {
+  let contiguous = capacity - head
+  if offset < contiguous {
+    head + offset
+  } else {
+    offset - contiguous
+  }
+}
+
+///|
+/// Moves an in-buffer index forward by one without division.
+#inline
+fn increment_index(
+  index : Int,
+  capacity : Int,
+) -> Int where {
+  proof_require: index_in_bounds(index, capacity),
+  proof_ensure: result => circular_successor(index, capacity, result),
+} {
+  if index == capacity - 1 {
+    0
+  } else {
+    index + 1
+  }
+}
+
+///|
+/// Moves an in-buffer index back by one without division.
+#inline
+fn decrement_index(
+  index : Int,
+  capacity : Int,
+) -> Int where {
+  proof_require: index_in_bounds(index, capacity),
+  proof_ensure: result => circular_predecessor(index, capacity, result),
+} {
+  if index == 0 {
+    capacity - 1
+  } else {
+    index - 1
+  }
+}
+
+///|
+/// Computes the capacity used by `realloc` after its runtime overflow check.
+/// The contract proves the layout invariant restored after a successful growth.
+#warnings("-unused_value")
+#inline
+fn deque_realloc_capacity(
+  capacity : Int,
+  len : Int,
+) -> Int where {
+  proof_require: len >= 0,
+  proof_require: len <= capacity,
+  proof_require: capacity <= 0x3fff_ffff,
+  proof_ensure: result => result > capacity,
+  proof_ensure: result => result <= 0x7fff_ffff,
+  proof_ensure: result => len < result,
+  proof_ensure: result => deque_layout_inv(result, 0, len),
+} {
+  if capacity == 0 {
+    8
+  } else {
+    capacity * 2
+  }
+}
+
+///|
+#inline
+fn deque_tail_index(
+  head : Int,
+  len : Int,
+  capacity : Int,
+) -> Int where {
+  proof_require: deque_layout_inv(capacity, head, len),
+  proof_require: len > 0,
+  proof_ensure: result => {
+    circular_index_at_offset(head, len - 1, capacity, result)
+  },
+  proof_ensure: result => index_in_bounds(result, capacity),
+} {
+  wrap_index(head, len - 1, capacity)
+}
+
+///|
+#warnings("-unused_value")
+#inline
+fn deque_element_index(
+  head : Int,
+  len : Int,
+  capacity : Int,
+  index : Int,
+) -> Int where {
+  proof_require: deque_layout_inv(capacity, head, len),
+  proof_require: index >= 0,
+  proof_require: index < len,
+  proof_ensure: result => {
+    circular_index_at_offset(head, index, capacity, result)
+  },
+  proof_ensure: result => index_in_bounds(result, capacity),
+} {
+  wrap_index(head, index, capacity)
+}
+
+///|
+#inline
+fn deque_push_back_core(
+  head : Int,
+  len : Int,
+  capacity : Int,
+) -> Int where {
+  proof_require: deque_layout_inv(capacity, head, len),
+  proof_require: len < capacity,
+  proof_ensure: result => circular_index_at_offset(head, len, capacity, result),
+  proof_ensure: result => {
+    index_in_bounds(result, capacity) &&
+    deque_layout_inv(capacity, head, len + 1)
+  },
+} {
+  wrap_index(head, len, capacity)
+}
+
+///|
+#warnings("-unused_value")
+#inline
+fn deque_push_front_core(
+  head : Int,
+  len : Int,
+  capacity : Int,
+) -> Int where {
+  proof_require: deque_layout_inv(capacity, head, len),
+  proof_require: len < capacity,
+  proof_ensure: result => circular_predecessor(head, capacity, result),
+  proof_ensure: result => index_in_bounds(result, capacity),
+  proof_ensure: result => deque_layout_inv(capacity, result, len + 1),
+} {
+  decrement_index(head, capacity)
+}
+
+///|
+#warnings("-unused_value")
+#inline
+fn deque_pop_front_core(
+  head : Int,
+  len : Int,
+  capacity : Int,
+) -> Int where {
+  proof_require: deque_layout_inv(capacity, head, len),
+  proof_require: len > 0,
+  proof_ensure: result => circular_successor(head, capacity, result),
+  proof_ensure: result => index_in_bounds(result, capacity),
+  proof_ensure: result => deque_layout_inv(capacity, result, len - 1),
+} {
+  increment_index(head, capacity)
+}
+
+///|
+#inline
+fn deque_pop_back_core(
+  head : Int,
+  len : Int,
+  capacity : Int,
+) -> Int where {
+  proof_require: deque_layout_inv(capacity, head, len),
+  proof_require: len > 0,
+  proof_ensure: result => {
+    circular_index_at_offset(head, len - 1, capacity, result)
+  },
+  proof_ensure: result => {
+    index_in_bounds(result, capacity) &&
+    deque_layout_inv(capacity, head, len - 1)
+  },
+} {
+  wrap_index(head, len - 1, capacity)
+}
diff --git a/deque/index_ops.mbtp b/deque/index_ops.mbtp
new file mode 100644
index 000000000..1c78b1c72
--- /dev/null
+++ b/deque/index_ops.mbtp
@@ -0,0 +1,121 @@
+// Copyright 2026 International Digital Economy Academy
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+///|
+/// An index in the half-open range `[0, capacity)`.
+predicate index_in_bounds(index : Int, capacity : Int) {
+  index >= 0 && index < capacity
+}
+
+///|
+/// `physical_index` is `offset` slots after `start` in a circular buffer. Since
+/// a valid offset is smaller than the capacity, at most one wrap is needed.
+predicate circular_index_at_offset(
+  start : Int,
+  offset : Int,
+  capacity : Int,
+  physical_index : Int,
+) {
+  if offset < capacity - start {
+    physical_index == start + offset
+  } else {
+    physical_index == offset - (capacity - start)
+  }
+}
+
+///|
+/// The branch calculation above is in bounds and equivalent to wrapping with
+/// remainder for every valid start and offset.
+lemma circular_index_at_offset_correct(
+  start : Int,
+  offset : Int,
+  capacity : Int,
+  physical_index : Int,
+) where {
+  proof_require: index_in_bounds(start, capacity),
+  proof_require: index_in_bounds(offset, capacity),
+  proof_require: circular_index_at_offset(
+    start,
+    offset,
+    capacity,
+    physical_index,
+  ),
+  proof_ensure: index_in_bounds(physical_index, capacity),
+  proof_ensure: physical_index == (start + offset) % capacity,
+} {
+}
+
+///|
+/// `successor` is the physical index immediately after `index`, wrapping from
+/// the last buffer slot to zero.
+predicate circular_successor(
+  index : Int,
+  capacity : Int,
+  successor : Int,
+) {
+  if index == capacity - 1 { successor == 0 } else { successor == index + 1 }
+}
+
+///|
+/// The branch calculation above is in bounds and equivalent to adding one
+/// modulo the capacity.
+lemma circular_successor_correct(
+  index : Int,
+  capacity : Int,
+  successor : Int,
+) where {
+  proof_require: index_in_bounds(index, capacity),
+  proof_require: circular_successor(index, capacity, successor),
+  proof_ensure: index_in_bounds(successor, capacity),
+  proof_ensure: successor == (index + 1) % capacity,
+} {
+}
+
+///|
+/// `predecessor` is the physical index immediately before `index`.
+predicate circular_predecessor(
+  index : Int,
+  capacity : Int,
+  predecessor : Int,
+) {
+  if index == 0 {
+    predecessor == capacity - 1
+  } else {
+    predecessor == index - 1
+  }
+}
+
+///|
+/// The branch calculation above is in bounds and equivalent to subtracting one
+/// modulo the capacity.
+lemma circular_predecessor_correct(
+  index : Int,
+  capacity : Int,
+  predecessor : Int,
+) where {
+  proof_require: index_in_bounds(index, capacity),
+  proof_require: circular_predecessor(index, capacity, predecessor),
+  proof_ensure: index_in_bounds(predecessor, capacity),
+  proof_ensure: predecessor == (index + capacity - 1) % capacity,
+} {
+}
+
+///|
+/// The arithmetic part of the private `Deque` representation invariant.
+predicate deque_layout_inv(capacity : Int, head : Int, len : Int) {
+  (capacity == 0 && head == 0 && len == 0) ||
+  (index_in_bounds(head, capacity) &&
+    len >= 0 &&
+    len <= capacity)
+}
diff --git a/deque/types.mbt b/deque/types.mbt
index 22e9cff94..35b2bb3ab 100644
--- a/deque/types.mbt
+++ b/deque/types.mbt
@@ -16,7 +16,7 @@
 /// A double-ended queue (deque) backed by a growable circular buffer.
 ///
 /// This implementation follows the Rust `VecDeque` design: only `head` and `len`
-/// are stored, with `tail` computed on demand as `(head + len - 1) % cap`.
+/// are stored, with `tail` computed on demand by wrapping `head + len - 1`.
 ///
 /// Layout:
 /// ```text
@@ -24,14 +24,14 @@
 ///   buf: [4, 5, _, _, _, 1, 2, 3]
 ///              ^        ^
 ///        (tail)       head
-///   head = 5, len = 5, tail = (5 + 5 - 1) % 8 = 1
+///   head = 5, len = 5, tail = wrap(5 + 5 - 1, 8) = 1
 ///   Logical order: [1, 2, 3, 4, 5]
 ///
 /// Contiguous case (head + len <= cap):
 ///   buf: [_, 1, 2, 3, 4, 5, _, _]
 ///           ^           ^
 ///         head       (tail)
-///   head = 1, len = 5, tail = (1 + 5 - 1) % 8 = 5
+///   head = 1, len = 5, tail = wrap(1 + 5 - 1, 8) = 5
 ///   Logical order: [1, 2, 3, 4, 5]
 ///
 /// Empty case (len == 0):
@@ -42,15 +42,16 @@
 ///
 /// Invariants:
 /// - `0 <= len <= buf.length()`
-/// - `0 <= head < buf.length()`
-/// - Element at index `i` is at `buf[(head + i) % buf.length()]`
-/// - When `len > 0`: front is `buf[head]`, back is `buf[(head + len - 1) % cap]`
-/// - When `len == 0`: no valid element, `head` can be any valid index
+/// - When `buf.length() == 0`: `len == 0` and `head == 0`
+/// - When `buf.length() > 0`: `0 <= head < buf.length()`
+/// - Element at index `i` is at `buf[wrap(head + i, buf.length())]`
+/// - When `len > 0`: front is `buf[head]`, back is at wrapped `head + len - 1`
+/// - When `len == 0` and the buffer is non-empty, `head` may be any valid index
 struct Deque[A] {
   /// Circular buffer storing elements. May contain uninitialized slots.
   mut buf : UninitializedArray[A]
   /// Number of elements currently in the deque.
   mut len : Int
-  /// Index of the first element (front). Valid range: 0 <= head < buf.length().
+  /// Index of the first element (front), or 0 for an empty zero-capacity deque.
   mut head : Int
 }