diff --git a/Strata/DL/Imperative/CmdEval.lean b/Strata/DL/Imperative/CmdEval.lean
index 5ee378ef99..c5c99659f2 100644
--- a/Strata/DL/Imperative/CmdEval.lean
+++ b/Strata/DL/Imperative/CmdEval.lean
@@ -66,11 +66,7 @@ def Cmd.eval [BEq P.Ident] [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P 
       let e := EC.eval σ e
       let assumptions := EC.getPathConditions σ
       let c' := .assert label e md
-      let propType := match md.getPropertyType with
-        | some s => if s == MetaData.divisionByZero then .divisionByZero
-                    else if s == MetaData.arithmeticOverflow then .arithmeticOverflow
-                    else .assert
-        | none => .assert
+      let propType := convertMetaDataPropertyType md
       match EC.denoteBool e with
       | some true => -- Proved via evaluation.
         (c', EC.deferObligation σ (ProofObligation.mk label propType assumptions e md))
diff --git a/Strata/DL/Imperative/EvalContext.lean b/Strata/DL/Imperative/EvalContext.lean
index 1f823cb008..941fa3b15f 100644
--- a/Strata/DL/Imperative/EvalContext.lean
+++ b/Strata/DL/Imperative/EvalContext.lean
@@ -102,12 +102,13 @@ inductive PropertyType where
   | assert
   | divisionByZero
   | arithmeticOverflow
+  | outOfBoundsAccess
   deriving Repr, DecidableEq
 
 /-- Whether an unreachable path counts as pass for this property type.
     Assertions pass vacuously when unreachable; covers fail. -/
 def PropertyType.passWhenUnreachable : PropertyType → Bool
-  | .assert | .divisionByZero | .arithmeticOverflow => true
+  | .assert | .divisionByZero | .arithmeticOverflow | .outOfBoundsAccess => true
   | .cover => false
 
 instance : ToFormat PropertyType where
@@ -116,6 +117,21 @@ instance : ToFormat PropertyType where
     | .assert => "assert"
     | .divisionByZero => "division by zero check"
     | .arithmeticOverflow => "arithmetic overflow check"
+    | .outOfBoundsAccess => "out-of-bounds access check"
+
+/-- Convert a `MetaData` entry's property-type classification string to the
+    `PropertyType` enum. Falls back to `.assert` when the metadata carries
+    no classification or an unrecognized string; callers that emit
+    propertyType classifications should add a matching arm here. -/
+def convertMetaDataPropertyType {P : PureExpr} [BEq P.Ident]
+    (md : MetaData P) : PropertyType :=
+  match md.getPropertyType with
+  | some s =>
+    if s == MetaData.divisionByZero then .divisionByZero
+    else if s == MetaData.arithmeticOverflow then .arithmeticOverflow
+    else if s == MetaData.outOfBoundsAccess then .outOfBoundsAccess
+    else .assert
+  | none => .assert
 
 /--
 A proof obligation can be discharged by some backend solver or a dedicated
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index f3d3a384d1..28c15c480b 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -320,6 +320,9 @@ def MetaData.divisionByZero : String := "divisionByZero"
 /-- Metadata value for arithmetic-overflow property type classification. -/
 def MetaData.arithmeticOverflow : String := "arithmeticOverflow"
 
+/-- Metadata value for out-of-bounds-access property type classification. -/
+def MetaData.outOfBoundsAccess : String := "outOfBoundsAccess"
+
 /-- Read the property type classification from metadata, if present. -/
 def MetaData.getPropertyType {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Option String :=
   match md.findElem MetaData.propertyType with
diff --git a/Strata/DL/Lambda/IntBoolFactory.lean b/Strata/DL/Lambda/IntBoolFactory.lean
index a5de45f549..b58a2028ee 100644
--- a/Strata/DL/Lambda/IntBoolFactory.lean
+++ b/Strata/DL/Lambda/IntBoolFactory.lean
@@ -120,22 +120,27 @@ instance (n : Nat) : LambdaLeanType (.bitvec n) (BitVec n) where
 
 These build well-formed `WFLFunc`s that have no `concreteEval` or `body`. -/
 
-/-- General polymorphic unevaluated function with optional axioms.
-    Handles any arity and any number of type arguments. -/
+/-- General polymorphic unevaluated function with optional axioms and
+    preconditions. Handles any arity and any number of type arguments. -/
 @[inline]
 def polyUneval (n : T.Identifier) (typeArgs : List String)
     (inputs : List (T.Identifier × LMonoTy)) (output : LMonoTy)
     (axioms : List (LExpr T.mono) := [])
+    (preconditions :
+      List (FuncPrecondition (LExpr T.mono) T.Metadata) := [])
     (h_nodup : List.Nodup (inputs.map (·.1.name)) := by first | decide | grind)
     (h_ta_nodup : List.Nodup typeArgs := by grind)
     (h_inputs : ∀ ty, ty ∈ ListMap.values inputs →
       ty.freeVars ⊆ typeArgs := by first | decide | grind)
     (h_output : output.freeVars ⊆ typeArgs
       := by first | decide | grind)
+    (h_precond : ∀ p, p ∈ preconditions →
+      (LExpr.freeVars p.expr).map (·.1.name) ⊆ inputs.map (·.1.name)
+      := by first | decide | grind)
     (h_ta_no_gen : ∀ ta, ta ∈ typeArgs → ¬ ("$__ty".toList.isPrefixOf ta.toList = true)
       := by first | decide | grind) : WFLFunc T :=
   ⟨{ name := n, typeArgs := typeArgs, inputs := inputs, output := output,
-     axioms := axioms }, {
+     axioms := axioms, preconditions := preconditions }, {
     arg_nodup := h_nodup
     body_freevars := by intro b hb; simp at hb
     concreteEval_argmatch := by intro fn _ _ _ hfn; simp at hfn
@@ -144,7 +149,7 @@ def polyUneval (n : T.Identifier) (typeArgs : List String)
     typeArgs_nodup := h_ta_nodup
     inputs_typevars_in_typeArgs := h_inputs
     output_typevars_in_typeArgs := h_output
-    precond_freevars := by intro p hp; simp at hp
+    precond_freevars := h_precond
     typeArgs_no_gen_prefix := h_ta_no_gen
   }⟩
 
diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean
index 0fedf025c4..67002bf27f 100644
--- a/Strata/Languages/Core/Factory.lean
+++ b/Strata/Languages/Core/Factory.lean
@@ -499,10 +499,57 @@ def seqAppendFunc : WFLFunc CoreLParams :=
               else #true))]
     ])
 
-/- A `Sequence` selection function with type `∀a. Sequence a → int → a`. -/
+/-! ### Sequence bounds preconditions
+
+`Sequence.select` / `update` / `take` / `drop` carry bounds
+preconditions; the other `Sequence.*` ops are total. -/
+
+/-- Choice of upper-bound operator in `mkSeqBoundsPrecond`: `Lt` (strict) for
+    `Sequence.select`/`update`, `Le` (non-strict) for `Sequence.take`/`drop`.
+    Restricting the parameter to this inductive rather than taking an
+    arbitrary `WFLFunc` or `LExpr` makes it impossible to attach a partial
+    operator (which would create a nested precondition obligation) by
+    accident. -/
+private inductive SeqBoundKind where | Lt | Le
+
+/-- Returns the *upper-bound* comparison for `mkSeqBoundsPrecond`.
+    The lower bound is always `0 ≤ x` (see `mkSeqBoundsPrecond`), so this
+    method characterises only the upper comparison. A future partial
+    Sequence op requiring a non-`int` comparison (e.g. a bitvector variant)
+    should introduce a separate helper rather than extend this enum. -/
+private def SeqBoundKind.upperOpExpr : SeqBoundKind → LExpr CoreLParams.mono
+  | .Lt => (intLtFunc (T := CoreLParams)).opExpr
+  | .Le => (intLeFunc (T := CoreLParams)).opExpr
+
+/-- Precondition `0 <= varName && varName `k.upperOpExpr` Sequence.length(seqName)`.
+
+    `seqName` defaults to `"s"` since all four current call sites
+    (`Sequence.select`/`update`/`take`/`drop`) name their `Sequence a` input
+    that way. The parameter exists so a future partial Sequence op with a
+    different input name need only pass it explicitly rather than rely on a
+    hidden string literal. Either way, mismatches between the function's
+    declared inputs and the names used here are caught at elaboration by
+    `polyUneval`'s `h_precond` free-vars check. -/
+private def mkSeqBoundsPrecond
+    (varName : String) (k : SeqBoundKind) (seqName : String := "s") :
+    Strata.DL.Util.FuncPrecondition (LExpr CoreLParams.mono) CoreLParams.Metadata :=
+  let sVar  : LExpr CoreLParams.mono := .fvar default seqName (some (seqTy mty[%a]))
+  let xVar  : LExpr CoreLParams.mono := .fvar default varName (some mty[int])
+  let zero  : LExpr CoreLParams.mono := .intConst default 0
+  let lenS  : LExpr CoreLParams.mono := .app default seqLengthFunc.opExpr sVar
+  let lower : LExpr CoreLParams.mono :=
+    .app default (.app default (intLeFunc (T := CoreLParams)).opExpr zero) xVar
+  let upper : LExpr CoreLParams.mono :=
+    .app default (.app default k.upperOpExpr xVar) lenS
+  ⟨.app default (.app default (boolAndFunc (T := CoreLParams)).opExpr lower) upper,
+   default⟩
+
+/- A `Sequence` selection function with type `∀a. Sequence a → int → a`.
+   Partial: requires `0 <= i && i < Sequence.length(s)`. -/
 def seqSelectFunc : WFLFunc CoreLParams :=
   polyUneval "Sequence.select" ["a"]
     [("s", seqTy mty[%a]), ("i", mty[int])] mty[%a]
+    (preconditions := [mkSeqBoundsPrecond "i" .Lt])
 
 /- A `Sequence` build (snoc) function with type `∀a. Sequence a → a → Sequence a`.
    `build(s, v)` appends a single element `v` to the end of `s`. -/
@@ -555,7 +602,8 @@ def seqBuildFunc : WFLFunc CoreLParams :=
     ])
 
 /- A `Sequence` update function with type `∀a. Sequence a → int → a → Sequence a`.
