diff --git a/NEXT.md b/NEXT.md
index 6c2815f..29b6544 100644
--- a/NEXT.md
+++ b/NEXT.md
@@ -102,8 +102,12 @@ test/programs/bounds.flan:25:29: slice [2 1) is out of bounds for length 5   (ex
 Three check sites, and the third is the one with the trap in it:
 
 - **`at` on `[n T]`** — the bound is static, so LLVM folds the check away for a
-  literal index. A literal that is *out* of bounds still only traps at runtime;
-  rejecting it in `check.ml` is a separate job.
+  literal index. A literal that is *out* of bounds never reaches emit at all:
+  `check.ml` rejects it, along with a negative literal index (wrong whatever
+  the target) and a literal `slice` range that runs backwards. Only literals —
+  a `defconst` is a global in the typed IR, not a folded constant, so
+  `(at a k)` stays a runtime trap. A slice bound may sit one past the end and
+  an index may not, which is the one place the two rules differ.
 - **`at` on a slice or string** — the bound is the runtime len.
 - **`slice`** — *two* comparisons, `lo <= hi` and `hi <= len`, both non-strict
   because a slice ending at len (or an empty one at `lo = len`) is legal and
diff --git a/lib/check.ml b/lib/check.ml
index 1786c03..84ddfa0 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -529,6 +529,25 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
      | other ->
        fail loc "deref takes a (Ptr T), found %s" (Types.to_string other))
 
+(* An index or a slice bound that is a literal is known now, so it is an error
+   now rather than a trap later. Only literals: a [defconst] is a global in the
+   typed IR, not a folded constant, so [(at arr size)] still traps at runtime —
+   which is what the emitted bounds check is for. A negative literal is wrong
+   whatever the target, but a length is static only for [n T]. *)
+and static_index loc (ty : Types.t) ~past_end what k =
+  if k < 0L then
+    fail loc "%s %Ld is negative — indices count from 0" what k;
+  match ty with
+  (* [past_end] is the difference between an index and a slice bound: the last
+     valid index is len - 1, but a slice may end at len. *)
+  | Types.Array (n, _) when if past_end then k > n else k >= n ->
+    fail loc "%s %Ld is out of bounds for length %Ld" what k n
+  | _ -> ()
+
+(* The literal value of a checked expression, if it has one. *)
+and literal (e : Tast.expr) =
+  match e.Tast.e with Tast.Int (k, _) -> Some k | _ -> None
+
 (* [(at a i)] and [(at grid row col)]: one index per dimension. *)
 and indexed ctx (target : Tast.expr) (idx : Ast.expr list) =
   let rec go ty = function
@@ -540,7 +559,11 @@ and indexed ctx (target : Tast.expr) (idx : Ast.expr list) =
         | other ->
           fail i.Ast.loc "%s cannot be indexed" (Types.to_string other)
       in
+      let loc = i.Ast.loc in
       let i = check ctx ~want:index_ty i in
+      (match literal i with
+       | Some k -> static_index loc ty ~past_end:false "index" k
+       | None -> ());
       let rest, ty = go elem rest in
       i :: rest, ty
   in
@@ -616,8 +639,23 @@ and named_call ctx ~want loc name args =
                       (Types.to_string other)
        in
        prim Tast.Slice (Types.Slice elem)
-         (let lo = check ctx ~want:index_ty lo in
-          [ target; lo; check ctx ~want:index_ty hi ])
+         (let lo_loc = lo.Ast.loc and hi_loc = hi.Ast.loc in
+          let lo = check ctx ~want:index_ty lo in
+          let hi = check ctx ~want:index_ty hi in
+          let ty = target.Tast.ty in
+          (* A bound may sit one past the end, so the length is checked against
+             lo and hi both, not against the last valid index. *)
+          (match literal lo with
+           | Some k -> static_index lo_loc ty ~past_end:true "slice bound" k
+           | None -> ());
+          (match literal hi with
+           | Some k -> static_index hi_loc ty ~past_end:true "slice bound" k
+           | None -> ());
+          (match literal lo, literal hi with
+           | Some a, Some b when a > b ->
+             fail loc "slice [%Ld %Ld) runs backwards — lo must not exceed hi" a b
+           | _ -> ());
+          [ target; lo; hi ])
      | _ -> assert false)
 
   (* ── pointers ──────────────────────────────────────────────────── *)
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 8bd4e37..6cfa3c2 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -403,6 +403,41 @@ let () =
   rejects_check "if branches disagree"
     "(defn f [] i32 (if true 1 true))" ~needle:"expected i32";
 
+  (* ── Static bounds ─────────────────────────────────────────────── *)
+  (* A literal index into a fixed array is known now, so it is an error now
+     rather than a trap later; everything else is the emitted bounds check's
+     job. A [defconst] is a global in the typed IR, not a folded constant, so
+     it deliberately stays a runtime trap. *)
+  let arr = "(defvar a [3 i32]) " in
+  accepts "last valid index"        (arr ^ "(defn f [] i32 (at a 2))");
+  rejects_check "index past the end" (arr ^ "(defn f [] i32 (at a 3))")
+    ~needle:"out of bounds for length 3";
+  rejects_check "negative index"     (arr ^ "(defn f [] i32 (at a -1))")
+    ~needle:"is negative";
+  rejects_check "index past the end of an inner dimension"
+    "(defvar g [2 [4 i32]]) (defn f [] i32 (at g 1 4))"
+    ~needle:"out of bounds for length 4";
+  accepts "a variable index is checked at runtime, not here"
+    (arr ^ "(defn f [i i32] i32 (at a i))");
+  accepts "a defconst index is not folded"
+    ("(defconst k 9) " ^ arr ^ "(defn f [] i32 (at a k))");
+
+  (* A slice bound may sit one past the end; an index may not. *)
+  accepts "slice ending at len"      (arr ^ "(defn f [] [i32] (slice a 1 3))");
+  accepts "empty slice at len"       (arr ^ "(defn f [] [i32] (slice a 3 3))");
+  rejects_check "slice bound past len" (arr ^ "(defn f [] [i32] (slice a 1 4))")
+    ~needle:"out of bounds for length 3";
+  rejects_check "negative slice bound" (arr ^ "(defn f [] [i32] (slice a -1 2))")
+    ~needle:"is negative";
+  rejects_check "reversed slice"     (arr ^ "(defn f [] [i32] (slice a 2 1))")
+    ~needle:"runs backwards";
+  (* A slice has no static length, so only the two target-independent rules
+     apply to one. *)
+  rejects_check "reversed slice of a slice"
+    "(defn f [s [u8]] [u8] (slice s 2 1))" ~needle:"runs backwards";
+  accepts "a slice's length is not known here"
+    "(defn f [s [u8]] [u8] (slice s 0 99))";
+
   (* ── Structs, fields and auto-deref ────────────────────────────── *)
   let cursor = "(defstruct Cursor [src [u8] pos i32]) " in
   accepts "struct literal, omitted field zeroed"