diff --git a/abstract_syntax/rewrite.py b/abstract_syntax/rewrite.py
index 3b905ad0..b6e1aa71 100644
--- a/abstract_syntax/rewrite.py
+++ b/abstract_syntax/rewrite.py
@@ -104,6 +104,8 @@ def count_marks(formula: AST) -> int:
       return sum([count_marks(elt) for elt in elements])
     case MakeArray(_, _, subject):
       return count_marks(subject)
+    case ArrayLength(_, _, subject):
+      return count_marks(subject)
     case _:
       internal_error(formula.location, 'in count_marks function, unhandled ' + str(formula))
 
@@ -165,6 +167,8 @@ def find_mark(formula: AST) -> None:
           find_mark(elt)
     case MakeArray(_, _, subject):
       find_mark(subject)
+    case ArrayLength(_, _, subject):
+      find_mark(subject)
     case _:
       internal_error(formula.location, 'in find_mark function, unhandled ' + str(formula))
 
@@ -238,6 +242,8 @@ def replace_mark(formula: Term | SwitchCase, replacement: Term) -> Term | Switch
                    [replace_mark(elt, replacement) for elt in elements])
     case MakeArray(loc2, tyof, subject):
       return MakeArray(loc2, tyof, replace_mark(subject, replacement))
+    case ArrayLength(loc2, tyof, subject):
+      return ArrayLength(loc2, tyof, replace_mark(subject, replacement))
     case _:
       internal_error(formula.location, 'in replace_mark function, unhandled ' + str(formula))
 