-   `update(s, i, v)` returns a sequence identical to `s` except at index `i` where the value is `v`. -/
+   `update(s, i, v)` returns a sequence identical to `s` except at index `i` where the value is `v`.
+   Partial: requires `0 <= i && i < Sequence.length(s)`. -/
 def seqUpdateFunc : WFLFunc CoreLParams :=
   polyUneval "Sequence.update" ["a"]
     [("s", seqTy mty[%a]), ("i", mty[int]), ("v", mty[%a])]
@@ -606,6 +654,7 @@ def seqUpdateFunc : WFLFunc CoreLParams :=
                   (((~Sequence.select : (Sequence %a) → int → %a) %3) %0)
                 else #true)))]
     ])
+    (preconditions := [mkSeqBoundsPrecond "i" .Lt])
 
 /- A `Sequence` contains function with type `∀a. Sequence a → a → bool`.
    `contains(s, v)` is true iff there exists an index `i` such that `select(s, i) == v`. -/
@@ -628,7 +677,8 @@ def seqContainsFunc : WFLFunc CoreLParams :=
     ])
 
 /- A `Sequence` take function with type `∀a. Sequence a → int → Sequence a`.
-   `take(s, n)` returns the first `n` elements of `s`. -/
+   `take(s, n)` returns the first `n` elements of `s`.
+   Partial: requires `0 <= n && n <= Sequence.length(s)`. -/
 def seqTakeFunc : WFLFunc CoreLParams :=
   polyUneval "Sequence.take" ["a"]
     [("s", seqTy mty[%a]), ("n", mty[int])]
