diff --git a/docs/BUGS-2026-09-18.md b/docs/BUGS-2026-09-18.md
index 077726f..e3780f5 100644
--- a/docs/BUGS-2026-09-18.md
+++ b/docs/BUGS-2026-09-18.md
@@ -78,10 +78,13 @@ territory; fix or record, the lane's call.
   (printed garbage). Breaks the premise stated in the clone note at check.ml:4152.
   Candidate fixes: refuse `free` of a non-binding target, or region-check the element at
   `push`/`put`. Sixth on the list; needs a deliberate mixed-allocator construction.
-- **Reversed slice under `--no-bounds-checks`**: the `lo <= hi` test is a representation
-  invariant, not a bounds check, but sits behind `if f.md.checks` in both backends
-  (`emit.ml:1037`, `x86.ml:2164`; same for SliceFromPtr's `n >= 0`). A negative-length
-  slice reaches user code. `flan_vec_as_slice` checks unconditionally — the model.
+- **Reversed slice under `--no-bounds-checks`** — **fixed**. The `lo <= hi` test is a
+  representation invariant, not a bounds check, but sat behind `if f.md.checks` in both
+  backends (`emit.ml:1037`, `x86.ml:2164`; same for SliceFromPtr's `n >= 0`), so a
+  negative-length slice reached user code. Split in both backends: `hi <= len` stays
+  behind the flag, `lo <= hi` and `n >= 0` are now emitted in every build, through the
+  same slice-failure path. `flan_vec_as_slice` was the model. See "A slice's length word
+  is a count" in docs/BUILT.md.
 - ~~**`reg leaks` lies at >3072 live blocks**~~ — **fixed**. Compaction now also asks
   whether there is an eighth of a table's worth of dead to reclaim, so a table full of
   live blocks stops thrashing the epoch; `flan_dev_reg_by_type` returns −1 with an unread
@@ -108,8 +111,20 @@ territory; fix or record, the lane's call.
   explicit or autoincremented, is range-checked against i32 in the parser before the collision scan,
   so the scan compares the numbers the program will actually have. Out of range is refused
   by name (`parse/enum-value-out-of-range`); explicit-duplicate aliasing stays legal.
-- **NaN sign**: LLVM constant-folds `0.0/0.0` to `nan`, x86 computes `-nan` — a stdout
-  DIFFER on a two-line program. Runtime paths agree (`-nan` both).
+- **NaN sign** — **fixed**. LLVM constant-folded `0.0/0.0` to `nan`, x86 computed `-nan`
+  — a stdout DIFFER on a two-line program. Resolved by canonicalizing the *printed* form
+  rather than the arithmetic: `flan_f64_to_bytes` and the two dev emitters render any NaN
+  as unsigned `nan`, which is what `format-f64` in the prelude always did. Pinned in
+  `test/programs/format.flan`. See docs/BUILT.md.
+- **x86's slice-from-ptr refusal is the wrong sentence**: `x86.ml` still reports a
+  negative promise through `flan_slice_error` — "slice [0 -2) is out of bounds for
+  length 0", naming a range and a length the caller never wrote — where `emit.ml` has
+  its own `flan_slice_promise_error`. Same condition and same exit on both sides, only
+  the text differs. The survey cannot see it: `bounds.flan` picks its case out of
+  `(at args 1)` and `survey.sh` runs every program with no arguments, so nothing in the
+  corpus reaches the `n = -2` case on the x86 path. Noticed while making the check
+  unconditional (which did not change what it prints); the fix is one `bounds_call` with
+  one extra instead of three.
 - **`emit.ml:3369` transient test ignores `new_globals`**: on the `retains=false` path a
   module first to intern a global gets dlclosed; zero-init makes it moot today, a literal
   init would dangle.
diff --git a/docs/BUILT.md b/docs/BUILT.md
index 597e3f2..7521e67 100644
--- a/docs/BUILT.md
+++ b/docs/BUILT.md
@@ -5723,3 +5723,74 @@ position, and requires the error overlay to start at exactly that position.
 The in-buffer `m` sends its text *un*padded, which is the honest shape there: the expansion is in no file, so
 there is no line or column for a refusal to be drawn at. The `:file` still goes on the wire, because that is what
 says which session's macros to expand against.
+
+## A slice's length word is a count
+
+`--no-bounds-checks` used to drop two different claims because they were written as one
+`and`. Splitting them is the whole of the change in `check_slice`, in both backends.
+
+`hi <= len` is a **bounds check**. It asks whether the range a caller wrote fits inside
+the thing being sliced, and the answer depends on a length that has nothing to do with
+the result's shape. Dropping it is what the flag is for: a release decision, taken by
+someone who has decided their indices are right and will accept undefined behaviour if
+they are not. It stays behind `f.md.checks`.
+
+`lo <= hi` is **not a bounds check**, and the old comment beside it said as much while the
+code did the opposite. A slice is `{ptr, i64}` and the `i64` is a count: the emitted
+`sub` computes it as `hi - lo`, and the `len` primitive, a re-slice, `flan_write_stdout`
+and any C the value is handed to all read it as a non-negative number of elements.
+`(slice s 2 1)` does not build an out-of-range slice, it builds a value that is not a
+slice — the length word holds -1, which as a count is 18446744073709551615. No build
+wants that, so no flag turns the test off. `flan_vec_as_slice` in the runtime has always
+validated its own `l > h` unconditionally, in plain C, on the same grounds; this is that
+rule arriving on the emitted path.
+
+`slice-from-ptr`'s `n >= 0` is the same claim spelled the other way, and it moved out
+from behind the flag with it. The argument for gating it read well — dropping bounds
+checks is a release decision, so this goes off with the rest — and was a category error:
+a bounds check compares an index against a length the compiler knows, and this form has
+no length to compare against, which is the first thing its own comment says. What it
+tests is that the word about to become the slice's count is a count.
+
+Mechanically: `emit.ml` emits two `signal_block`s rather than one `and i1`, so an
+unchecked build carries exactly one compare and a checked one carries the two it always
+did. `x86.ml` keeps all three frame temporaries stored outside the flag and gates only
+the second compare — the third temporary is the length the message prints, and gating its
+store with its compare would trap correctly with a garbage number in the text, which is
+the kind of wrong answer that builds, links, and passes any test that reads the IR.
+
+Both still report through `flan_slice_error` (`flan_slice_promise_error` for the promise),
+because from a handler's point of view there is one condition here — a range that was
+refused — and which half was violated is in the sentence, not in the type.
+
+The runtime's `clamp_len` stays. It was written *because* this hole existed: a release
+build handed it a length of -1 and it was the last thing between that and a 511-byte read
+off the end of a slice. `check_slice` no longer lets the value out of Flan, but
+`clamp_len` takes a raw `(ptr, len)` pair, and the FFI, a C caller and a caller's own
+`slice-from-ptr` promise all reach it. A function correct on its own arguments does not
+become incorrect because its callers improved.
+
+## A NaN prints without a sign
+
+`(/ 0.0 0.0)` printed `nan` through LLVM and `-nan` through the x86 backend. Neither is
+wrong about the arithmetic: IEEE 754 does not specify the sign of a NaN any operation
+produces, LLVM's constant folder answers with the positive quiet NaN at compile time, and
+`divsd` answers with the negative one at run time. Putting the operands in `defvar`
+globals so nothing folds makes both say `-nan`, which is what confirms the divergence is
+the folding path and not a disagreement about float arithmetic.
+
+The fix is at the **print site**, not in the arithmetic, and the reason to prefer it is
+not cross-backend agreement — that is a side effect. `format-f64` in the prelude has
+always rendered this value as `nan`: it reaches the case through `(not (= x x))` and has
+no sign bit in its hands at all. So a build where `(print x)` said `-nan` and
+`(show x 2)` said `nan` was already contradicting itself about one value inside one
+backend. `flan_f64_to_bytes` now renders any NaN as `nan`, and `flan_dev_emit_f64` and
+`flan_dev_watch_emit_f64` do the same, because the REPL and `println` are held to
+agreeing about what a value looks like — the same rule the escape tables beside them
+already follow. `print` agrees with `show` first; the two backends agree second.
+
+The test is `x != x` rather than `isnan`, which keeps `math.h` out of the runtime and is
+the same comparison the prelude uses. An infinity still prints signed: there the sign is
+the value, and the backends were always agreed about it. Pinned in
+`test/programs/format.flan`, which is in the x86 survey corpus, so one program holds both
+the printed form under `dune test` and the agreement under the survey.
diff --git a/lib/emit.ml b/lib/emit.ml
index a76ec7a..94cfa21 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -1031,22 +1031,49 @@ let check_at f ~guard loc idx len =
   end
 
 (* [slice] is not: a slice ending at len — or an empty one at lo = len — is
-   legal, and its one-past-the-end gep is defined. [lo <= hi] is not redundant
-   with it, because a reversed range would otherwise yield hi - lo as a huge
-   unsigned length, which is a worse hole than the missing check. *)
+   legal, and its one-past-the-end gep is defined.
+
+   Two tests, and they are not the same kind of test, which is the whole of
+   what this function has to get right. [hi <= len] is a bounds check: it asks
+   whether the range the caller wrote fits inside the thing being sliced, and
+   the answer depends entirely on a length that is nothing to do with the
+   result's representation. Dropping it is what [--no-bounds-checks] is for —
+   a release decision, taken by someone who has decided their indices are
+   right and will accept undefined behaviour if they are not.
+
+   [lo <= hi] is not that. The value this expression builds is a [%slice],
+   which is {ptr, i64}, and the i64 is a *count*: the sub below computes it as
+   hi - lo, and every consumer in the language and in the runtime reads it as
+   a non-negative number of elements. A reversed range does not produce an
+   out-of-range slice, it produces a slice that is not a slice — (slice s 2 1)
+   writes -1 into the length word, and -1 as an unsigned count is
+   18446744073709551615. That value is not a bounds error anyone can opt out
+   of; it is a malformed value of the type, and it goes on to be passed,
+   stored, re-sliced and handed to C. So the test rides ahead of the flag: it
+   is emitted in every build, at -O0, at -O2, with checks on and with checks
+   off, exactly the way flan_vec_as_slice in the runtime validates [l > h]
+   unconditionally and for the same reason.
+
+   Two [signal_block]s and not one [and], so that the unchecked build emits
+   exactly one compare and the checked build emits the two it always did. Both
+   report through @flan_slice_error with the same three numbers, because from
+   a handler's point of view there is still one condition here — a range that
+   was refused — and which half of it was violated is in the text. *)
 let check_slice f ~guard loc lo hi len =
-  if f.md.checks then begin
-    let a = fresh f in
-    ins f "%s = icmp ule i64 %s, %s" a lo hi;
-    let b = fresh f in
-    ins f "%s = icmp ule i64 %s, %s" b hi len;
-    let ok = fresh f in
-    ins f "%s = and i1 %s, %s" ok a b;
+  let fail ok =
     signal_block f loc ~guard ok (fun id n ->
       ins f
         "call void @flan_slice_error(ptr %s, i64 %d, i64 %s, i64 %s, i64 %s, \
          ptr %s)"
         id n lo hi len xfer_param)
+  in
+  let a = fresh f in
+  ins f "%s = icmp ule i64 %s, %s" a lo hi;
+  fail a;
+  if f.md.checks then begin
+    let b = fresh f in
+    ins f "%s = icmp ule i64 %s, %s" b hi len;
+    fail b
   end
 
 (* ── Expressions ───────────────────────────────────────────────────── *)
@@ -2129,10 +2156,19 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
      to i64 is a huge unsigned value that [ule] waves straight through.
 
      It goes through [signal_block] for the reason the other two bounds checks
-     do — a bad length signals BoundsError and is answerable — and behind
-     [f.md.checks] for the reason they are: dropping bounds checks is a release
-     decision, not an optimisation one, so this is on at -O0 and -O2 alike and
-     off only when checks as a whole were asked off.
+     do — a bad length signals BoundsError and is answerable. It is *not*
+     behind [f.md.checks], and the argument that it should be was the argument
+     this paragraph used to make: that dropping bounds checks is a release
+     decision, so this goes off with the rest of them. That reads well and is
+     a category error. A bounds check compares a caller's index against a
+     length the compiler knows; this has no length to compare against — the
+     paragraph above says so in its first sentence — so there is nothing here
+     for [--no-bounds-checks] to be dropping. What it tests is that the word
+     about to be written into the [%slice]'s length field is a count and not a
+     negative number reinterpreted as an enormous one. That is [check_slice]'s
+     [lo <= hi], spelled the other way round, and it holds in every build for
+     the same reason: a slice with a negative length is not an unchecked slice,
+     it is not a slice.
 
      It has its own runtime function, @flan_slice_promise_error, and that is
      the whole of what it needed. It used to borrow @flan_slice_error — the
@@ -2148,14 +2184,12 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
     let nv = value f n in
     let n64 = fresh f in
     ins f "%s = sext i32 %s to i64" n64 nv;
-    if f.md.checks then begin
-      let ok = fresh f in
-      ins f "%s = icmp sge i64 %s, 0" ok n64;
-      signal_block f e.Tast.loc ~guard:(fun () -> guard f) ok (fun id len ->
-        ins f
-          "call void @flan_slice_promise_error(ptr %s, i64 %d, i64 %s, ptr %s)"
-          id len n64 xfer_param)
-    end;
+    let ok = fresh f in
+    ins f "%s = icmp sge i64 %s, 0" ok n64;
+    signal_block f e.Tast.loc ~guard:(fun () -> guard f) ok (fun id len ->
+      ins f
+        "call void @flan_slice_promise_error(ptr %s, i64 %d, i64 %s, ptr %s)"
+        id len n64 xfer_param);
     let a = fresh f in
     ins f "%s = insertvalue %%slice zeroinitializer, ptr %s, 0" a pv;
     let b = fresh f in
diff --git a/lib/x86.ml b/lib/x86.ml
index cbd5c20..ffba06c 100644
--- a/lib/x86.ml
+++ b/lib/x86.ml
@@ -2165,37 +2165,63 @@ and check_at f (base : loc) (ty : Types.t) (i : Tast.expr) (iv : loc) =
         lbl f.b ok)
 
 (* [slice] is not strict: a slice ending at len — or an empty one at lo = len —
-   is legal. [lo <= hi] is not redundant with [hi <= len], because a reversed
-   range would otherwise yield hi - lo as a huge unsigned length, which is a
-   worse hole than the missing check. *)
+   is legal. Two compares, and only one of them is a bounds check.
+
+   [hi <= len] is the bounds check. It asks whether the caller's range fits
+   inside the thing being sliced, which is a question about a length this
+   backend has to go and load, and [--no-bounds-checks] exists to stop asking
+   it — the release decision, taken by someone who accepts undefined behaviour
+   if their indices are wrong.
+
+   [lo <= hi] is a different claim and survives the flag. The two words stored
+   at the bottom of this case are a slice, and the second is a *count*: the
+   `sub` in the caller computes hi - lo, and everything downstream — the len
+   primitive, a re-slice, flan_write_stdout, any C this is handed to — reads
+   it as a non-negative number of elements. A reversed range does not build an
+   out-of-range slice, it builds a value that is not a slice: (slice s 2 1)
+   stores -1, and -1 read as a count is 18446744073709551615. There is no
+   build in which that is the intended behaviour, so there is no flag that
+   turns the compare off. flan_vec_as_slice validates its own [l > h]
+   unconditionally in plain C and always has; this is the same rule, arriving
+   late on the emitted path.
+
+   Hence the shape below. All three frame temporaries are stored before either
+   compare and outside the flag, because [bounds_call] reads all three and the
+   third is the length the message prints — gate the store along with the
+   compare and an unchecked build traps with the right range beside a garbage
+   length, which is a wrong answer that builds, links and passes every test
+   that reads the IR rather than the text. *)
 and check_slice f (base : loc) (ty : Types.t) (loc : Loc.t) (lo : Tast.expr)
       (llo : loc) (hi : Tast.expr) (lhi : loc) =