@@ -436,7 +442,11 @@ def rewrite_aux(loc: Meta, formula: Term | SwitchCase, equation: Formula | AutoR
     case MakeArray(loc2, tyof, subject):
       return MakeArray(loc, tyof,
                        rewrite_aux(loc, subject, equation, env, depth - 1))
-  
+
+    case ArrayLength(loc2, tyof, subject):
+      return ArrayLength(loc, tyof,
+                         rewrite_aux(loc, subject, equation, env, depth - 1))
+
     case TLet(loc2, tyof, var, rhs, body):
       return TLet(loc2, tyof, var, rewrite_aux(loc, rhs, equation, env, depth - 1),
                   rewrite_aux(loc, body, equation, env, depth - 1))
diff --git a/abstract_syntax/terms.py b/abstract_syntax/terms.py
index 8ffdd325..7325178b 100644
--- a/abstract_syntax/terms.py
+++ b/abstract_syntax/terms.py
@@ -1665,6 +1665,24 @@ def reduce(self, env: Env) -> Term:
                 return new_get.reduce(env)
     return ArrayGet(self.location, self.typeof, subject_red, position_red)
 
+@dataclass
+class ArrayLength(Term):
+  # `length(a)` for a mutable-array handle (or a pure array). Produced only
+  # by the type checker when `length` is applied to an array-typed argument
+  # (issue #1117, Phase 2h); it is never parsed, so both parsers still see
+  # the surface `length(a)` as an ordinary `Call`. In Phase 2 an array's
+  # length is immutable for the lifetime of the handle, so this node has no
+  # runtime reduction -- the default `_map_children` walk only reduces the
+  # `subject`, leaving `length(a)` symbolic for use inside specifications and
+  # array-bounds obligations.
+  subject: Term
+
+  def __eq__(self, other: object) -> bool:
+    return eq_fields(self, other, 'subject')
+
+  def __str__(self) -> str:
+    return 'length(' + str(self.subject) + ')'
+
 @dataclass
 class TLet(Term):
   var: str
diff --git a/checker_types.py b/checker_types.py
index 6c3208e6..cde4b7b8 100644
--- a/checker_types.py
+++ b/checker_types.py
@@ -24,6 +24,7 @@
     And,
     Array,
     ArrayGet,
+    ArrayLength,
     ArrayType,
     Bool,
     BoolType,
@@ -114,6 +115,51 @@ def _var_ref_base_name(term: Term) -> str | None:
     return cast(str, term.get_name()).split('.')[0]
   return None
 
+# A mutable-array index must be `UInt`: `length(a)` is typed as the stdlib list
+# length (`UInt`) and the `<` overloads compare homogeneous pairs, so only a
+# `UInt` index can form the natural `i < length(a)` bound. Checked on the
+# mutable-array path only (#1117); pure-array indexing is left untouched.
+def _check_array_index_type(index: Term) -> None:
+  if _type_named(index.typeof, 'UInt'):
+    return
+  user_error(index.location,
+             'a mutable-array index must be a UInt, not '
+             + str(index.typeof))
+
+def _array_length_result_type(loc: Meta, rator: Term) -> Type:
+  # The result type of `length` applied to an array handle is whatever the
+  # in-scope `length` function returns for a list (`UInt` in the stdlib). We
+  # read it off the resolved operator so no `UInt` node is fabricated here and
+  # `length(a)` on an array agrees with `length` on a list.
+  match rator.typeof:
+    case FunctionType(_, _, _, return_type):
+      return return_type
+    case OverloadType(_, overloads):
+      for _, overload_type in overloads:
+        if isinstance(overload_type, FunctionType):
+          return overload_type.return_type
+  user_error(loc, 'cannot determine the result type of length for an array; '
+                  'is the standard library imported?')
+
+def _length_of_array(
+    loc: Meta, rator: Term, args: list[Term], env: Env,
+    recfun: RecursiveName, subterms: SubtermNames,
+) -> Term | None:
+  # `length(a)` where `a` is a mutable-array handle `[T]!` types as the
+  # array-length type (`UInt`) and stays symbolic (#1117). Returns None for any
+  # other `length` call -- including on a pure `[T]` array -- so the caller
+  # falls back to the ordinary list-`length` resolution. Scoping the intercept
+  # to `[T]!` keeps `ArrayLength` confined to procedure specifications and
+  # array-bounds obligations, which never reach the recursive-call or compiler
+  # walkers that pure runtime terms do.
+  if len(args) != 1 or _var_ref_base_name(rator) != 'length':
+    return None
+  new_arg = type_synth_term(args[0], env, recfun, subterms)
+  if not isinstance(new_arg.typeof, MutableArrayType):
+    return None
+  new_rator = type_synth_term(rator, env, recfun, subterms)
+  return ArrayLength(loc, _array_length_result_type(loc, new_rator), new_arg)
+
 def _nat_constructor_literal_value(term: Term) -> int | None:
   match term:
     case Mark(_, _, subject) | TAnnote(_, _, subject, _):
@@ -988,8 +1034,26 @@ def type_synth_term(
       match new_array.typeof:
         case ArrayType(loc2, elt_type):
           ret = ArrayGet(loc, elt_type, new_array, new_index)
+        case MutableArrayType(loc2, elt_type):
+          # A mutable-array read `a[i]` has the element type, requires an
+          # unsigned/integer index, and (in a later verifier pass) carries an
+          # `i < length(a)` bounds obligation built by imperative_verifier.
+          _check_array_index_type(new_index)
+          ret = ArrayGet(loc, elt_type, new_array, new_index)
         case _:
           user_error(loc, 'expected an array, not ' + str(new_array.typeof))
+
+    case Call(loc, _, rator, [arg]) if _var_ref_base_name(rator) == 'length':
+      # `length(a)` on an array handle types as the array-length type (`UInt`)
+      # and stays symbolic (#1117); on any other argument it is an ordinary
+      # `length` call on a list, handled by the general Call path.
+      length_term = _length_of_array(loc, rator, [arg], env, recfun, subterms)
+      if length_term is not None:
+        ret = length_term
+      else:
+        ret = type_check_call(loc, rator, [arg], env, recfun, subterms, None,
+                              term)
+        check_recursive_call(ret, recfun, subterms)
           
     case Call(loc, _, (OverloadedVar(loc2, ty2, [op_name, *_])
                        | ResolvedVar(loc2, ty2, op_name)), args) \
@@ -1237,6 +1301,18 @@ def type_check_term(
               + ' but got ' + str(ty))
       return new_term
       
+    case Call(loc, _, rator, [arg]) if _var_ref_base_name(rator) == 'length':
+      length_term = _length_of_array(loc, rator, [arg], env, recfun, subterms)
+      if length_term is not None:
+        if length_term.typeof != typ:
+          user_error(loc, 'expected a term of type ' + str(typ)
+                     + '\nbut got ' + str(length_term) + ' of type '
+                     + str(length_term.typeof))
+        return length_term
+      ret = type_check_call(loc, rator, [arg], env, recfun, subterms, typ, term)
+      check_recursive_call(ret, recfun, subterms)
+      return ret
+
     case Call(loc, _, rator, args):
       ret = type_check_call(loc, rator, args, env, recfun, subterms, typ, term)
       check_recursive_call(ret, recfun, subterms)
diff --git a/imperative_verifier.py b/imperative_verifier.py
index e2876d09..b4032f1f 100644
--- a/imperative_verifier.py
+++ b/imperative_verifier.py
@@ -28,12 +28,15 @@
 
 from dataclasses import dataclass, field
 from enum import Enum
-from typing import List, Optional, Tuple
+from typing import List, Optional, Sequence, Set, Tuple, cast
 
 from lark.tree import Meta
 
 import style
-from abstract_syntax import And, Bool, Env, Formula, Proof, is_true
+from abstract_syntax import (
+    And, ArrayGet, ArrayLength, Bool, Call, Env, Formula, Proof, ResolvedVar,
+    is_true,
+)
 
 
 class ObligationKind(Enum):
@@ -147,3 +150,55 @@ def _report_incomplete(self, env: Env) -> None:
         + style.orange('Goal:') + '\n\t' + str(self.goal)
         + givens_str(env),
         formula=self.goal, env=env)
+
+
+# --- array-bounds obligations for mutable-array reads (issue #1117) ----------
+
+def array_bounds_goal(read: ArrayGet) -> Formula:
+  """The bounds proof goal ``i < length(a)`` for a mutable-array read ``a[i]``.
+
+  ``read`` is an already-type-checked ``ArrayGet`` over a mutable array. The
+  goal is built with a base-name ``ResolvedVar('<')`` over an ``ArrayLength``
+  node -- the same post-typecheck constructor idiom ``mkEqual`` uses for ``=``
+  -- so it matches a ``requires i < length(a)`` precondition (or loop
+  invariant) of the same shape once ``discharge`` reduces both sides."""
+  loc = read.location
+  length = ArrayLength(read.subject.location, None, read.subject)
+  return cast(Formula, Call(loc, None, ResolvedVar(loc, None, '<'),
+                            [read.position, length]))
+
+
+def _read_key(read: ArrayGet) -> Tuple[object, object, str]:
+  """Identity of a source array access: its source span plus its rendered
+  form, so the same syntactic ``a[i]`` visited more than once in a pass is
+  recorded only once while two distinct accesses stay separate."""
+  loc = read.location
+  return (getattr(loc, 'start_pos', None), getattr(loc, 'end_pos', None),
+          str(read))
+
+
+@dataclass
+class ArrayBoundsObligations:
+  """Collect array-bounds obligations for the mutable-array reads seen in one
+  verification pass, deduplicating repeated reads of the same source access so
+  a given ``a[i]`` yields at most one ``i < length(a)`` goal (#1117)."""
+
+  _seen: Set[Tuple[object, object, str]] = field(default_factory=set)
+  _obligations: List[ImperativeObligation] = field(default_factory=list)
+
+  def record(self, read: ArrayGet,
+             givens: Sequence[Tuple[str, Formula]] = ()) -> None:
+    """Record the bounds obligation for one mutable-array read. A read whose
+    source access was already recorded in this pass is ignored."""
+    key = _read_key(read)
+    if key in self._seen:
+      return
+    self._seen.add(key)
+    self._obligations.append(
+        ImperativeObligation(read.location, array_bounds_goal(read),
+                             ObligationKind.ARRAY_BOUNDS,
+                             givens=list(givens)))
+
+  def obligations(self) -> List[ImperativeObligation]:
+    """The recorded obligations, in first-seen order."""
+    return list(self._obligations)
diff --git a/test-deduce.py b/test-deduce.py
index 783766e2..c835907a 100644
--- a/test-deduce.py
+++ b/test-deduce.py
@@ -268,6 +268,8 @@ def _patched_check_system_limits() -> None:
     "./test/should-error/proc_call_as_term.pf",
     "./test/should-warn/imperative_false_proc.pf",
     "./test/should-warn/imperative_allocation.pf",
+    "./test/should-warn/imperative_mutable_array.pf",
+    "./test/should-error/imperative_mutable_array_bad_index.pf",
     "./test/should-error/imperative_new_pure_term.pf",
     "./test/should-error/imperative_new_operator_name.pf",
     "./test/should-validate/imperative_import.pf",
diff --git a/test/should-error/imperative_mutable_array_bad_index.pf b/test/should-error/imperative_mutable_array_bad_index.pf
new file mode 100644
index 00000000..72df0023
--- /dev/null
+++ b/test/should-error/imperative_mutable_array_bad_index.pf
@@ -0,0 +1,9 @@
+// Phase 2h (issue #1117): a mutable-array read must be indexed by an
+// unsigned/integer type. Indexing a `[UInt]!` handle by a `bool` is a type
+// error, caught while type-checking the postcondition.
+import UInt
+
+proc bad_index(a: [UInt]!)
+  ensures a[true] = a[true]
+{
+}
diff --git a/test/should-error/imperative_mutable_array_bad_index.pf.err b/test/should-error/imperative_mutable_array_bad_index.pf.err
new file mode 100644
index 00000000..1a5c7ad3
--- /dev/null
+++ b/test/should-error/imperative_mutable_array_bad_index.pf.err
@@ -0,0 +1 @@
+./test/should-error/imperative_mutable_array_bad_index.pf:7.13-7.17: a mutable-array index must be a UInt, not bool
diff --git a/test/should-warn/imperative_mutable_array.pf b/test/should-warn/imperative_mutable_array.pf
new file mode 100644
index 00000000..e3bf5f91
--- /dev/null
+++ b/test/should-warn/imperative_mutable_array.pf
@@ -0,0 +1,15 @@
+// Phase 2h (issue #1117): `length(a)` and mutable-array reads `a[i]` on a
+// `[T]!` handle are now typed inside procedure specifications -- `length(a)`
+// has the array-length type (`UInt`) and `a[i]` the element type, so a
+// `requires i < length(a)` / `ensures result = a[i]` contract type-checks.
+// Bodies and specs are still only recognized, so the proc emits the Phase 1m
+// "accepted but not verified" warning (issue #1108).
+import UInt
+import List
+
+proc read_demo(a: [UInt]!, i: UInt) -> UInt
+  requires i < length(a)
+  ensures result = a[i]
+{
+  return a[i]
+}
diff --git a/test/should-warn/imperative_mutable_array.pf.warn b/test/should-warn/imperative_mutable_array.pf.warn
new file mode 100644
index 00000000..7e4a924c
--- /dev/null
+++ b/test/should-warn/imperative_mutable_array.pf.warn
@@ -0,0 +1 @@
+./test/should-warn/imperative_mutable_array.pf:10.1-15.2: warning: proc 'read_demo' is accepted but not verified -- parsing and declaration plumbing succeeded, but no verifier has run on its body or specs yet (experimental imperative layer, issue #854)
diff --git a/test/unit/test_array_bounds.py b/test/unit/test_array_bounds.py
new file mode 100644
index 00000000..90109c89
--- /dev/null
+++ b/test/unit/test_array_bounds.py
@@ -0,0 +1,153 @@
+"""Unit tests for mutable-array read typing and array-bounds obligations
+(issue #1117, Phase 2h).
+
+Two halves, both exercised without the CLI or the stdlib:
+
+  * ``type_synth_term`` on an ``ArrayGet`` distinguishes the pure ``[T]`` path
+    (unchanged) from the mutable ``[T]!`` path (element type + index check);
+  * ``imperative_verifier`` builds and deduplicates the ``i < length(a)``
+    bounds obligation for a mutable-array read.
+"""
+
+from lark.tree import Meta
+
+from abstract_syntax import (
+    ArrayGet, ArrayLength, ArrayType, BoolType, Call, Env, MutableArrayType,
+    ResolvedVar,
+)
+from checker_types import type_synth_term
+from error import IncompleteProof, UserError
+from imperative_verifier import (
+    ArrayBoundsObligations, ImperativeObligation, ObligationKind,
+    array_bounds_goal,
+)
+
+
+def _meta(start: int = 0, end: int = 1) -> Meta:
+  m = Meta()
+  m.empty = False
+  m.filename = 'test.pf'
+  m.line = 3
+  m.column = 5
+  m.start_pos = start
+  m.end_line = 3
+  m.end_column = 6
+  m.end_pos = end
+  return m
+
+
+def _env() -> Env:
+  return Env({'__current_module__': 'test'})
+
+
+def _rv(name: str) -> ResolvedVar:
+  return ResolvedVar(_meta(), None, name)
+
+
+def _uint_type() -> ResolvedVar:
+  # A stand-in for the `UInt` type: `_check_array_index_type` only inspects the
+  # type's base name, so a bare `UInt` reference is enough here -- no stdlib.
+  return ResolvedVar(_meta(), None, 'UInt')
+
+
+def _typing_env() -> Env:
+  # A bare env with array/scalar term vars -- no stdlib needed because the
+  # ArrayGet path only reads the subject's `typeof` and (for the mutable path)
+  # the index's `typeof`.
+  env = _env()
+  env = env.declare_term_var(_meta(), 'marr',
+                             MutableArrayType(_meta(), BoolType(_meta())))
+  env = env.declare_term_var(_meta(), 'parr',
+                             ArrayType(_meta(), BoolType(_meta())))
+  env = env.declare_term_var(_meta(), 'idx', _uint_type())
+  env = env.declare_term_var(_meta(), 'flag', BoolType(_meta()))
+  return env
+
+
+def _read(subject: str = 'marr', index: str = 'idx',
+          start: int = 0, end: int = 5) -> ArrayGet:
+  return ArrayGet(_meta(start, end), None, _rv(subject), _rv(index))
+
+
+# --- ArrayType vs MutableArrayType typing -----------------------------------
+
+def test_mutable_read_has_element_type() -> None:
+  ret = type_synth_term(_read('marr', 'idx'), _typing_env(), None, [])
+  assert isinstance(ret, ArrayGet)
+  assert ret.typeof == BoolType(_meta())
+
+
+def test_pure_read_is_unchanged_and_skips_index_check() -> None:
+  # The pure `[T]` path never checked the index type; a `bool` index that the
+  # mutable path rejects must still be accepted here so pure-array behavior is
+  # unchanged.
+  ret = type_synth_term(_read('parr', 'flag'), _typing_env(), None, [])
+  assert isinstance(ret, ArrayGet)
+  assert ret.typeof == BoolType(_meta())
+
+
+def test_mutable_read_rejects_non_integer_index() -> None:
+  try:
+    type_synth_term(_read('marr', 'flag'), _typing_env(), None, [])
+    assert False, 'expected a UserError for a bool index'
+  except UserError as e:
+    assert 'index must be' in str(e)
+
+
+def test_read_of_non_array_is_rejected() -> None:
+  try:
+    type_synth_term(_read('flag', 'idx'), _typing_env(), None, [])
+    assert False, 'expected a UserError for a non-array subject'
+  except UserError as e:
+    assert 'expected an array' in str(e)
+
+
+# --- bounds-obligation construction -----------------------------------------
+
+def test_bounds_goal_is_index_less_than_length() -> None:
+  goal = array_bounds_goal(_read('marr', 'idx'))
+  assert isinstance(goal, Call)
+  assert isinstance(goal.rator, ResolvedVar) and goal.rator.get_name() == '<'
+  index, length = goal.args
+  assert index == _rv('idx')
+  assert isinstance(length, ArrayLength) and length.subject == _rv('marr')
+
+
+def test_recording_a_read_yields_one_array_bounds_obligation() -> None:
+  collector = ArrayBoundsObligations()
+  collector.record(_read())
+  obligations = collector.obligations()
+  assert len(obligations) == 1
+  ob = obligations[0]
+  assert isinstance(ob, ImperativeObligation)
+  assert ob.kind is ObligationKind.ARRAY_BOUNDS
+  # Source-located at the read.
+  assert ob.location.start_pos == 0 and ob.location.end_pos == 5
+
+
+def test_duplicate_source_access_is_recorded_once() -> None:
+  collector = ArrayBoundsObligations()
+  collector.record(_read(start=0, end=5))
+  collector.record(_read(start=0, end=5))   # same source access
+  collector.record(_read(start=6, end=11))  # a distinct access
+  assert len(collector.obligations()) == 2
+
+
+# --- discharge --------------------------------------------------------------
+
+def test_in_bounds_read_verifies_when_precondition_supplies_the_bound() -> None:
+  collector = ArrayBoundsObligations()
+  collector.record(_read(),
+                   givens=[('pre', array_bounds_goal(_read()))])
+  collector.obligations()[0].discharge(_env())  # returns normally
+
+
+def test_missing_bounds_evidence_reports_array_bounds_diagnostic() -> None:
+  collector = ArrayBoundsObligations()
+  collector.record(_read())
+  try:
+    collector.obligations()[0].discharge(_env())
+    assert False, 'expected an IncompleteProof'
+  except IncompleteProof as e:
+    assert 'array bounds' in str(e)
+    assert 'test.pf:3.5' in str(e)
diff --git a/test/unit/test_ast_invariants.py b/test/unit/test_ast_invariants.py
index a0c748fb..fa683d8a 100644
--- a/test/unit/test_ast_invariants.py
+++ b/test/unit/test_ast_invariants.py
@@ -211,6 +211,10 @@ def _spec_ArrayGet() -> ast.ArrayGet:
     return ast.ArrayGet(_meta(), None, _var("xs"), ast.Int(_meta(), None, 0))
 
 
+def _spec_ArrayLength() -> ast.ArrayLength:
+    return ast.ArrayLength(_meta(), None, _var("xs"))
+
+
 def _spec_TLet() -> ast.TLet:
     return ast.TLet(_meta(), None, "x", _var("rhs"), _var("body"))
 
@@ -618,6 +622,7 @@ def _spec_AssociativeBinding() -> ast.AssociativeBinding:
     ast.Array: _spec_Array,
     ast.MakeArray: _spec_MakeArray,
     ast.ArrayGet: _spec_ArrayGet,
+    ast.ArrayLength: _spec_ArrayLength,
     ast.TLet: _spec_TLet,
     ast.And: _spec_And,
     ast.Or: _spec_Or,