@@ -664,9 +714,11 @@ def seqTakeFunc : WFLFunc CoreLParams :=
                 (((~Sequence.select : (Sequence %a) → int → %a) %2) %0)
               else #true))]
     ])
+    (preconditions := [mkSeqBoundsPrecond "n" .Le])
 
 /- A `Sequence` drop function with type `∀a. Sequence a → int → Sequence a`.
-   `drop(s, n)` returns the sequence with the first `n` elements removed. -/
+   `drop(s, n)` returns the sequence with the first `n` elements removed.
+   Partial: requires `0 <= n && n <= Sequence.length(s)`. -/
 def seqDropFunc : WFLFunc CoreLParams :=
   polyUneval "Sequence.drop" ["a"]
     [("s", seqTy mty[%a]), ("n", mty[int])]
@@ -709,6 +761,7 @@ def seqDropFunc : WFLFunc CoreLParams :=
                     (((~Int.Add : int → int → int) %0) %1))
               else #true))]
     ])
+    (preconditions := [mkSeqBoundsPrecond "n" .Le])
 
 def emptyTriggersFunc : WFLFunc CoreLParams :=
   nullaryUneval "Triggers.empty" mty[Triggers]
diff --git a/Strata/Languages/Core/ObligationExtraction.lean b/Strata/Languages/Core/ObligationExtraction.lean
index 34eb371291..5cd3cd05f4 100644
--- a/Strata/Languages/Core/ObligationExtraction.lean
+++ b/Strata/Languages/Core/ObligationExtraction.lean
@@ -55,11 +55,7 @@ def extractGo (pc : PathConditions Expression) : Statements →
   | s :: rest, acc =>
     match s with
     | .cmd (.cmd (.assert label e md)) =>