-  if f.md.Emit.checks then
-    let len =
-      match ty with
-      | Types.Array (n, _) -> Some (`Const n)
-      | Types.Slice _ | Types.String -> Some (`At (shift base 8))
-      | _ -> None
-    in
-    match len with
-    | None -> ()
-    | Some len ->
-      scoped f (fun () ->
-        let a = ptmp f and b = ptmp f and c = ptmp f in
-        load_loc f ~reg:rax llo lo.Tast.ty;
-        store_int f.b ~src:rax ~mm:(Frame a) ~size:8;
-        load_loc f ~reg:rdx lhi hi.Tast.ty;
-        store_int f.b ~src:rdx ~mm:(Frame b) ~size:8;
-        load_len f len;
-        store_int f.b ~src:rcx ~mm:(Frame c) ~size:8;
-        let ok = new_label f "inb" and bad = new_label f "oob" in
-        cmp_rr f.b ~a:rax ~c:rdx;
+  let len =
+    match ty with
+    | Types.Array (n, _) -> Some (`Const n)
+    | Types.Slice _ | Types.String -> Some (`At (shift base 8))
+    | _ -> None
+  in
+  match len with
+  | None -> ()
+  | Some len ->
+    scoped f (fun () ->
+      let a = ptmp f and b = ptmp f and c = ptmp f in
+      load_loc f ~reg:rax llo lo.Tast.ty;
+      store_int f.b ~src:rax ~mm:(Frame a) ~size:8;
+      load_loc f ~reg:rdx lhi hi.Tast.ty;
+      store_int f.b ~src:rdx ~mm:(Frame b) ~size:8;
+      load_len f len;
+      store_int f.b ~src:rcx ~mm:(Frame c) ~size:8;
+      let ok = new_label f "inb" in
+      cmp_rr f.b ~a:rax ~c:rdx;
+      if f.md.Emit.checks then begin
+        let bad = new_label f "oob" in
         jcc_lbl f.b ~cc:cc_a bad;
         cmp_rr f.b ~a:rdx ~c:rcx;
         jcc_lbl f.b ~cc:cc_be ok;
-        lbl f.b bad;
-        bounds_call f "flan_slice_error" loc [ a; b; c ];
-        lbl f.b ok)
+        lbl f.b bad
+      end else
+        jcc_lbl f.b ~cc:cc_be ok;
+      bounds_call f "flan_slice_error" loc [ a; b; c ];
+      lbl f.b ok)
 
 (* [emit.ml]'s [check_div] and [check_cast], item 3 of docs/handoffs/HANDOFF-x86-rt.md's
    list, and the one item on it that was blocked on a language decision rather
@@ -2666,23 +2692,31 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) dst =
 
      It reuses [flan_slice_error] for [emit.ml]'s reason: the violated
      condition is 0 <= n, which has the shape of a reversed slice, so the range