-      let propType := match md.getPropertyType with
-        | some s => if s == MetaData.divisionByZero then .divisionByZero
-                    else if s == MetaData.arithmeticOverflow then .arithmeticOverflow
-                    else .assert
-        | none => .assert
+      let propType := convertMetaDataPropertyType md
       extractGo pc rest (acc.push (ProofObligation.mk label propType pc e md))
 
     | .cmd (.cmd (.cover label e md)) =>
diff --git a/Strata/Languages/Core/SarifOutput.lean b/Strata/Languages/Core/SarifOutput.lean
index 6e69cf014b..7874a9b912 100644
--- a/Strata/Languages/Core/SarifOutput.lean
+++ b/Strata/Languages/Core/SarifOutput.lean
@@ -29,7 +29,8 @@ def outcomeToLevel (mode : VerificationMode) (property : Imperative.PropertyType
   match mode, property, outcome.satisfiabilityProperty, outcome.validityProperty with
   -- Cover satisfied (sat on P∧Q): always pass
   | _, .cover, .sat _, _ => .none
-  -- Unreachable (both unsat): deductive=warning for assert/divisionByZero/arithmeticOverflow, error for cover and bugFinding modes
+  -- Unreachable (both unsat): deductive=warning for assert-like properties
+  -- (those that pass vacuously), error for cover and bugFinding modes.
   | .deductive, p, .unsat, .unsat => if p.passWhenUnreachable then .warning else .error
   | _, _, .unsat, .unsat => .error
   -- Pass: validity proven (unsat on P∧¬Q)
@@ -88,6 +89,7 @@ def extractLocation (files : Map Strata.Uri Lean.FileMap) (md : Imperative.MetaD
 def propertyTypeToClassification : Imperative.PropertyType → String
   | .divisionByZero => "division-by-zero"
   | .arithmeticOverflow => "arithmetic-overflow"
+  | .outOfBoundsAccess => "out-of-bounds-access"
   | .cover => "cover"
   | .assert => "assert"
 
@@ -111,6 +113,8 @@ def extractRelatedLocations (files : Map Strata.Uri Lean.FileMap) (md : Imperati
 def vcResultToSarifResult (mode : VerificationMode) (files : Map Strata.Uri Lean.FileMap) (vcr : VCResult) : Strata.Sarif.Result :=
   let ruleId := vcr.obligation.label
   let relatedLocations := extractRelatedLocations files vcr.obligation.metadata
+  let properties : Strata.Sarif.PropertyBag :=
+    { propertyType := propertyTypeToClassification vcr.obligation.property }
   match vcr.outcome with
   | .error err =>
     let level := .error
@@ -119,7 +123,7 @@ def vcResultToSarifResult (mode : VerificationMode) (files : Map Strata.Uri Lean
     let locations := match extractLocation files vcr.obligation.metadata with
       | some loc => #[locationToSarif loc]
       | none => #[]
-    { ruleId, level, message, locations, relatedLocations }
+    { ruleId, level, message, locations, relatedLocations, properties }
   | .ok outcome =>
     let level := outcomeToLevel mode vcr.obligation.property outcome
     let messageText := outcomeToMessage outcome
@@ -127,7 +131,7 @@ def vcResultToSarifResult (mode : VerificationMode) (files : Map Strata.Uri Lean
     let locations := match extractLocation files vcr.obligation.metadata with
       | some loc => #[locationToSarif loc]
       | none => #[]
-    { ruleId, level, message, locations, relatedLocations }
+    { ruleId, level, message, locations, relatedLocations, properties }
 
 /-- Convert VCResults to a SARIF document -/
 def vcResultsToSarif (mode : VerificationMode) (files : Map Strata.Uri Lean.FileMap) (vcResults : VCResults) : Strata.Sarif.SarifDocument :=
diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index ce2b35a975..57f800544d 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -320,11 +320,7 @@ private def createUnreachableAssertObligations
     Imperative.ProofObligations Expression :=
   asserts.toArray.map
     (fun (label, md) =>
-      let propType := match md.getPropertyType with
-        | some s => if s == Imperative.MetaData.divisionByZero then .divisionByZero
-                    else if s == Imperative.MetaData.arithmeticOverflow then .arithmeticOverflow
-                    else .assert
-        | _ => .assert
+      let propType := Imperative.convertMetaDataPropertyType md
       (Imperative.ProofObligation.mk label propType pathConditions (LExpr.true ()) md))
 
 /--
diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 86441d2fbb..8763abab03 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/Strata/Languages/Core/Verifier.lean
@@ -786,7 +786,7 @@ def label (o : VCOutcome) (property : Imperative.PropertyType)
   -- Simplified labels for minimal check level
   else if checkLevel == .minimal then
     if property.passWhenUnreachable then
-      -- Assert-like property (assert, divisionByZero, arithmeticOverflow)
+      -- Assert-like property (i.e. passes vacuously on unreachable paths).
       if checkMode == .deductive then
         match o.validityProperty with
         | .unsat => "pass"
diff --git a/Strata/Transform/PrecondElim.lean b/Strata/Transform/PrecondElim.lean
index ee77df3440..e16d42c025 100644
--- a/Strata/Transform/PrecondElim.lean
+++ b/Strata/Transform/PrecondElim.lean
@@ -76,6 +76,8 @@ private def classifyPrecondition (funcName : String) (precondIdx : Nat := 0) : O
   | .bv ⟨_, .SafeAdd⟩ | .bv ⟨_, .SafeSub⟩ | .bv ⟨_, .SafeMul⟩ | .bv ⟨_, .SafeNeg⟩
   | .bv ⟨_, .SafeUAdd⟩ | .bv ⟨_, .SafeUSub⟩ | .bv ⟨_, .SafeUMul⟩ | .bv ⟨_, .SafeUNeg⟩ =>
     some Imperative.MetaData.arithmeticOverflow
+  | .seq .Select | .seq .Update | .seq .Take | .seq .Drop =>
+    some Imperative.MetaData.outOfBoundsAccess
   | _ => none
 
 /--
diff --git a/StrataTest/Languages/Core/Examples/Seq.lean b/StrataTest/Languages/Core/Examples/Seq.lean
index 937c40858d..d124c1d619 100644
--- a/StrataTest/Languages/Core/Examples/Seq.lean
+++ b/StrataTest/Languages/Core/Examples/Seq.lean
@@ -68,6 +68,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30)) == 3
 
+Label: assert_t_0_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: t_0
 Property: assert
 Assumptions:
@@ -75,6 +82,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 0) == 10
 
+Label: assert_t_1_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 1 < Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: t_1
 Property: assert
 Assumptions:
@@ -82,6 +96,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1) == 20
 
+Label: assert_t_2_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 2 < Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: t_2
 Property: assert
 Assumptions:
@@ -102,14 +123,26 @@ Obligation: t_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_t_0_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: t_0
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_t_1_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: t_1
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_t_2_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: t_2
 Property: assert
 Result: ✅ pass
@@ -185,6 +218,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50))) == 5
 