-     is reported as [0 n) against a length of 0. *)
+     is reported as [0 n) against a length of 0.
+
+     It is not behind [f.md.Emit.checks], and the reason is the one
+     [check_slice] above spells out at length. [--no-bounds-checks] drops a
+     comparison against a known length; this comparison has no length to be
+     against — the paragraph above says as much — so the flag has nothing here
+     to drop. The word being stored into the second half of [dst] is the
+     slice's count, and a count that is negative is not a slice with the
+     bounds check taken off, it is not a slice. So the test runs in every
+     build, exactly as [lo <= hi] does. *)
   | Tast.SliceFromPtr, [ p; n ] ->
     let lp = eval f p in
     let ln = eval f n in
-    if f.md.Emit.checks then
-      scoped f (fun () ->
-        let a = ptmp f and b = ptmp f and c = ptmp f in
-        xor_rr f.b ~dst:rax ~src:rax;
-        store_int f.b ~src:rax ~mm:(Frame a) ~size:8;
-        store_int f.b ~src:rax ~mm:(Frame c) ~size:8;
-        load_loc f ~reg:rax ln n.Tast.ty;
-        store_int f.b ~src:rax ~mm:(Frame b) ~size:8;
-        cmp_imm f.b ~dst:rax 0;
-        let ok = new_label f "inb" in
-        jcc_lbl f.b ~cc:cc_ge ok;
-        bounds_call f "flan_slice_error" e.Tast.loc [ a; b; c ];
-        lbl f.b ok);
+    scoped f (fun () ->
+      let a = ptmp f and b = ptmp f and c = ptmp f in
+      xor_rr f.b ~dst:rax ~src:rax;
+      store_int f.b ~src:rax ~mm:(Frame a) ~size:8;
+      store_int f.b ~src:rax ~mm:(Frame c) ~size:8;
+      load_loc f ~reg:rax ln n.Tast.ty;
+      store_int f.b ~src:rax ~mm:(Frame b) ~size:8;
+      cmp_imm f.b ~dst:rax 0;
+      let ok = new_label f "inb" in
+      jcc_lbl f.b ~cc:cc_ge ok;
+      bounds_call f "flan_slice_error" e.Tast.loc [ a; b; c ];
+      lbl f.b ok);
     load_loc f ~reg:rax lp p.Tast.ty;
     store_int f.b ~src:rax ~mm:(lmem f dst ~scratch:r11) ~size:8;
     load_loc f ~reg:rax ln n.Tast.ty;