+Label: assert_append_elem_0_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50)))
+
 Label: append_elem_0
 Property: assert
 Assumptions:
@@ -192,6 +232,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50)), 0) == 10
 
+Label: assert_append_elem_4_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 4 < Sequence.length(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50)))
+
 Label: append_elem_4
 Property: assert
 Assumptions:
@@ -199,6 +246,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.append(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), Sequence.build(Sequence.build(s, 40), 50)), 4) == 50
 
+Label: set_u_calls_Sequence.update_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 1 < Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: update_length
 Property: assert
 Assumptions:
@@ -206,6 +260,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.update(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1, 99)) == 3
 
+Label: assert_update_same_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 1 < Sequence.length(Sequence.update(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1, 99))
+
 Label: update_same
 Property: assert
 Assumptions:
@@ -213,6 +274,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.update(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1, 99), 1) == 99
 
+Label: assert_update_other_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.update(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1, 99))
+
 Label: update_other
 Property: assert
 Assumptions:
@@ -227,6 +295,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.contains(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 20)
 
+Label: set_u_calls_Sequence.take_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 2 <= Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: take_length
 Property: assert
 Assumptions:
@@ -234,6 +309,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.take(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 2)) == 2
 
+Label: assert_take_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.take(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 2))
+
 Label: take_elem
 Property: assert
 Assumptions:
@@ -241,6 +323,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.select(Sequence.take(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 2), 0) == 10
 
+Label: set_u_calls_Sequence.drop_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 1 <= Sequence.length(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30))
+
 Label: drop_length
 Property: assert
 Assumptions:
@@ -248,6 +337,13 @@ s_empty: Sequence.length(s) == 0
 Obligation:
 Sequence.length(Sequence.drop(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1)) == 2
 
+Label: assert_drop_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Assumptions:
+s_empty: Sequence.length(s) == 0
+Obligation:
+true && 0 < Sequence.length(Sequence.drop(Sequence.build(Sequence.build(Sequence.build(s, 10), 20), 30), 1))
+
 Label: drop_elem
 Property: assert
 Assumptions:
@@ -261,22 +357,42 @@ Obligation: append_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_append_elem_0_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: append_elem_0
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_append_elem_4_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: append_elem_4
 Property: assert
 Result: ✅ pass
 
+Obligation: set_u_calls_Sequence.update_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: update_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_update_same_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: update_same
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_update_other_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: update_other
 Property: assert
 Result: ✅ pass
@@ -285,18 +401,34 @@ Obligation: contains_yes
 Property: assert
 Result: ❓ unknown
 
+Obligation: set_u_calls_Sequence.take_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: take_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_take_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: take_elem
 Property: assert
 Result: ✅ pass
 
+Obligation: set_u_calls_Sequence.drop_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: drop_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_drop_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: drop_elem
 Property: assert
 Result: ✅ pass
@@ -365,6 +497,11 @@ Property: assert
 Obligation:
 Sequence.length(Sequence.build(Sequence.empty<int>(), 42)) == 1
 
+Label: assert_build_on_empty_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Obligation:
+true && 0 < Sequence.length(Sequence.build(Sequence.empty<int>(), 42))
+
 Label: build_on_empty_elem
 Property: assert
 Obligation:
@@ -380,6 +517,10 @@ Obligation: build_on_empty_length
 Property: assert
 Result: ✅ pass
 
+Obligation: assert_build_on_empty_elem_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
 Obligation: build_on_empty_elem
 Property: assert
 Result: ✅ pass
diff --git a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean
index 51d905cbd8..a415360eeb 100644
--- a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean
+++ b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean
@@ -85,12 +85,16 @@ func update : ∀[k, v]. ((m : (Map k v)) (i : k) (x : v)) → (Map k v);
 func Sequence.length : ∀[a]. ((s : (Sequence a))) → int;
 func Sequence.empty : ∀[a]. () → (Sequence a);
 func Sequence.append : ∀[a]. ((s1 : (Sequence a)) (s2 : (Sequence a))) → (Sequence a);
-func Sequence.select : ∀[a]. ((s : (Sequence a)) (i : int)) → a;
+func Sequence.select : ∀[a]. ((s : (Sequence a)) (i : int)) → a
+  requires 0 <= i && i < Sequence.length(s);
 func Sequence.build : ∀[a]. ((s : (Sequence a)) (v : a)) → (Sequence a);
-func Sequence.update : ∀[a]. ((s : (Sequence a)) (i : int) (v : a)) → (Sequence a);
+func Sequence.update : ∀[a]. ((s : (Sequence a)) (i : int) (v : a)) → (Sequence a)
+  requires 0 <= i && i < Sequence.length(s);
 func Sequence.contains : ∀[a]. ((s : (Sequence a)) (v : a)) → bool;