diff --git a/runtime/flan_dev.c b/runtime/flan_dev.c
index f283211..f21b519 100644
--- a/runtime/flan_dev.c
+++ b/runtime/flan_dev.c
@@ -221,9 +221,16 @@ void flan_dev_emit_i64(int64_t x) {
   emit_cstr(buf);
 }
 
+/* Unsigned NaN, for flan_f64_to_bytes's reason and one of its own: the REPL
+ * and println must not disagree about what a value looks like, which is the
+ * rule the escape table below is already held to. A NaN's sign bit is decided
+ * by whether the value was folded or computed, so showing it makes the printed
+ * form depend on the backend and the optimisation level rather than on the
+ * number. */
 void flan_dev_emit_f64(double x) {
   char buf[64];
-  snprintf(buf, sizeof buf, "%g", x);
+  if (x != x) snprintf(buf, sizeof buf, "nan");
+  else snprintf(buf, sizeof buf, "%g", x);
   emit_cstr(buf);
 }
 
@@ -532,9 +539,12 @@ void flan_dev_watch_emit_u64(uint64_t x) {
   watch_cstr(buf);
 }
 
+/* Unsigned NaN, the same rule [flan_dev_emit_f64] states: a watch row and a
+ * REPL answer for one value must read the same. */
 void flan_dev_watch_emit_f64(double x) {
   char buf[64];
-  snprintf(buf, sizeof buf, "%g", x);
+  if (x != x) snprintf(buf, sizeof buf, "nan");
+  else snprintf(buf, sizeof buf, "%g", x);
   watch_cstr(buf);
 }
 
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index 75ac84d..d25f34c 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -281,11 +281,21 @@ static int64_t fit(int n) {
  * here. Below was not, and it was the real one: a slice's length is a signed
  * 64-bit count, (slice s 2 1) computes 2 - 1 - 2 = -1, and `(size_t)n` on a
  * negative n is 18446744073709551615, which is not less than 511, so k became
- * 511 and the memcpy read 511 bytes from wherever the slice pointed. A checked
- * build traps on the reversed slice before it gets here; an unchecked one does
- * not, and every other (ptr, len) entry point in this file — flan_write_stdout,
- * flan_escape_bytes, flan_dev_emit — already guards the negative case. These
- * two were the exceptions. */
+ * 511 and the memcpy read 511 bytes from wherever the slice pointed. Every
+ * other (ptr, len) entry point in this file — flan_write_stdout,
+ * flan_escape_bytes, flan_dev_emit — already guarded the negative case. These
+ * two were the exceptions.
+ *
+ * It is worth saying why this stays now that (slice s 2 1) traps in every
+ * build and not only in a checked one. This clamp was written when it did not:
+ * lo <= hi sat behind --no-bounds-checks in both backends, so a release build
+ * handed a length of -1 straight to these functions, and the clamp was the
+ * last thing between that and a 511-byte read. check_slice no longer lets the
+ * value out, which makes the negative case unreachable *from Flan* — and not
+ * from here, because these take a raw (ptr, len) pair and the FFI, a C caller
+ * and slice-from-ptr's promise all reach them too. A function that is correct
+ * on its own arguments does not become incorrect because its callers improved,
+ * and two branches are not the price to argue about. */
 static size_t clamp_len(int64_t n, size_t cap) {
   if (n <= 0) return 0;
   return (uint64_t)n < (uint64_t)cap ? (size_t)n : cap;
@@ -308,9 +318,31 @@ int64_t flan_bytes_to_i64(const uint8_t *p, int64_t n) {
 }
 
 /* %g so that 3.5 prints as "3.5" and not "3.500000" — calc-me's expected
- * output is a table of exact strings. */
+ * output is a table of exact strings.
+ *
+ * NaN is rendered by hand, and the reason is that %g renders the *sign bit* of
+ * something that does not have a sign. glibc prints "-nan" when the bit is set
+ * and "nan" when it is not, and which one a program gets is decided by things
+ * no source line chose: LLVM's constant folder answers (/ 0.0 0.0) with a
+ * positive quiet NaN at compile time, divsd on this machine answers the same
+ * expression with the negative one at run time, so the same two-line program
+ * printed "nan" through one backend and "-nan" through the other. Neither is
+ * wrong about the arithmetic — IEEE 754 does not specify the sign of a NaN any
+ * operation produces — which is exactly what makes it the wrong thing to show.
+ *
+ * Reporting it unsigned is not a new rule here either: format-f64 in the
+ * prelude has always answered "nan" for the same value, because it reaches the
+ * case with (not (= x x)) and has no sign bit in its hands at all. So a build
+ * where (print x) said "-nan" and (show x 2) said "nan" was already disagreeing
+ * with itself about one value inside one backend. This makes print agree with
+ * show first and the two backends agree second.
+ *
+ * The test is x != x rather than isnan, which keeps math.h out of this file
+ * and is the same comparison the prelude uses. An infinity still prints signed:
+ * there the sign is the value. */
 void flan_f64_to_bytes(double x, uint8_t *buf, flan_slice *out) {
-  int n = snprintf((char *)buf, FLAN_NUM_BYTES, "%g", x);
+  int n = (x != x) ? snprintf((char *)buf, FLAN_NUM_BYTES, "nan")
+                   : snprintf((char *)buf, FLAN_NUM_BYTES, "%g", x);
   out->ptr = buf;
   out->len = fit(n);
 }
diff --git a/spike/x86/p11-reversed-slice.flan b/spike/x86/p11-reversed-slice.flan
new file mode 100644
index 0000000..d276d4e
--- /dev/null
+++ b/spike/x86/p11-reversed-slice.flan
@@ -0,0 +1,26 @@
+;;;; A slice built backwards, for the survey rather than for a person.
+;;;;
+;;;; test/programs/bounds.flan already covers this, and cannot cover it here:
+;;;; it picks its case out of (at args 1) and survey.sh runs every program
+;;;; with no arguments at all. So the one backend comparison that would catch
+;;;; check_slice's lo <= hi being re-gated on --no-bounds-checks is a program
+;;;; that reaches the reversed slice on its own.
+;;;;
+;;;; What it pins is that both backends die here in *every* build. lo <= hi is
+;;;; not a bounds check — it is the claim that the length word of the %slice
+;;;; this expression builds is a count, and hi - lo is -1 — so
+;;;; --no-bounds-checks has nothing here to drop, and running this sweep with
+;;;; SURVEY_FLAGS=--no-bounds-checks must report the same MATCH as without it.
+;;;; A backend that quietly builds the slice exits 0 while the other exits 134
+;;;; and the survey says DIFFER.
+;;;;
+;;;; The two ends come from (len args), which is 1 for a program run with no
+;;;; arguments and is not a number either optimiser can see, so the branch
+;;;; cannot be folded away and the checker has no literal to object to.
+(defn main [args [string]] i32
+  (let [s (bytes "hello")
+        hi (i32 (len args))
+        lo (+ hi 1)]
+    (print (slice s lo hi))
+    (println ""))
+  0)
diff --git a/test/programs/bounds.flan b/test/programs/bounds.flan
index def7bdd..228c519 100644
--- a/test/programs/bounds.flan
+++ b/test/programs/bounds.flan
@@ -1,6 +1,14 @@
 ;;;; Bounds checks, NEXT.md item 2. One program, one case per argument, so a
 ;;;; trap is observable: the checked build exits 134 with the source location
-;;;; on stderr, the unchecked one runs off the end and is not asserted on.
+;;;; on stderr.
+;;;;
+;;;; The unchecked build is not uniform, and the split is the point. An index
+;;;; past the end runs off the end there and is not asserted on — that is what
+;;;; --no-bounds-checks buys. Two of the cases below still trap: the reversed
+;;;; range at n = 2 and the negative promise at n = -2, because neither is a
+;;;; bounds check. Both are the claim that a slice's length word is a count,
+;;;; and a build that drops them does not produce an unchecked slice, it
+;;;; produces a value that is not one. See check_slice in lib/emit.ml.
 ;;;;
 ;;;; The selector is also the index wherever it can be, which is what keeps the
 ;;;; index dynamic — a literal would let the checker reject it outright one day
diff --git a/test/programs/format.flan b/test/programs/format.flan
index cfe4f53..4fac218 100644
--- a/test/programs/format.flan
+++ b/test/programs/format.flan
@@ -61,6 +61,20 @@
   (show (/ 1.0 0.0) 2)                  ; inf
   (show (/ -1.0 0.0) 2)                 ; -inf
 
+  ;; The same three through print, which goes to the runtime's %g rather than
+  ;; to format-f64, and the first of them is here for a reason the other two
+  ;; are not. A NaN carries a sign bit that no arithmetic chose: LLVM folds
+  ;; (/ 0.0 0.0) at compile time and answers the positive one, divsd answers
+  ;; the negative one at run time, and "%g" prints the difference. So this
+  ;; line printed "nan" through one backend and "-nan" through the other for
+  ;; the same source, and disagreed with the (show ...) above it inside either
+  ;; one. flan_f64_to_bytes now renders any NaN unsigned, which is what
+  ;; format-f64 always did. An infinity still prints signed: there the sign is
+  ;; the value, and both backends were always agreed about it.
+  (print (/ 0.0 0.0)) (println "")      ; nan
+  (print (/ 1.0 0.0)) (println "")      ; inf
+  (print (/ -1.0 0.0)) (println "")     ; -inf
+
   ;; Past 9e18 an f64 has no fractional bits and the integer part does not fit
   ;; in an i64, so this falls back to %g rather than approximating.
   (show 1e20 2)                         ; 1e+20
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 48df08c..d3a0ac4 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -719,7 +719,9 @@ let () =
        1.005\n1.0001\n7.000000\n\
        -0.50\n-0.00\n0.00\n0.00\n\
        2\n1.500000000\n\
-       nan\ninf\n-inf\n1e+20\n1234567890123.00\n\
+       nan\ninf\n-inf\n\
+       nan\ninf\n-inf\n\
+       1e+20\n1234567890123.00\n\
        fps 59.9 / frame 0.0167\n"
     in
     outputs "a number with a precision" "programs/format.flan" format_out;
@@ -1531,10 +1533,17 @@ let () =
     bounds ();
     bounds ~opt:"-O0" ();
 
-    (* The release build drops them — the calls, that is; the two declarations
-       stay in the header and LLVM discards the unused ones. Asserted on the IR
-       rather than by running an unchecked out-of-bounds program, which has no
-       defined behaviour to assert on. *)
+    (* What the release build drops, and what it does not. Asserted on the IR
+       for the first half, because an index past the end has no defined
+       behaviour to run and assert on; the second half is asserted by running
+       the program, below, because it does.
+
+       The line: @flan_bounds_error is the bounds check and goes. The two slice
+       calls stay, because what survives behind them is not a bounds check —
+       check_slice's lo <= hi and slice-from-ptr's n >= 0 are the claim that a
+       %slice's length word holds a count. This assertion is written as
+       "present" and not merely as "no longer looked at", so that re-gating
+       either one on f.md.checks fails here rather than passing quietly. *)
     let p =
       Reader.read_file "programs/bounds.flan" |> Parse.program |> Check.program
     in
@@ -1543,12 +1552,54 @@ let () =
       print_endline "FAIL  checks on: no bounds call emitted"
     end;
     let off = Emit.program ~checks:false p in
-    if contains off "call void @flan_bounds_error("
-       || contains off "call void @flan_slice_error("
-       || contains off "call void @flan_slice_promise_error(" then begin
+    if contains off "call void @flan_bounds_error(" then begin
       incr failures;
-      print_endline "FAIL  --no-bounds-checks: a check survived"
+      print_endline "FAIL  --no-bounds-checks: a bounds check survived"
     end;
+    if not (contains off "call void @flan_slice_error(") then begin
+      incr failures;
+      print_endline "FAIL  --no-bounds-checks: the lo <= hi invariant went too"
+    end;
+    if not (contains off "call void @flan_slice_promise_error(") then begin
+      incr failures;
+      print_endline "FAIL  --no-bounds-checks: the n >= 0 invariant went too"
+    end;
+
+    (* And the same thing as behaviour rather than as text. A slice built
+       backwards writes hi - lo into a length word that every reader takes for
+       a count, so the value it produces is not a slice with its bounds check
+       removed — it is not a slice. The same for a promise of -2 elements.
+       Both must still die, with the same sentence, in a build that asked for
+       no bounds checks at all.
+
+       The in-bounds selector is run too, and it is the other half of the
+       claim: the flag still buys something, and a program that slices
+       correctly does not start paying for a check it was promised was gone.
+
+       This is the one place the two halves can be told apart, and it is worth
+       one compile. *)
+    let unchecked = compile ~checks:false "programs/bounds.flan" in
+    let still_traps name arg reason =
+      let code, text = run unchecked (Some arg) in
+      if code <> 134 || not (contains text reason) then begin
+        incr failures;
+        Printf.printf
+          "FAIL  %s under --no-bounds-checks\n        got: %S (exit %d)\n\
+          \     wanted: %S (exit 134)\n"
+          name text code reason
+      end
+    in
+    still_traps "reversed slice" "2" "slice [2 1) is out of bounds for length 5";
+    still_traps "slice-from-ptr with a negative length" "-2"
+      "slice-from-ptr was promised -2 elements behind the pointer";
+    let code, text = run unchecked (Some "0") in
+    if text <> "0ello\n" || code <> 0 then begin
+      incr failures;
+      Printf.printf
+        "FAIL  in-bounds edges under --no-bounds-checks\n        got: %S (exit %d)\n"
+        text code
+    end;
+    (try Sys.remove unchecked with Sys_error _ -> ());
 
     (* The other half of the same change: a bad index that something *answers*.
        bounds.flan above is still the unhandled case and still exits 134 with
diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml
index 3405f17..a3f2dfc 100644
--- a/test/test_sanitize.ml
+++ b/test/test_sanitize.ml
@@ -230,11 +230,16 @@ let unchecked_controls () =
       "9",  "at -O2 the load is folded away — an out-of-bounds inbounds GEP \
              into a string constant is poison, so nothing is read and a wrong \
              value is printed. Reported at -O0.";
-      "2",  "a reversed slice (lo 2, hi 1), whose length comes out negative; \
-             nothing is read, and flan_write_stdout ignores a negative count. \
-             No access, so nothing for ASan to see — the hazard is a slice \
-             with a negative length reaching user code, which is a checker \
-             question" ]
+      "2",  "a reversed slice (lo 2, hi 1), which this build traps on before \
+             anything is read. It is in this list rather than out of it \
+             because it used to be here for the opposite reason: the length \
+             came out negative, nothing was read, and ASan had nothing to \
+             see, which made a slice with a negative length reaching user \
+             code a checker question and not a sanitizer one. The checker \
+             answered it — lo <= hi is a representation invariant and no \
+             longer sits behind --no-bounds-checks — so ASan is still silent \
+             here and now for a better reason. The trap itself is asserted in \
+             test_acceptance.ml" ]
   in
   match compile ~sanitize:true ~checks:false "programs/bounds.flan" with
   | exception Failure m -> fail "unchecked bounds.flan: build: %s" m
diff --git a/test/test_valgrind.ml b/test/test_valgrind.ml
index 3577948..2d646ef 100644
--- a/test/test_valgrind.ml
+++ b/test/test_valgrind.ml
@@ -261,11 +261,14 @@ let corpus =
 
    It is a subset and not the whole corpus because --no-bounds-checks turns
    out to remove much less than its name suggests, and that is worth writing
-   down: [check_at] and [check_slice] in emit.ml are behind the flag, but a
-   Vec's and a Map's bounds checks are not — they live inside flan_vec_at and
-   the map probe in flan_rt.c, are plain C, and run in every build. So the
-   flag lowers the guard on fixed arrays and slices only. These are the
-   programs where that distinction reaches heap storage. *)
+   down: [check_at] is behind the flag and so is *half* of [check_slice] — the
+   [hi <= len] compare — while its [lo <= hi] stays, because that one is the
+   claim that a slice's length word is a count and not a bounds check at all.
+   A Vec's and a Map's bounds checks are not behind it either: they live inside
+   flan_vec_at and the map probe in flan_rt.c, are plain C, and run in every
+   build. So the flag lowers the guard on indexing a fixed array or a slice,
+   and on nothing else. These are the programs where that distinction reaches
+   heap storage. *)
 let unchecked_subset =
   [ "programs/allocators.flan", [];
     "programs/edn.flan", [];