-func Sequence.take : ∀[a]. ((s : (Sequence a)) (n : int)) → (Sequence a);
-func Sequence.drop : ∀[a]. ((s : (Sequence a)) (n : int)) → (Sequence a);
+func Sequence.take : ∀[a]. ((s : (Sequence a)) (n : int)) → (Sequence a)
+  requires 0 <= n && n <= Sequence.length(s);
+func Sequence.drop : ∀[a]. ((s : (Sequence a)) (n : int)) → (Sequence a)
+  requires 0 <= n && n <= Sequence.length(s);
 func Triggers.empty :  () → Triggers;
 func Triggers.addGroup :  ((g : TriggerGroup) (t : Triggers)) → Triggers;
 func TriggerGroup.empty :  () → TriggerGroup;
diff --git a/StrataTest/Languages/Core/Tests/SarifOutputTests.lean b/StrataTest/Languages/Core/Tests/SarifOutputTests.lean
index 98c8cac9b0..ad488d023c 100644
--- a/StrataTest/Languages/Core/Tests/SarifOutputTests.lean
+++ b/StrataTest/Languages/Core/Tests/SarifOutputTests.lean
@@ -55,9 +55,10 @@ def makeFilesMap (file : String) : Map Strata.Uri Lean.FileMap :=
   Map.empty.insert uri makeFileMap
 
 /-- Create a simple proof obligation for testing -/
-def makeObligation (label : String) (md : MetaData Expression := #[]) : ProofObligation Expression :=
+def makeObligation (label : String) (md : MetaData Expression := #[])
+    (property : Imperative.PropertyType := .assert) : ProofObligation Expression :=
   { label := label
-    property := .assert
+    property := property
     assumptions := []
     obligation := Lambda.LExpr.boolConst () true
     metadata := md }
@@ -65,8 +66,9 @@ def makeObligation (label : String) (md : MetaData Expression := #[]) : ProofObl
 /-- Create a VCResult for testing -/
 def makeVCResult (label : String) (outcome : VCOutcome)
   (md : MetaData Expression := #[])
-  (lexprModel : LExprModel := []) : VCResult :=
-  { obligation := makeObligation label md
+  (lexprModel : LExprModel := [])
+  (property : Imperative.PropertyType := .assert) : VCResult :=
+  { obligation := makeObligation label md property
     outcome := .ok outcome
     verbose := .normal
     lexprModel := lexprModel
@@ -345,4 +347,33 @@ def makeVCResult (label : String) (outcome : VCOutcome)
   let sarif := vcResultsToSarif .deductive files vcResults
   Strata.Sarif.toJsonString sarif
 
+/-! ## Property classification tests
+
+The SARIF `properties.propertyType` field should reflect the obligation's
+`PropertyType`, not the default `"assert"`. -/
+
+private def sarifPropertyType (vcr : VCResult) : String :=
+  let files := makeFilesMap "/test/x.st"
+  (vcResultToSarifResult .deductive files vcr).properties.propertyType
+
+/-- info: "assert" -/
+#guard_msgs in
+#eval sarifPropertyType (makeVCResult "t" (mkOutcome (.sat []) .unsat) (property := .assert))
+
+/-- info: "division-by-zero" -/
+#guard_msgs in
+#eval sarifPropertyType (makeVCResult "t" (mkOutcome (.sat []) .unsat) (property := .divisionByZero))
+
+/-- info: "arithmetic-overflow" -/
+#guard_msgs in
+#eval sarifPropertyType (makeVCResult "t" (mkOutcome (.sat []) .unsat) (property := .arithmeticOverflow))
+
+/-- info: "out-of-bounds-access" -/
+#guard_msgs in
+#eval sarifPropertyType (makeVCResult "t" (mkOutcome (.sat []) .unsat) (property := .outOfBoundsAccess))
+
+/-- info: "cover" -/
+#guard_msgs in
+#eval sarifPropertyType (makeVCResult "t" (mkOutcome (.sat []) .unsat) (property := .cover))
+
 end Core.Sarif.Tests
diff --git a/StrataTest/Transform/PrecondElim.lean b/StrataTest/Transform/PrecondElim.lean
index 651ec8b0de..3242d25afa 100644
--- a/StrataTest/Transform/PrecondElim.lean
+++ b/StrataTest/Transform/PrecondElim.lean
@@ -418,4 +418,80 @@ procedure test (inout g : int, y : int)
 #guard_msgs in
 #eval (Std.format (transformProgram loopGuardPrecondPgm))
 
+/-! ### Test 10: `collectPrecondAsserts` tags Sequence bounds obligations with `outOfBoundsAccess`
+
+Exercises the full `collectPrecondAsserts` path — the code called by
+`transformStmt` / `mkContractWFProc` / `mkFuncWFProc` — and inspects the
+metadata on the generated assert. Mirrors `OverflowCheckTest.lean`. -/
+
+section SeqBoundsObligations
+
+open Strata Core Lambda Core.PrecondElim Imperative
+
+/-- Shared fvar fixtures so each per-op case below is a one-liner. -/
+private def fxS : Core.Expression.Expr := .fvar () ⟨"s", ()⟩ (some (Core.seqTy .int))
+private def fxI : Core.Expression.Expr := .fvar () ⟨"i", ()⟩ (some .int)
+private def fxV : Core.Expression.Expr := .fvar () ⟨"v", ()⟩ (some .int)
+private def fxN : Core.Expression.Expr := .fvar () ⟨"n", ()⟩ (some .int)
+private def fxJ : Core.Expression.Expr := .fvar () ⟨"j", ()⟩ (some .int)
+
+/-- Check that `collectPrecondAsserts` produces exactly `expectedCount`
+    obligations from `expr`, each tagged with `outOfBoundsAccess`. -/
+private def assertOutOfBoundsObligations
+    (expr : Core.Expression.Expr) (expectedCount : Nat) : IO Unit := do
+  let stmts := collectPrecondAsserts Core.Factory expr "test" #[]
+  assert! stmts.length == expectedCount
+  for s in stmts do
+    let md : MetaData Core.Expression := match s with
+      | Statement.assert _ _ md => md | _ => #[]
+    assert! md.getPropertyType == some MetaData.outOfBoundsAccess
+
+-- Sequence.select / update / take / drop each emit one out-of-bounds obligation.
+#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqSelectOp [fxS, fxI]) 1
+#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqUpdateOp [fxS, fxI, fxV]) 1
+#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqTakeOp   [fxS, fxN]) 1
+#eval assertOutOfBoundsObligations (LExpr.mkApp () Core.seqDropOp   [fxS, fxN]) 1
+
+-- Nested: `Sequence.select(Sequence.update(s, i, v), j)` emits two
+-- obligations (one per partial call), both tagged `outOfBoundsAccess`.
+#eval assertOutOfBoundsObligations
+  (LExpr.mkApp () Core.seqSelectOp [LExpr.mkApp () Core.seqUpdateOp [fxS, fxI, fxV], fxJ]) 2
+
+-- Sequence.length is total: no precondition obligations generated.
+#eval do
+  let stmts := collectPrecondAsserts Core.Factory
+    (LExpr.mkApp () Core.seqLengthOp [fxS]) "test" #[]
+  assert! stmts.isEmpty
+
+/-! #### Test 10a: Pretty-printed obligation shape per partial op
+
+Catches regressions that preserve count and metadata tag but corrupt the
+obligation body (e.g. swapping `.Lt` for `.Le` at a call site, changing
+the bound variable name, or swapping the lower/upper bound inside
+`mkSeqBoundsPrecond`). -/
+
+private def printFirstObligation (expr : Core.Expression.Expr) : IO Unit := do
+  let stmts := collectPrecondAsserts Core.Factory expr "test" #[]
+  match stmts.head? with
+  | some (Statement.assert _ e _) => IO.println s!"{Std.format e}"
+  | _ => IO.println "<unexpected>"
+
+/-- info: 0 <= i && i < Sequence.length(s) -/
+#guard_msgs in
+#eval printFirstObligation (LExpr.mkApp () Core.seqSelectOp [fxS, fxI])
+
+/-- info: 0 <= i && i < Sequence.length(s) -/
+#guard_msgs in
+#eval printFirstObligation (LExpr.mkApp () Core.seqUpdateOp [fxS, fxI, fxV])
+
+/-- info: 0 <= n && n <= Sequence.length(s) -/
+#guard_msgs in
+#eval printFirstObligation (LExpr.mkApp () Core.seqTakeOp [fxS, fxN])
+
+/-- info: 0 <= n && n <= Sequence.length(s) -/
+#guard_msgs in
+#eval printFirstObligation (LExpr.mkApp () Core.seqDropOp [fxS, fxN])
+
+end SeqBoundsObligations
+
 end PrecondElimTests