diff --git a/README.ko.md b/README.ko.md
index 9c5434c..b6996a8 100644
--- a/README.ko.md
+++ b/README.ko.md
@@ -63,8 +63,9 @@ Windows x64에 툴체인을 고정한 상태입니다.
 `no_std` + `extern "C"` Rust를 내보내고 이를 `cargo` cdylib으로 빌드합니다.
 
 **현재 언어.** 타입은 `f64`, `bool`, `i32`, `string` 네 가지입니다. 수치 타입에는 산술(`+`, `-`,
-`*`, `/`, 그리고 `i32`의 `%`)과 비교, 그리고 명시적 `as` 변환이 있습니다. `i32`의 나눗셈은
-전역(total)이라 `x / 0`은 트랩이 아니라 `0`입니다. `string`은 **파라미터**나 **`-> string!` 반환**에
+`*`, `/`, 그리고 `i32`의 `%`)과 비교, 그리고 명시적 `as` 변환이 있습니다. `i32`를 0으로
+나누면 트랩이 아니라 `0`이고, 실패 가능(`-> T!`) 함수 안에서 `i32` 결과가 넘치면 wrap하지 않고
+예약 status로 실패합니다. `string`은 **파라미터**나 **`-> string!` 반환**에
 쓸 수 있고, 연산은 `==`·`!=`(바이트 비교)와 **연결 `+`** 입니다 — 연결 결과는 모듈에 할당자가 없어
 `return` 자리에만 놓을 수 있습니다. `i32 as string`으로 숫자를 렌더링합니다. 반환은 **호스트가 준
 버퍼**에 씁니다 — 모듈은 할당하지 않습니다. 배열 파라미터는 `xs: [i32]`로 씁니다(원소는 `i32`·`f64`·`bool`).
diff --git a/README.md b/README.md
index 8e47f5d..a762c42 100644
--- a/README.md
+++ b/README.md
@@ -64,7 +64,9 @@ backend emits `no_std`, `extern "C"` Rust and builds it as a `cargo` cdylib.
 
 **The language today.** Four types: `f64`, `bool`, `i32` and `string`. The numeric ones come
 with arithmetic (`+`, `-`, `*`, `/`, and `%` on `i32`), comparisons, and an explicit `as`
-conversion between them; `i32` division is total, so `x / 0` is `0` rather than a trap.
+conversion between them; `i32` division by zero gives `0` rather than a trap, and inside a
+fallible (`-> T!`) function an `i32` result that overflows fails with a reserved status instead
+of wrapping.
 A `string` can be a parameter or a `-> string!` return; it compares with `==` and `!=` on
 bytes, and concatenates with `+` — which only a `return` may hold, since the module has no
 allocator. `i32 as string` renders a number. Returning a string uses a caller-allocated
diff --git a/compiler/src/abi.rs b/compiler/src/abi.rs
index 2a85508..4c5314f 100644
--- a/compiler/src/abi.rs
+++ b/compiler/src/abi.rs
@@ -28,6 +28,13 @@ pub const ML_ST_INSUFFICIENT_BUFFER: i32 = -1;
 
 pub const ML_ST_INDEX_OUT_OF_RANGE: i32 = -2;
 
+/// An i32 result — or an `f64 as i32` value — does not exist: the operation overflowed, or the
+/// f64 was NaN or truncates outside i32. Returned only from FALLIBLE bodies
+/// (`SPEC-checked-arithmetic`); an infallible body has no status channel and keeps wrapping.
+/// Its own value rather than `-2`, so a host can tell "outside an array" from "no such value"
+/// (DP-O3).
+pub const ML_ST_OVERFLOW: i32 = -3;
+
 /// Longest module name the compiler accepts, in ASCII characters.
 ///
 /// The module name is not just a file stem: it becomes the crate name, the C header guard,
diff --git a/compiler/src/codegen.rs b/compiler/src/codegen.rs
index 689b5c7..44e9001 100644
--- a/compiler/src/codegen.rs
+++ b/compiler/src/codegen.rs
@@ -755,6 +755,19 @@ fn emit_stmt(s: &IrStmt, indent: usize, abi: RetAbi, out: &mut String) {
     }
 }
 
+/// How a FALLIBLE body leaves when an i32 operation or `f64 as i32` has no value
+/// (`SPEC-checked-arithmetic`), or `None` for an infallible body — which has no status channel
+/// and keeps wrapping and saturating (DP-O1). The same per-shape choice the `Index` arm makes.
+fn overflow_bail(abi: RetAbi) -> Option<String> {
+    match abi {
+        RetAbi::Fallible => Some(format!("return Err({});", crate::abi::ML_ST_OVERFLOW)),
+        RetAbi::StringOut | RetAbi::ArrayOut(_) => {
+            Some(format!("return {};", crate::abi::ML_ST_OVERFLOW))
+        }
+        RetAbi::Plain => None,
+    }
+}
+
 fn emit_expr(e: &IrExpr, abi: RetAbi) -> String {
     match &e.kind {
         // `xs[i]`, bounds-checked (SPEC-array-input 2.3).
@@ -874,6 +887,18 @@ fn emit_expr(e: &IrExpr, abi: RetAbi) -> String {
             // exactly the semantics the SPEC pins. That agreement is why this lowering is one
             // line; it is NOT the reason the semantics were chosen, and a C backend must
             // implement them by hand (C casts are UB out of range).
+            // In a fallible body `f64 as i32` fails where there is no i32 value: NaN, or a value
+            // that truncates outside i32 (SPEC-checked-arithmetic §2.1). The open interval
+            // (-2147483649, 2147483648) is exactly what truncation toward zero keeps in range,
+            // and NaN fails both comparisons.
+            if *to == IrType::I32 && operand.ty == IrType::F64 {
+                if let Some(bail) = overflow_bail(abi) {
+                    return format!(
+                        "{{ let __c = {}; if !(__c > -2147483649.0f64 && __c < 2147483648.0f64) {{ {bail} }} __c as i32 }}",
+                        emit_expr(operand, abi)
+                    );
+                }
+            }
             format!("({} as {})", emit_expr(operand, abi), rust_type(*to))
         }
         IrExprKind::Unary { op, operand } => {
@@ -893,6 +918,13 @@ fn emit_expr(e: &IrExpr, abi: RetAbi) -> String {
             // i32::MIN`"), and Rust's plain `-` only wraps while `overflow-checks` is off.
             // Same reasoning as the `wrapping_*` arms below: put the rule in the code.
             if matches!(op, IrUnOp::Neg) && operand.ty == IrType::I32 {
+                // Checked in a fallible body: `-i32::MIN` has no value (SPEC-checked-arithmetic).
+                if let Some(bail) = overflow_bail(abi) {
+                    return format!(
+                        "(match ({}).checked_neg() {{ Some(__o) => __o, None => {{ {bail} }} }})",
+                        emit_expr(operand, abi)
+                    );
+                }
                 return format!("({}).wrapping_neg()", emit_expr(operand, abi));
             }
             let sym = match op {
@@ -940,6 +972,19 @@ fn emit_expr(e: &IrExpr, abi: RetAbi) -> String {
             //
             // DP-N4 is untouched: a zero divisor still yields the defined `0i32`.
             if matches!(op, IrBinOp::Div | IrBinOp::Rem) && lhs.ty == IrType::I32 {
+                // In a fallible body the one quotient with no value — `i32::MIN / -1`, 2^31 —
+                // fails (SPEC-checked-arithmetic). `%` does not: `i32::MIN % -1` is 0, which
+                // exists (DP-O5), so the remainder keeps the template below. Operands are still
+                // bound left to right before anything is tested.
+                if matches!(op, IrBinOp::Div) {
+                    if let Some(bail) = overflow_bail(abi) {
+                        return format!(
+                            "{{ let __l = {}; let __d = {}; if __d == 0 {{ 0i32 }} else if __d == -1 && __l == i32::MIN {{ {bail} }} else {{ __l.wrapping_div(__d) }} }}",
+                            emit_expr(lhs, abi),
+                            emit_expr(rhs, abi)
+                        );
+                    }
+                }
                 let method = if matches!(op, IrBinOp::Div) {
                     "wrapping_div"
                 } else {
@@ -986,6 +1031,17 @@ fn emit_expr(e: &IrExpr, abi: RetAbi) -> String {
                     | IrBinOp::And
                     | IrBinOp::Or => None,
                 } {
+                    // Checked in a fallible body (SPEC-checked-arithmetic): the same receiver-
+                    // first evaluation, and no value becomes the reserved status instead of a
+                    // wrapped number.
+                    if let Some(bail) = overflow_bail(abi) {
+                        let checked = method.replace("wrapping_", "checked_");
+                        return format!(
+                            "(match ({}).{checked}({}) {{ Some(__o) => __o, None => {{ {bail} }} }})",
+                            emit_expr(lhs, abi),
+                            emit_expr(rhs, abi)
+                        );
+                    }
                     return format!(
                         "({}).{method}({})",
                         emit_expr(lhs, abi),
diff --git a/compiler/src/header.rs b/compiler/src/header.rs
index a322955..d9c113a 100644
--- a/compiler/src/header.rs
+++ b/compiler/src/header.rs
@@ -143,6 +143,16 @@ fn can_report_out_of_range(module: &IrModule) -> bool {
         .any(|f| crate::ir::can_fail_out_of_range(&f.body))
 }
 
+/// Can any FALLIBLE function in this module answer `ML_ST_OVERFLOW`? One predicate for both
+/// bindings, for the reason [`can_report_out_of_range`] gives. Infallible bodies are not asked:
+/// they keep wrapping and have no status to report it with (SPEC-checked-arithmetic DP-O1).
+fn can_report_overflow(module: &IrModule) -> bool {
+    module
+        .functions
+        .iter()
+        .any(|f| f.fallible && crate::ir::can_fail_overflow(&f.body))
+}
+
 /// Does this module RETURN any byte outside ASCII?
 ///
 /// Delegates to [`crate::ir::returns_non_ascii_bytes`], which is where it moved when the
@@ -341,6 +351,20 @@ pub fn emit_c_header(module: &IrModule, dll_name: &str) -> String {
         );
         let _ = writeln!(s, "#endif");
     }
+    if can_report_overflow(module) {
+        let _ = writeln!(
+            s,
+            "/* A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value \
+             (overflow,"
+        );
+        let _ = writeln!(
+            s,
+            " * or NaN). The out-parameter is NOT written (D17); calling again gives the same answer. */"
+        );
+        let _ = writeln!(s, "#ifndef ML_ST_OVERFLOW");
+        let _ = writeln!(s, "#define ML_ST_OVERFLOW ({})", crate::abi::ML_ST_OVERFLOW);
+        let _ = writeln!(s, "#endif");
+    }
     // D17 error codes (module-defined, positive i32). Constants — not exported symbols.
     if !module.errors.is_empty() {
         for e in &module.errors {
@@ -823,6 +847,14 @@ pub fn emit_delphi_unit(module: &IrModule, dll_name: &str) -> String {
             crate::abi::ML_ST_INDEX_OUT_OF_RANGE
         );
     }
+    if can_report_overflow(module) {
+        let _ = writeln!(
+            s,
+            "  {{ A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value\n    \
+             (overflow, or NaN). The out-parameter is NOT written (D17). }}"
+        );
+        let _ = writeln!(s, "  ML_ST_OVERFLOW = {};", crate::abi::ML_ST_OVERFLOW);
+    }
     s.push('\n');
     let _ = writeln!(
         s,
diff --git a/compiler/src/ir.rs b/compiler/src/ir.rs
index 0d10175..80f762b 100644
--- a/compiler/src/ir.rs
+++ b/compiler/src/ir.rs
@@ -557,6 +557,66 @@ pub fn can_fail_out_of_range(body: &[IrStmt]) -> bool {
     })
 }
 
+/// Can this body return `ML_ST_OVERFLOW` — does it hold a checked operation?
+///
+/// `SPEC-checked-arithmetic` §2.1: i32 `+ - * /` and unary `-`, and `f64 as i32`. `%` is not
+/// here (DP-O5 — `i32::MIN % -1` is 0, which exists). The caller asks only about FALLIBLE
+/// bodies: an infallible one lowers the same operators wrapping. Exhaustive over the IR for
+/// the reason [`can_fail_out_of_range`] is — a gate that asks a narrower question lets a
+/// module return a status its bindings never name (#238).
+pub fn can_fail_overflow(body: &[IrStmt]) -> bool {
+    fn in_expr(e: &IrExpr) -> bool {
+        match &e.kind {
+            IrExprKind::Binary { op, lhs, rhs } => {
+                let checked = lhs.ty == IrType::I32
+                    && match op {
+                        IrBinOp::Add | IrBinOp::Sub | IrBinOp::Mul | IrBinOp::Div => true,
+                        IrBinOp::Rem
+                        | IrBinOp::Lt
+                        | IrBinOp::Gt
+                        | IrBinOp::Le
+                        | IrBinOp::Ge
+                        | IrBinOp::Eq
+                        | IrBinOp::Ne
+                        | IrBinOp::And
+                        | IrBinOp::Or => false,
+                    };
+                checked || in_expr(lhs) || in_expr(rhs)
+            }
+            IrExprKind::Unary { op, operand } => {
+                (matches!(op, IrUnOp::Neg) && operand.ty == IrType::I32) || in_expr(operand)
+            }
+            IrExprKind::Cast { to, operand } => {
+                (*to == IrType::I32 && operand.ty == IrType::F64) || in_expr(operand)
+            }
+            IrExprKind::ByteLen(operand) => in_expr(operand),
+            IrExprKind::Index { index, .. } => in_expr(index),
+            IrExprKind::ByteSlice { s, from, to } => in_expr(s) || in_expr(from) || in_expr(to),
+            IrExprKind::Fixed { x, places } => in_expr(x) || in_expr(places),
+            IrExprKind::Call { args, .. } | IrExprKind::Concat(args) => args.iter().any(in_expr),
+            IrExprKind::Len { .. }
+            | IrExprKind::ConstF64(_)
+            | IrExprKind::ConstStr(_)
+            | IrExprKind::ConstI32(_)
+            | IrExprKind::ConstBool(_)
+            | IrExprKind::Var(_) => false,
+        }
+    }
+    body.iter().any(|s| match s {
+        IrStmt::If { cond, body } | IrStmt::While { cond, body } => {
+            in_expr(cond) || can_fail_overflow(body)
+        }
+        IrStmt::ResultSet { index, value } => in_expr(index) || in_expr(value),
+        IrStmt::ResultLen(e)
+        | IrStmt::Return(e)
+        | IrStmt::Let { value: e, .. }
+        | IrStmt::Assign { value: e, .. }
+        | IrStmt::AssignOut { value: e, .. } => in_expr(e),
+        IrStmt::TryCall { args, .. } => args.iter().any(in_expr),
+        IrStmt::Fail(_) => false,
+    })
+}
+
 /// Does this body compare a span anywhere? — `SPEC-string-slice-compare` DP-C2.
 ///
 /// The companion to [`first_index`], and it exists for the same stated reason: `check_expr`
diff --git a/compiler/tests/bindings.rs b/compiler/tests/bindings.rs
index a851a02..c6b8e13 100644
--- a/compiler/tests/bindings.rs
+++ b/compiler/tests/bindings.rs
@@ -47,7 +47,8 @@ fn delphi_unit_matches_module_abi() {
 
 /// **Every conditional block in both binding generators, both branches, one table.**
 ///
-/// `header.rs` decides **eleven** things by inspecting the module, and the count is the first
+/// `header.rs` decides **twelve** things by inspecting the module — eleven when this test was
+/// written; `ML_ST_OVERFLOW` (`SPEC-checked-arithmetic`) is the twelfth — and the count is the first
 /// thing this test got wrong: the first draft said eight, covered seven of them, and claimed
 /// to cover all. Review counted again. The `.pas` has its own copies of both status constants
 /// under their own conditions, and the UTF-8 notice is two emissions, not one.
@@ -86,6 +87,7 @@ fn each_conditional_binding_block_fires_for_exactly_the_shapes_that_need_it() {
     const H_Q12_ARR: &str = "Q12 for an ARRAY return";
     const H_INSUF: &str = "ML_ST_INSUFFICIENT_BUFFER";
     const H_OOR: &str = "ML_ST_INDEX_OUT_OF_RANGE";
+    const H_OVF: &str = "#define ML_ST_OVERFLOW";
     const H_UTF8: &str = "UTF-8";
     // The error-constant block. Module-level (`!module.errors.is_empty()`), so it belongs in
     // this matrix — the first draft of the comment below called it per-function and was wrong.
@@ -111,15 +113,16 @@ fn each_conditional_binding_block_fires_for_exactly_the_shapes_that_need_it() {
         "ML_ST_INDEX_OUT_OF_RANGE = {};",
         mlc::abi::ML_ST_INDEX_OUT_OF_RANGE
     );
-    let (pas_insuf, pas_oor) = (p_insuf.as_str(), p_oor.as_str());
+    let p_ovf = format!("ML_ST_OVERFLOW = {};", mlc::abi::ML_ST_OVERFLOW);
+    let (pas_insuf, pas_oor, pas_ovf) = (p_insuf.as_str(), p_oor.as_str(), p_ovf.as_str());
     // Nested inside the `returns_str || returns_array` block: only an ARRAY return gets it.
     const P_ELEMENTS: &str = "count ELEMENTS, not bytes, so the";
     const P_UTF8: &str = "UTF-8";
     const P_ERR: &str = "ML_M_ERR_E_BAD";
 
-    let all = [H_Q12_STR, H_Q12_ARR, H_INSUF, H_OOR, H_UTF8, H_ERR];
+    let all = [H_Q12_STR, H_Q12_ARR, H_INSUF, H_OOR, H_OVF, H_UTF8, H_ERR];
     let all_pas = [
-        P_ARR_RET, P_ARR_PAR, P_UNICODE, pas_insuf, pas_oor, P_ELEMENTS, P_UTF8, P_ERR,
+        P_ARR_RET, P_ARR_PAR, P_UNICODE, pas_insuf, pas_oor, pas_ovf, P_ELEMENTS, P_UTF8, P_ERR,
     ];
 
     let cases: &[(&str, &str, &[&str], &[&str])] = &[
@@ -191,6 +194,15 @@ fn each_conditional_binding_block_fires_for_exactly_the_shapes_that_need_it() {
             &[H_ERR],
             &[P_ERR],
         ),
+        // i32 arithmetic in a FALLIBLE body can have no i32 value, so the overflow status is
+        // declared. Every other row does arithmetic on nothing, on f64, or in no fallible body,
+        // and carries the absent half; which operators count is `checked_arithmetic.rs`'s table.
+        (
+            "checked arithmetic",
+            "export fn f(a: i32) -> i32! { return a + 1 }",
+            &[H_OVF],
+            &[pas_ovf],
+        ),
         // A string parameter with a scalar return: only the Delphi note, because only Delphi
         // has a way to get this wrong silently (measured 2026-09-10, DP-S2).
         (
diff --git a/compiler/tests/checked_arithmetic.rs b/compiler/tests/checked_arithmetic.rs
new file mode 100644
index 0000000..9b083ff
--- /dev/null
+++ b/compiler/tests/checked_arithmetic.rs
@@ -0,0 +1,68 @@
+//! Checked i32 arithmetic in fallible bodies — what the bindings promise (`SPEC-checked-arithmetic`).
+//!
+//! The values live in `hosts/rust-oracle/tests/checked_arithmetic.rs`. What is here is decided
+//! without loading a module: which modules declare `ML_ST_OVERFLOW` (§2.5 — exactly those
+//! that can return it, one predicate for both bindings), and that the fingerprint does not
+//! move (DP-O4).
+
+use mlc::compile_to_ir;
+use mlc::header::{emit_c_header, emit_delphi_unit};
+use mlc::iface::fingerprint;
+
+fn declares(src: &str) -> (bool, bool) {
+    let ir = compile_to_ir(src).expect("compile");
+    let h = emit_c_header(&ir, "m");
+    let pas = emit_delphi_unit(&ir, "m");
+    (
+        h.contains("#define ML_ST_OVERFLOW (-3)"),
+        pas.contains("ML_ST_OVERFLOW = -3;"),
+    )
+}
+
+/// **§2.5: the status is declared exactly where it can be returned — and both bindings agree.**
+#[test]
+fn only_a_module_that_can_overflow_declares_the_status() {
+    for (src, can) in [
+        // Every checked operation, each in a fallible body.
+        ("export fn f(a: i32, b: i32) -> i32! { return a + b }", true),
+        ("export fn f(a: i32, b: i32) -> i32! { return a - b }", true),
+        ("export fn f(a: i32, b: i32) -> i32! { return a * b }", true),
+        ("export fn f(a: i32) -> i32! { return -a }", true),
+        ("export fn f(a: i32, b: i32) -> i32! { return a / b }", true),
+        ("export fn f(x: f64) -> i32! { return x as i32 }", true),
+        // The other two fallible shapes.
+        ("export fn f(a: i32) -> string! { return (a * 2) as string }", true),
+        (
+            "export fn f(a: i32) -> [i32]! {\n  result 1\n  result[0] = a * 2\n}",
+            true,
+        ),
+        // An internal fallible helper counts: it is a fallible body too.
+        (
+            "fn h(a: i32) -> i32! { return a * 2 }\nexport fn f(a: i32) -> i32! { let x = try h(a)  return x }",
+            true,
+        ),
+        // Not checked: infallible bodies, `%` (DP-O5), f64 arithmetic, widening casts.
+        ("export fn f(a: i32, b: i32) -> i32 { return a * b }", false),
+        ("export fn f(a: i32, b: i32) -> i32! { return a % b }", false),
+        ("export fn f(x: f64, y: f64) -> f64! { return x * y }", false),
+        ("export fn f(a: i32) -> f64! { return a as f64 }", false),
+        ("error E = 1\nexport fn f(a: i32) -> i32! { if a < 0 { fail E }  return a }", false),
+    ] {
+        let (h, pas) = declares(src);
+        assert_eq!(h, pas, "the header and the unit disagree about {src:?}");
+        assert_eq!(h, can, "{src:?} declares ML_ST_OVERFLOW: {h}, expected {can}");
+    }
+}
+
+/// **DP-O4: the fingerprint does not see which reserved negatives a body reaches.**
+///
+/// The same signature with and without an overflowing operation has one fingerprint — the
+/// manifest records signatures and error codes, and a reserved status is the ABI's (D17).
+#[test]
+fn checking_arithmetic_does_not_move_the_fingerprint() {
+    let fp = |src: &str| fingerprint(&compile_to_ir(src).expect("compile"));
+    assert_eq!(
+        fp("export fn f(a: i32) -> i32! { return a }"),
+        fp("export fn f(a: i32) -> i32! { return a * 2 }"),
+    );
+}
diff --git a/compiler/tests/golden/generated.rs.txt b/compiler/tests/golden/generated.rs.txt
index 0f5e846..be5045f 100644
--- a/compiler/tests/golden/generated.rs.txt
+++ b/compiler/tests/golden/generated.rs.txt
@@ -202,7 +202,7 @@ fn ml_fn_masked(acct: *const u8, ml_buf: *mut u8, ml_cap: i32, ml_needed: *mut i
     let __l0 = ml_sublen(__s0, __f0, __t0);
     if __l0 < 0 { return -2; }
     let __s2 = acct;
-    let __f2 = (ml_slen(acct)).wrapping_sub(4i32);
+    let __f2 = (match (ml_slen(acct)).checked_sub(4i32) { Some(__o) => __o, None => { return -3; } });
     let __t2 = ml_slen(acct);
     let __l2 = ml_sublen(__s2, __f2, __t2);
     if __l2 < 0 { return -2; }
@@ -301,8 +301,8 @@ fn ml_fn_allocate(stock: *const i32, stock_len: i32, want: i32, ml_buf: *mut i32
             if __i < 0 || __i >= __n { return -2; }
             unsafe { *ml_buf.add(__i as usize) = take; }
         }
-        left = (left).wrapping_sub(take);
-        i = (i).wrapping_add(1i32);
+        left = (match (left).checked_sub(take) { Some(__o) => __o, None => { return -3; } });
+        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return -3; } });
     }
     0
 }
@@ -328,7 +328,7 @@ fn ml_fn_in_stock(stock: *const i32, stock_len: i32, ml_buf: *mut bool, ml_cap:
             if __i < 0 || __i >= __n { return -2; }
             unsafe { *ml_buf.add(__i as usize) = ({ let __i = i; if __i < 0 || __i >= stock_len { return -2; } unsafe { *stock.add(__i as usize) } } > 0i32); }
         }
-        i = (i).wrapping_add(1i32);
+        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return -3; } });
     }
     0
 }
@@ -360,14 +360,14 @@ fn ml_fn_basket_total(qty: *const i32, qty_len: i32, price: *const i32, price_le
     let mut total = 0i32;
     let mut i = 0i32;
     while (i < qty_len) {
-        let line = ({ let __i = i; if __i < 0 || __i >= qty_len { return Err(-2); } unsafe { *qty.add(__i as usize) } }).wrapping_mul({ let __i = i; if __i < 0 || __i >= price_len { return Err(-2); } unsafe { *price.add(__i as usize) } });
+        let line = (match ({ let __i = i; if __i < 0 || __i >= qty_len { return Err(-2); } unsafe { *qty.add(__i as usize) } }).checked_mul({ let __i = i; if __i < 0 || __i >= price_len { return Err(-2); } unsafe { *price.add(__i as usize) } }) { Some(__o) => __o, None => { return Err(-3); } });
         if (line > cap) {
-            total = (total).wrapping_add(cap);
+            total = (match (total).checked_add(cap) { Some(__o) => __o, None => { return Err(-3); } });
         }
         if (line <= cap) {
-            total = (total).wrapping_add(line);
+            total = (match (total).checked_add(line) { Some(__o) => __o, None => { return Err(-3); } });
         }
-        i = (i).wrapping_add(1i32);
+        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return Err(-3); } });
     }
     return Ok(total);
 }
@@ -383,7 +383,7 @@ fn ml_fn_largest(xs: *const f64, xs_len: i32, floor: f64) -> Result<f64, i32> {
         if ({ let __i = i; if __i < 0 || __i >= xs_len { return Err(-2); } unsafe { *xs.add(__i as usize) } } > best) {
             best = { let __i = i; if __i < 0 || __i >= xs_len { return Err(-2); } unsafe { *xs.add(__i as usize) } };
         }
-        i = (i).wrapping_add(1i32);
+        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return Err(-3); } });
     }
     return Ok(best);
 }
@@ -406,7 +406,7 @@ fn ml_fn_any_set(flags: *const bool, flags_len: i32) -> Result<bool, i32> {
         if { let __i = i; if __i < 0 || __i >= flags_len { return Err(-2); } unsafe { *flags.add(__i as usize) } } {
             return Ok(true);
         }
-        i = (i).wrapping_add(1i32);
+        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return Err(-3); } });
     }
     return Ok(false);
 }
@@ -1352,7 +1352,7 @@ fn ml_fn_replay(start: i32, events: *const i32, events_len: i32) -> Result<i32,
     let mut i = 0i32;
     while (i < events_len) {
         s = match ml_fn_next_state(s, { let __i = i; if __i < 0 || __i >= events_len { return Err(-2); } unsafe { *events.add(__i as usize) } }) { Ok(__v) => __v, Err(__e) => return Err(__e) };
-        i = (i).wrapping_add(1i32);
+        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return Err(-3); } });
     }
     return Ok(s);
 }
@@ -1432,7 +1432,7 @@ fn ml_fn_boxes_checked(qty: i32, per_box: i32) -> Result<i32, i32> {
     if (per_box == 0i32) {
         return Err(1);
     }
-    return Ok({ let __l = qty; let __d = per_box; if __d == 0 { 0i32 } else { __l.wrapping_div(__d) } });
+    return Ok({ let __l = qty; let __d = per_box; if __d == 0 { 0i32 } else if __d == -1 && __l == i32::MIN { return Err(-3); } else { __l.wrapping_div(__d) } });
 }
 #[no_mangle]
 pub extern "C" fn mlx_boxes_checked(qty: i32, per_box: i32, out_value: *mut i32) -> i32 {
@@ -1626,7 +1626,7 @@ fn ml_fn_receipt_line(item: *const u8, qty: i32, unit_price: i32, ml_buf: *mut u
     let __p1 = b" x \0".as_ptr();
     let __p2 = qty;
     let __p3 = b" = \0".as_ptr();
-    let __p4 = (qty).wrapping_mul(unit_price);
+    let __p4 = (match (qty).checked_mul(unit_price) { Some(__o) => __o, None => { return -3; } });
     let mut __n: i32 = 1;
     __n += ml_slen(__p0);
     __n += ml_slen(__p1);
@@ -1782,9 +1782,9 @@ fn ml_fn_schedule(principal: i32, months: i32, ml_buf: *mut i32, ml_cap: i32, ml
         {
             let __i = i;
             if __i < 0 || __i >= __n { return -2; }
-            unsafe { *ml_buf.add(__i as usize) = { let __l = principal; let __d = months; if __d == 0 { 0i32 } else { __l.wrapping_div(__d) } }; }
+            unsafe { *ml_buf.add(__i as usize) = { let __l = principal; let __d = months; if __d == 0 { 0i32 } else if __d == -1 && __l == i32::MIN { return -3; } else { __l.wrapping_div(__d) } }; }
         }
-        i = (i).wrapping_add(1i32);
+        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return -3; } });
     }
     0
 }
@@ -1802,9 +1802,9 @@ fn ml_fn_one_payment(principal: i32, months: i32, month: i32) -> Result<i32, i32
     if (month >= months) {
         return Err(1);
     }
-    let base = { let __l = principal; let __d = months; if __d == 0 { 0i32 } else { __l.wrapping_div(__d) } };
+    let base = { let __l = principal; let __d = months; if __d == 0 { 0i32 } else if __d == -1 && __l == i32::MIN { return Err(-3); } else { __l.wrapping_div(__d) } };
     if (month == 0i32) {
-        return Ok((base).wrapping_add({ let __l = principal; let __d = months; if __d == 0 { 0i32 } else { __l.wrapping_rem(__d) } }));
+        return Ok((match (base).checked_add({ let __l = principal; let __d = months; if __d == 0 { 0i32 } else { __l.wrapping_rem(__d) } }) { Some(__o) => __o, None => { return Err(-3); } }));
     }
     return Ok(base);
 }
@@ -1889,7 +1889,7 @@ fn ml_fn_bump(n: i32) -> Result<i32, i32> {
     if (n < 0i32) {
         return Err(1);
     }
-    return Ok((n).wrapping_sub(7i32));
+    return Ok((match (n).checked_sub(7i32) { Some(__o) => __o, None => { return Err(-3); } }));
 }
 #[no_mangle]
 pub extern "C" fn mlx_bump(n: i32, out_value: *mut i32) -> i32 {
@@ -1937,7 +1937,7 @@ fn ml_fn_grade(n: i32, tier: *mut i32) -> Result<i32, i32> {
         return Err(1);
     }
     unsafe { *tier = 1i32; }
-    return Ok((n).wrapping_mul(10i32));
+    return Ok((match (n).checked_mul(10i32) { Some(__o) => __o, None => { return Err(-3); } }));
 }
 #[no_mangle]
 pub extern "C" fn mlx_grade(n: i32, tier: *mut i32, out_value: *mut i32) -> i32 {
diff --git a/compiler/tests/golden/headers.h.txt b/compiler/tests/golden/headers.h.txt
index 7a1eae8..f9608ef 100644
--- a/compiler/tests/golden/headers.h.txt
+++ b/compiler/tests/golden/headers.h.txt
@@ -44,6 +44,11 @@
 #ifndef ML_ST_INDEX_OUT_OF_RANGE
 #define ML_ST_INDEX_OUT_OF_RANGE (-2)
 #endif
+/* A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value (overflow,
+ * or NaN). The out-parameter is NOT written (D17); calling again gives the same answer. */
+#ifndef ML_ST_OVERFLOW
+#define ML_ST_OVERFLOW (-3)
+#endif
 #define ML_ACCOUNT_ERR_E_SHORT_ACCOUNT 1
 
 #ifdef __cplusplus
@@ -159,6 +164,11 @@ int32_t mlx_add(int32_t /* a */, int32_t /* b */);
 #ifndef ML_ST_INDEX_OUT_OF_RANGE
 #define ML_ST_INDEX_OUT_OF_RANGE (-2)
 #endif
+/* A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value (overflow,
+ * or NaN). The out-parameter is NOT written (D17); calling again gives the same answer. */
+#ifndef ML_ST_OVERFLOW
+#define ML_ST_OVERFLOW (-3)
+#endif
 #ifdef __cplusplus
 extern "C" {
 #endif
@@ -212,6 +222,11 @@ int32_t mlx_in_stock(const int32_t* /* stock */, int32_t /* stock_len */, bool*
 #ifndef ML_ST_INDEX_OUT_OF_RANGE
 #define ML_ST_INDEX_OUT_OF_RANGE (-2)
 #endif
+/* A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value (overflow,
+ * or NaN). The out-parameter is NOT written (D17); calling again gives the same answer. */
+#ifndef ML_ST_OVERFLOW
+#define ML_ST_OVERFLOW (-3)
+#endif
 #define ML_BASKET_ERR_E_LENGTH_MISMATCH 1
 
 #ifdef __cplusplus
@@ -889,6 +904,11 @@ int32_t mlx_negate_if(int32_t /* x */, bool /* flip */);
 #ifndef ML_ST_INDEX_OUT_OF_RANGE
 #define ML_ST_INDEX_OUT_OF_RANGE (-2)
 #endif
+/* A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value (overflow,
+ * or NaN). The out-parameter is NOT written (D17); calling again gives the same answer. */
+#ifndef ML_ST_OVERFLOW
+#define ML_ST_OVERFLOW (-3)
+#endif
 #define ML_ORDER_ERR_E_BAD_TRANSITION 1
 #define ML_ORDER_ERR_E_UNKNOWN_STATE 2
 
@@ -955,6 +975,11 @@ int32_t mlx_state_label(int32_t /* state */, char* ml_buf, int32_t ml_cap, int32
  * type, parameter order, out-ness or error code does. */
 #define ML_PACK_IFACE_HASH 0xDA0077B3A04515ABULL
 
+/* A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value (overflow,
+ * or NaN). The out-parameter is NOT written (D17); calling again gives the same answer. */
+#ifndef ML_ST_OVERFLOW
+#define ML_ST_OVERFLOW (-3)
+#endif
 #define ML_PACK_ERR_E_EMPTY_BOX 1
 
 #ifdef __cplusplus
@@ -1064,6 +1089,11 @@ int32_t mlx_line_check(int32_t /* qty */, int32_t* /* tier */, int32_t* out_valu
 #define ML_ST_INSUFFICIENT_BUFFER (-1)
 #endif
 
+/* A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value (overflow,
+ * or NaN). The out-parameter is NOT written (D17); calling again gives the same answer. */
+#ifndef ML_ST_OVERFLOW
+#define ML_ST_OVERFLOW (-3)
+#endif
 #define ML_RECEIPT_ERR_E_NO_ITEMS 1
 
 #ifdef __cplusplus
@@ -1231,6 +1261,11 @@ int32_t mlx_safe_div(double /* a */, double /* b */, double* out_value);
 #ifndef ML_ST_INDEX_OUT_OF_RANGE
 #define ML_ST_INDEX_OUT_OF_RANGE (-2)
 #endif
+/* A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value (overflow,
+ * or NaN). The out-parameter is NOT written (D17); calling again gives the same answer. */
+#ifndef ML_ST_OVERFLOW
+#define ML_ST_OVERFLOW (-3)
+#endif
 #define ML_SCHEDULE_ERR_E_BAD_TERM 1
 
 #ifdef __cplusplus
@@ -1289,6 +1324,11 @@ int32_t mlx_one_payment(int32_t /* principal */, int32_t /* months */, int32_t /
 #define ML_ST_INSUFFICIENT_BUFFER (-1)
 #endif
 
+/* A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value (overflow,
+ * or NaN). The out-parameter is NOT written (D17); calling again gives the same answer. */
+#ifndef ML_ST_OVERFLOW
+#define ML_ST_OVERFLOW (-3)
+#endif
 #define ML_SHAPES_ERR_E_NEG 1
 #define ML_SHAPES_ERR_E_ODD 2
 
diff --git a/compiler/tests/golden/units.pas.txt b/compiler/tests/golden/units.pas.txt
index 6e51cf0..da5ee80 100644
--- a/compiler/tests/golden/units.pas.txt
+++ b/compiler/tests/golden/units.pas.txt
@@ -52,6 +52,9 @@ const
   { An index outside 0..len, or a span outside the string. The out-parameter is
     NOT written (D17), and the length is the one YOU passed alongside the pointer. }
   ML_ST_INDEX_OUT_OF_RANGE = -2;
+  { A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value
+    (overflow, or NaN). The out-parameter is NOT written (D17). }
+  ML_ST_OVERFLOW = -3;
 
 function ml_module_abi_version: LongWord; cdecl; external ML_MODULE;
 function ml_iface_hash_account: UInt64; cdecl; external ML_MODULE;
@@ -144,6 +147,9 @@ const
   { An index outside 0..len, or a span outside the string. The out-parameter is
     NOT written (D17), and the length is the one YOU passed alongside the pointer. }
   ML_ST_INDEX_OUT_OF_RANGE = -2;
+  { A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value
+    (overflow, or NaN). The out-parameter is NOT written (D17). }
+  ML_ST_OVERFLOW = -3;
 
 function ml_module_abi_version: LongWord; cdecl; external ML_MODULE;
 function ml_iface_hash_allocate: UInt64; cdecl; external ML_MODULE;
@@ -194,6 +200,9 @@ const
   { An index outside 0..len, or a span outside the string. The out-parameter is
     NOT written (D17), and the length is the one YOU passed alongside the pointer. }
   ML_ST_INDEX_OUT_OF_RANGE = -2;
+  { A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value
+    (overflow, or NaN). The out-parameter is NOT written (D17). }
+  ML_ST_OVERFLOW = -3;
 
 function ml_module_abi_version: LongWord; cdecl; external ML_MODULE;
 function ml_iface_hash_basket: UInt64; cdecl; external ML_MODULE;
@@ -687,6 +696,9 @@ const
   { An index outside 0..len, or a span outside the string. The out-parameter is
     NOT written (D17), and the length is the one YOU passed alongside the pointer. }
   ML_ST_INDEX_OUT_OF_RANGE = -2;
+  { A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value
+    (overflow, or NaN). The out-parameter is NOT written (D17). }
+  ML_ST_OVERFLOW = -3;
 
 function ml_module_abi_version: LongWord; cdecl; external ML_MODULE;
 function ml_iface_hash_order: UInt64; cdecl; external ML_MODULE;
@@ -719,6 +731,9 @@ const
   ML_MODULE = 'pack.dll';
   ML_PACK_IFACE_HASH: UInt64 = UInt64($DA0077B3A04515AB);
   ML_PACK_ERR_E_EMPTY_BOX = 1;
+  { A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value
+    (overflow, or NaN). The out-parameter is NOT written (D17). }
+  ML_ST_OVERFLOW = -3;
 
 function ml_module_abi_version: LongWord; cdecl; external ML_MODULE;
 function ml_iface_hash_pack: UInt64; cdecl; external ML_MODULE;
@@ -810,6 +825,9 @@ const
     NUL included. Truncation is a FAILURE, not a short success - nothing is written,
     and ml_needed is the exact size to allocate, in the same unit as ml_cap. }
   ML_ST_INSUFFICIENT_BUFFER = -1;
+  { A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value
+    (overflow, or NaN). The out-parameter is NOT written (D17). }
+  ML_ST_OVERFLOW = -3;
 
 function ml_module_abi_version: LongWord; cdecl; external ML_MODULE;
 function ml_iface_hash_receipt: UInt64; cdecl; external ML_MODULE;
@@ -917,6 +935,9 @@ const
   { An index outside 0..len, or a span outside the string. The out-parameter is
     NOT written (D17), and the length is the one YOU passed alongside the pointer. }
   ML_ST_INDEX_OUT_OF_RANGE = -2;
+  { A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value
+    (overflow, or NaN). The out-parameter is NOT written (D17). }
+  ML_ST_OVERFLOW = -3;
 
 function ml_module_abi_version: LongWord; cdecl; external ML_MODULE;
 function ml_iface_hash_schedule: UInt64; cdecl; external ML_MODULE;
@@ -979,6 +1000,9 @@ const
     NUL included. Truncation is a FAILURE, not a short success - nothing is written,
     and ml_needed is the exact size to allocate, in the same unit as ml_cap. }
   ML_ST_INSUFFICIENT_BUFFER = -1;
+  { A fallible function's i32 arithmetic or f64-to-i32 conversion has no i32 value
+    (overflow, or NaN). The out-parameter is NOT written (D17). }
+  ML_ST_OVERFLOW = -3;
 
 function ml_module_abi_version: LongWord; cdecl; external ML_MODULE;
 function ml_iface_hash_shapes: UInt64; cdecl; external ML_MODULE;
diff --git a/compiler/tests/language_gaps.rs b/compiler/tests/language_gaps.rs
index 88d3fdc..828361f 100644
--- a/compiler/tests/language_gaps.rs
+++ b/compiler/tests/language_gaps.rs
@@ -208,9 +208,6 @@ fn conversions_that_do_not_exist_yet() {
         "i32 as bool",
         "export fn f(a: i32) -> bool { return a as bool }",
     );
-    // 체크드 오버플로 is in the same bullet and is deliberately NOT here: it is a property of
-    // arithmetic, not a construct one can write, so there is no source text to reject.
-    // `-i32::MIN == i32::MIN` is measured in unary.rs instead.
 }
 
 // ------------------------------------------------------------------ data and declarations
@@ -260,10 +257,6 @@ fn data_shapes_that_do_not_exist_yet() {
 ///
 /// The right column is not decoration: it is checked against the actual call sites below, so
 /// a row cannot name a case that does not exist.
-///
-/// One item of the block is deliberately absent — 체크드 오버플로. It is a property of
-/// arithmetic rather than a construct, so there is no source text to reject; see
-/// `conversions_that_do_not_exist_yet`.
 const GAPS: &[(&str, &str)] = &[
     // 부분문자열은 더 이상 공백이 아니다 — `byte_slice(s, from, to)`가 2026-09-13에 들어왔다.
     // 대신 **범위 문법**이 공백이고, 그것이 `s[0..3]`을 거부하는 진짜 이유다. `byte_len`이
diff --git a/docs/HOST_ABI.md b/docs/HOST_ABI.md
index ac56a94..2b6ef43 100644
--- a/docs/HOST_ABI.md
+++ b/docs/HOST_ABI.md
@@ -53,6 +53,10 @@
   호스트가 들을 자리가 없다. **호스트 규칙: 받은 `double`을 쓰기 전에 유한한지 본다**
   (C는 `isfinite`, Delphi는 `Math.IsNan`/`IsInfinite`). 모듈 저자가 `!`와 `raw != raw`로
   막을 수도 있지만 **그것은 저자의 선택이지 ABI의 보장이 아니다.**
+- **`!` 함수의 i32 산술과 `f64 as i32`는 값이 없으면 `ML_ST_OVERFLOW`(`-3`)로 실패한다**
+  (`SPEC-checked-arithmetic`) — `+ - *`, 단항 `-`, `i32::MIN / -1`, 그리고 NaN이거나 절단 뒤 i32
+  밖인 변환. **무한 함수는 그대로 wrap·포화한다** — status 채널이 없다. 생성 `.h`·`.pas`는 그
+  상수를 **낼 수 있는 모듈에만** 선언한다. `-3`도 절단이 아니다(아래 Q12 표).
 - 마샬링은 **스칼라와 문자열**: `f64`/`bool`/`i32`, 그리고 아래에 적은 범위의 `string`.
   (이 줄은 "스칼라만"이었다 — 바로 아래 두 줄이 문자열 입력과 반환을 구현됐다고 적는 동안
   그대로 남아 있었다. 한 불릿이 자기 자신과 모순됐다.) 실패 가능 함수는 D17대로
@@ -232,7 +236,7 @@ int32_t mlx_carrier_name(const char* scac, char* ml_buf, int32_t ml_cap, int32_t
 |---|---|---|---|
 | `0` | 성공 | 채워짐(NUL 종료) | 쓴 길이 |
 | **`ML_ST_INSUFFICIENT_BUFFER`(`-1`)** | **용량 부족 — 절단** | **건드리지 않음**(실측: 64B canary 전부 보존) | **필요한 길이** |
-| **그 밖의 예약 음수** (오늘 `ML_ST_INDEX_OUT_OF_RANGE` = `-2`) | **절단이 아니다** — 경계 검사 실패 | **정의되지 않음** | **정의되지 않음** |
+| **그 밖의 예약 음수** (오늘 `ML_ST_INDEX_OUT_OF_RANGE` = `-2`, `ML_ST_OVERFLOW` = `-3`) | **절단이 아니다** — 경계 검사 실패, 또는 i32 값이 없음 | **정의되지 않음** | **정의되지 않음** |
 | 양수 | 모듈 정의 도메인 에러(D17) | 건드리지 않음 | 건드리지 않음 |
 
 > ⚠ **음수를 한 줄로 읽지 마라 — 그것이 이 표가 2026-09-22까지 틀려 있던 방식이다.**
@@ -243,7 +247,8 @@ int32_t mlx_carrier_name(const char* scac, char* ml_buf, int32_t ml_cap, int32_t
 >
 > **재시도 조건은 `status < 0`이 아니라 `status == ML_ST_INSUFFICIENT_BUFFER`다.** `-2`에
 > `ml_cap = *ml_needed`로 다시 부르면 **같은 답이 온다**(실측: `status = -2`, `needed = 2`가 몇 번을
-> 불러도 그대로) — 수렴하지 않는 루프다.
+> 불러도 그대로) — 수렴하지 않는 루프다. `-3`도 같다(실측: `result` 뒤에 넘친 배열 반환이 두 번
+> 불러도 `-3`, `checked_arithmetic.rs`).
 >
 > **두 반환 형태에서 `-2`일 때의 사정이 다르다**(둘 다 "읽지 마라"로 귀결되지만, 왜 다른지는
 > 알아 둘 값이 있다): `-> string!`은 경계 검사가 쓰기보다 **먼저** 돌아 `buf`도 `*needed`도
diff --git a/docs/LANGUAGE.md b/docs/LANGUAGE.md
index c2e0ca2..4b7e498 100644
--- a/docs/LANGUAGE.md
+++ b/docs/LANGUAGE.md
@@ -114,7 +114,8 @@
   대입할 수 없다. `const`는 최상위에서만 뜻을 가져 `fn const()`는 여전히 합법이다
 - `if cond { … }` — **`else` 없음**
 - `while cond { … }` — 반복. `break`/`continue`는 아직 없다(함수 탈출은 `return`)
-- **단항 연산자** `-e`(f64/i32) · `!e`(bool). `-`의 오버플로는 wrap — `-i32::MIN == i32::MIN`(측정)
+- **단항 연산자** `-e`(f64/i32) · `!e`(bool). `-i32::MIN`은 `!` 본문에서 **`ML_ST_OVERFLOW`(`-3`)**,
+  무한 함수에서 wrap(`-i32::MIN == i32::MIN`) — 둘 다 측정, 규칙은 아래 `+ - *` 항목과 같다
 - **논리 연산자** `a && b` · `a || b` — 양쪽 `bool`, 결과 `bool`. `&&`가 `||`보다 강하게 결합하고
   둘 다 비교보다 느슨하다. **단락 평가한다 — 명세이자 실측이다**(2026-09-13): 범위 밖 인덱스가
   식 자리에서 `ML_ST_INDEX_OUT_OF_RANGE`를 내므로, `false && xs[99] > 0`이 **status `0`** 을
@@ -134,16 +135,27 @@
 - **지역 변수** `let NAME = EXPR` — 블록 스코프, 타입 추론, 기본 **불변**
 - **가변 지역 변수** `let mut NAME = EXPR` + **대입문** `NAME = EXPR` — 대입 대상은 `let mut` 지역만
   (파라미터·불변 `let` 거부). 대입은 **문**이지 식이 아니다(`a = b = c` 불가)
-- 식: 리터럴, 파라미터·지역 변수 참조, `+ - * / %`, 비교. **`i32`의 `/`·`%`는 전역(total)**이다 —
-  **제수가 런타임에 0이면**(`x / y`에서 `y == 0`) 결과는 `0`이고 `x % y`도 `0`이며
-  `i32::MIN / -1`은 wrap이다(전부 측정). `%`는 i32 전용.
+- 식: 리터럴, 파라미터·지역 변수 참조, `+ - * / %`, 비교. **`i32`의 `/`·`%`는 0 제수에서 트랩하지
+  않는다** — **제수가 런타임에 0이면**(`x / y`에서 `y == 0`) 결과는 `0`이고 `x % y`도 `0`이다.
+  `i32::MIN / -1`은 참 몫 2^31이 i32 밖이라 `!` 본문에서 **`-3`**, 무한 함수에서 wrap이고,
+  `i32::MIN % -1`은 참 나머지 `0`이 i32 안이라 어디서나 `0`이다(전부 측정). `%`는 i32 전용.
   **제수를 리터럴 `0`으로 쓰면**(`x / 0`) 컴파일 에러다 — 런타임 규약과 다른 층이고, 리터럴은
   언제나 실수이기 때문이다
-- **`i32`의 `+`·`-`·`*`는 오버플로에서 wrap한다** — `2000000000 + 2000000000 = -294967296`,
-  `i32::MAX + 1 = i32::MIN`(로드된 모듈에서 측정, `i32_type.rs`). **포화가 아니다**, 그리고
-  그 구분이 이 줄의 이유다: 같은 언어의 **`f64 as i32`는 포화한다**(아래 "명시적 변환"), 그래서
-  *"i32는 clamp한다"* 로 배운 저자가 산술에서 틀린다. **조용하다** — 무한 함수에는 호스트가
-  들을 채널이 없다(D17은 `!`가 붙은 함수에만 status를 준다).
+- **`i32`의 `+`·`-`·`*`가 넘치면 — 연산자가 아니라 본문이 정한다**(SPEC-checked-arithmetic):
+  - **`!` 함수 본문에서는 `ML_ST_OVERFLOW`(`-3`)로 실패한다.** 다른 실패와 같이 호스트는 out을
+    읽지 않는다(D17 DP-E3).
+    `i32::MAX + 1`, `46341 * 46341`, `i32::MIN - 1`이 `-3`이고 경계 바로 안쪽은 정확한 값이다
+    (로드된 모듈에서 측정, `checked_arithmetic.rs`). 이 status를 낼 수 있는 모듈의 `.h`·`.pas`가
+    그 이름을 선언한다. `result` 뒤에 나면 버퍼는 `-2`와 같이 정의되지 않는다(`HOST_ABI.md`).
+  - **무한 함수 본문에서는 wrap한다** — `2000000000 + 2000000000 = -294967296`,
+    `i32::MAX + 1 = i32::MIN`(측정, `i32_type.rs`). **포화가 아니다**: 같은 언어의 `f64 as i32`는
+    무한 함수에서 **포화한다**(아래 "명시적 변환"), 그래서 *"i32는 clamp한다"* 로 배운 저자가
+    산술에서 틀린다. **조용하다** — 무한 함수에는 호스트가 들을 채널이 없다(D17).
+  - **같은 `a * b`가 시그니처에 따라 다르게 동작한다.** `!` 함수가 부른 **무한 헬퍼** 안의 산술도
+    wrap한다 — 의도한 wrap을 쓰는 방법이 그것이다(DP-O7). 리터럴만의 오버플로(`2147483647 + 1`)는
+    컴파일 에러가 아니라 **실행 시 `-3`**이다(DP-O9). 참값이 i32에 드는데 중간값만 넘쳐도
+    실패한다(`a * 2 / 2`가 `a = 2^30`에서 `-3`, 측정) — 정답을 주는 것은 `i64`뿐이고, 그것은
+    아래 공백 블록에 있다.
 - **`f64`의 `/`는 전역이 아니다 — `inf`·`NaN`이 그대로 호스트로 간다**(2026-09-16 실측,
   `STATUS.md` §9-61). 바로 위 두 항목이 `i32`에 대해 말하는 것과 **반대**이고, 그 대비가 이 줄의
   이유다. 로드된 모듈에서 잰 값:
@@ -159,6 +171,7 @@
 
   마지막 두 줄이 위험하다: 변환 자체는 **기록된 규칙대로**인데(위 "명시적 변환"), 그 결과가
   **그럴듯한 숫자**라 호스트가 구분할 수 없다. 그리고 `-> f64`·`-> i32`에는 status 채널이 없다.
+  표의 값은 **무한 함수**의 것이다 — `!` 본문에서는 마지막 두 식이 **`-3`**이다(측정).
 
   ⚠ **리터럴도 다르다 — 그리고 그것은 의도다.** `i32`에서 **제수를 리터럴 `0`으로 쓰면**
   (`x / 0`) **컴파일 에러**인데(위 항목 — 런타임에 0이 들어오는 쪽은 `0`을 돌려준다),
@@ -174,10 +187,10 @@
   **저자가 막는 방법은 있다**: `if raw != raw { fail … }`가 컴파일되고 동작한다(실측 — NaN이면
   status 1, 아니면 값). 함수를 `!`로 선언해야 한다. **이 줄이 생기기 전에는 그래야 한다는 것을
   말하는 곳이 없었다.**
-  wrap은 사고가 아니라 **결정**이다: `no_std` cdylib의 `#[panic_handler]`가 `loop {}`라
-  오버플로 패닉은 호스트를 **죽이는 것이 아니라 멈춘다**(§5-4). 그래서 codegen이 셋을
-  `wrapping_add`/`wrapping_sub`/`wrapping_mul`로 **명시적·무조건** 낮춘다 — 프로파일 설정에
-  기대지 않는다. 체크드 산술을 원하면 그것은 별도 슬라이스다(아래 공백 목록)
+  wrap도 체크드도 **패닉이 아니다** — 그것이 결정이다: `no_std` cdylib의 `#[panic_handler]`가
+  `loop {}`라 오버플로 패닉은 호스트를 **죽이는 것이 아니라 멈춘다**(§5-4). 그래서 codegen이 무한
+  본문에서는 `wrapping_add`/`_sub`/`_mul`을, `!` 본문에서는 `checked_*`와 `-3` 반환을 **명시적으로**
+  방출한다 — 어느 쪽도 프로파일 설정에 기대지 않는다
 - **이름 제약**: **파라미터와 지역 변수** 이름은 `ml_`·`mlx_`·`__`로 시작할 수 없다(#101 이후
   **함수 이름에는 이 제약이 없다** — 함수는 `ml_fn_<이름>`으로 방출되어 생성 식별자와 겹치지 않는다.
   `fn match`·`fn type`처럼 대상 언어의 예약어도 이제 함수 이름으로 쓸 수 있다).
@@ -253,7 +266,9 @@
 - **명시적 변환** `e as f64` / `e as i32`. 단항보다 **느슨하게**, `*`·`/`보다 **강하게** 결합한다
   (Rust·C#·Kotlin과 같다) — `-x as f64`는 `(-x) as f64`이고, 옛 의미는 `-(x as f64)`로 쓴다.
   암시적 혼합은 여전히 금지(DP-I2).
-  `f64 as i32`는 **0 방향 절단 + 포화, NaN→0**(측정된 언어 규칙 — 대상 언어의 캐스트에 위임하지 않는다)
+  `f64 as i32`는 **0 방향 절단 + 포화, NaN→0**(측정된 언어 규칙 — 대상 언어의 캐스트에 위임하지 않는다).
+  **`!` 본문에서는** NaN이거나 절단 뒤 i32 밖이면 **`-3`**이다 — `2147483647.9`는 `i32::MAX`,
+  `2147483648.0`·무한은 `-3`(측정)
 
 아직 아님 — **⏳ 미구현** (위 "포함" 목록 중). **언어 표면의 공백은 전부 이 블록에 있다**:
 
@@ -288,9 +303,7 @@
   **지역 배열·배열 리터럴**(작업 배열) — 넷 다 우회는 된다(곱셈 루프 · 두 줄 내부 `fn` · 파라미터로
   받기). `min`/`max`와 수학 함수는 키워드가 아니라 **아직 없는 내장 시그니처**다
 - 복합 대입(`+= -= *=`) — `=`만 구현됨
-- `f64` 나머지(`%`는 i32 전용 — SPEC-i32-division DP-D4), **체크드 오버플로**, `bool` 변환
-  (체크드가 없다는 것이 *"무슨 일이 일어나는지 모른다"* 는 뜻은 아니다 — **wrap이고 측정돼 있다**,
-  위 식 항목. 이 줄이 오래 "공백"이라고만 말하고 값은 어디에도 없었다)
+- `f64` 나머지(`%`는 i32 전용 — SPEC-i32-division DP-D4), `bool` 변환
 
 ## 내부 의미 모델 (Delphi 방식의 의미)
 
diff --git a/docs/STATUS.md b/docs/STATUS.md
index 04d614a..cabe78e 100644
--- a/docs/STATUS.md
+++ b/docs/STATUS.md
@@ -119,10 +119,12 @@
 않는다.
 
 **둘 다 측정된 적이 없고, 오늘은 측정할 수도 없다.** 지금 언어의 어떤 연산도 패닉에 도달하지 못하기
-때문이다: `f64` 0나눗셈은 `inf`, `as`는 포화, 정수 산술은 wrap — `compiler/src/codegen.rs`가 `i32`의
-`+ - *`에 `wrapping_add`/`_sub`/`_mul`을 **명시적으로 방출**하므로 프로필 설정과 무관하다
-(`-i32::MIN == i32::MIN`으로 **실측**됨 — SPEC-unary, §9-55.4) — 그리고 `i32`의 `/`·`%`는 **가드를 달아**
-방출된다(#76 — 제수가 0이면 0을 돌려주고 `i32::MIN / -1`은 `wrapping_div`로 간다).
+때문이다: `f64` 0나눗셈은 `inf`, 무한 함수에서 `as`는 포화하고 정수 산술은 wrap — `compiler/src/codegen.rs`가
+`i32`의 `+ - *`에 `wrapping_add`/`_sub`/`_mul`을 **명시적으로 방출**하므로 프로필 설정과 무관하다
+(`-i32::MIN == i32::MIN`으로 **실측**됨 — SPEC-unary, §9-55.4). `!` 본문에서는 둘 다 `checked_*`와 범위
+비교로 `ML_ST_OVERFLOW`(`-3`)를 **반환**한다 — 패닉이 아니다(SPEC-checked-arithmetic). 그리고 `i32`의 `/`·`%`는
+**가드를 달아** 방출된다(#76 — 제수가 0이면 0을 돌려주고, `i32::MIN / -1`은 무한 함수에서 `wrapping_div`로,
+`!` 본문에서 `-3`으로 간다).
 `#[panic_handler]`는 오늘 `no_std`를 만족시키려고 있을 뿐 **도달 불가능한 코드**다.
 따라서 위 서술의 근거 수준은 **E1(소스 판독 + Grok 교차확인)이며 E2가 아니다.**
 
@@ -231,8 +233,9 @@
 >
 > **▶ 다음 세션 — 여기서 시작한다.** 순서대로:
 >
-> 1. **체크드 정수 산술 SPEC 확인 — 사용자 결정.** 방향(A+as)은 확인받았다(2026-09-26). 초안은
->    `docs/slices/SPEC-checked-arithmetic.md`이고 §4의 DP-O3~O9가 확인을 기다린다. 확인되면 §6의 두 PR로 구현한다.
+> 1. **체크드 정수 산술 — 구현 중.** DP-O1~O9 전부 사용자 확인(2026-09-26). `docs/slices/SPEC-checked-arithmetic.md`
+>    §6의 작업 1(codegen·바인딩·오라클 값·문서)이 들어갔고, **작업 2가 남았다** — 실제 C 호스트가 `-3`을 받는 수용 D,
+>    §9-69의 161행 재측정, 크기 변화, 그리고 슬라이스 닫기.
 >    같은 날 인코딩 질문은 `OPEN_QUESTIONS.md` **Q17**로 올렸다(권고 (A) — 사용자 확인 대기).
 > 2. **작은 항목**: C# 호스트(Phase 4) · LSP(Phase 3, 큰 일).
 > 3. **외부**: `X1`·`X2` — Delphi가 있는 CI 러너. 이 저장소 안에서는 닫히지 않는다.
diff --git a/docs/slices/README.md b/docs/slices/README.md
index 776c2be..03b0d05 100644
--- a/docs/slices/README.md
+++ b/docs/slices/README.md
@@ -62,7 +62,7 @@ TDD 구현 → Grok 검증 → PR** 순서를 따른다(`CLAUDE.md` "개발 방
 | [고정 소수 포맷 `fixed(x, places)`](SPEC-fixed-decimals.md) | ✅ **구현 완료** (2026-09-15) | `fixed(x, places)` — 고정 소수 십진 표기. 모듈 안 우회가 조용히 틀리던 것(`1234.05` → `"1234.5"`)을 막는다 | §7 §9-53 / #243 |
 | [나눗셈 가드가 왼쪽 피연산자를 건너뛴다](SPEC-division-guard-operands.md) | ✅ **구현 완료** (2026-09-23) | 제수가 0이면 `/`·`%`의 왼쪽 피연산자(배열 경계 검사)가 실행되지 않던 결함 — 왼쪽을 먼저 묶어 평가한다 | #287 / #291 |
 | [상수 선언 `const` · `export const`](SPEC-constants.md) | ✅ **구현 완료** (2026-09-26) | 이름 붙은 리터럴 — `export const`만 헤더(`ML_<MODULE>_CONST_<NAME>`)와 지문에 나가, 번호를 바꾼 모듈을 게이트가 거부한다 | #325 / #326·#327 |
-| [체크드 정수 산술](SPEC-checked-arithmetic.md) | 🔨 **SPEC 초안 · 확인 대기** (2026-09-26) | `!` 본문의 i32 오버플로와 `f64 as i32`가 `-3`으로 실패한다 — 방향(A+as)은 확인받았고 하위 결정 DP-O3~O9가 남았다 | §9-69 / — |
+| [체크드 정수 산술](SPEC-checked-arithmetic.md) | 🔨 **확정 · 구현 중** (2026-09-26) | `!` 본문의 i32 오버플로와 `f64 as i32`가 `-3`으로 실패한다 — DP-O1~O9 사용자 확인, §6 작업 1이 들어갔고 작업 2(C 호스트 수용 D · 재측정)가 남았다 | §9-69 / — |
 
 > **2026-09-25에 행을 한 줄로 접었다.** 접기 전의 서술은 [`../history/slices-index.md`](../history/slices-index.md)에
 > 바이트 그대로 있다. **새 행도 한 줄로 쓴다** — 행당 400 B(`every_slice_index_row_is_one_line`)이고, 경위는 그
@@ -125,8 +125,8 @@ TDD 구현 → Grok 검증 → PR** 순서를 따른다(`CLAUDE.md` "개발 방
 두 번째 호스트(C#, ROADMAP Phase 4), 그리고 ROADMAP Phase 2가 이름만 두고 설계가 없던 둘 —
 **인터페이스 정의 파일**(설계부터)과 **개발/배포 빌드 분리**(D13, `SECURITY.md` P1).
 *(2026-09-25 로드맵 검토에서 더했다 — Phase 2의 다섯 항목 중 이 둘이 이 목록에 없었다.)*
-§7(§9-69, 12개 도메인 72규칙과 귀속 대조)이 더한 후보: **체크드 정수 산술**(가장 강한 근거 — 방향 A+as를 확인받아
-SPEC 초안이 있다, 위 색인), **i64**, **입력 문자열의 인코딩 계약**(닫힌 DP-S2의 재개 — 설계 질문, §9-69.3), 비트 연산자,
+§7(§9-69, 12개 도메인 72규칙과 귀속 대조)이 더한 후보: **체크드 정수 산술**(가장 강한 근거 — 확정되어
+구현 중이다, 위 색인), **i64**, **입력 문자열의 인코딩 계약**(닫힌 DP-S2의 재개 — 설계 질문, §9-69.3), 비트 연산자,
 지역 작업 배열, 수학 내장 함수, 문자 단위 길이.
 **struct는 §9-1이 강제되지 않는다고 결론냈다** — 고르려면 그 절을 먼저 읽는다(§9-69도 귀속 0으로 다시 확인했다).
 배열도 같은 결론이었고(§9-9가 다섯 번째로), **입력은 그 사실을 SPEC 첫 절에 적은 채로 열렸다**.
diff --git a/docs/slices/SPEC-checked-arithmetic.md b/docs/slices/SPEC-checked-arithmetic.md
index da59681..78ccd8b 100644
--- a/docs/slices/SPEC-checked-arithmetic.md
+++ b/docs/slices/SPEC-checked-arithmetic.md
@@ -1,8 +1,9 @@
 # SPEC — 체크드 정수 산술 (`!` 본문)
 
-- **상태: 초안. 사용자 확인 전이며 제품 코드는 한 줄도 쓰지 않았다.**
-  - **방향은 확인받았다(2026-09-26)**: 설계 **A+as** — `!` 함수 본문의 i32 산술과 `f64 as i32`가 넘치면
-    예약 음수 status로 실패한다(§9-69.2의 권장안). 이 문서가 묻는 것은 **§4의 하위 결정**이다.
+- **상태: 확정 · 구현 중.** §4의 DP-O1~O9 전부 **사용자 확인**(2026-09-26, 권고안 그대로). §6의 작업 1이
+  들어갔고 작업 2가 남았다.
+  - 방향은 먼저 확인받았다: 설계 **A+as** — `!` 함수 본문의 i32 산술과 `f64 as i32`가 넘치면
+    예약 음수 status로 실패한다(§9-69.2의 권장안).
 - 선행: `SPEC-i32.md`(DP-I4 — `+ - *` wrap) · `SPEC-unary.md`(DP-U4 — `-i32::MIN` wrap) ·
   `SPEC-i32-division.md`(D2 행 — `i32::MIN / -1` wrap) · `SPEC-numeric-conversion.md`(§2.3 — `f64 as i32` 포화·NaN→0) ·
   `SPEC-array-return.md`(DP-R9 — `result` 뒤의 실패) · `SPEC-fixed-decimals.md`(DP-M4 — `-2` 재사용 선례)
@@ -135,7 +136,9 @@ Rust의 `checked_rem`은 `i32::MIN % -1`에서 `None`을 준다(나눗셈이 넘
 
 ---
 
-## 4. 설계 결정 (확인 요청)
+## 4. 설계 결정
+
+DP-O1·O2는 방향 확인 때, DP-O3~O9는 이 표 그대로 **사용자 확인**을 받았다(2026-09-26).
 
 | DP | 결정 | 대안 | 근거 |
 |---|---|---|---|
@@ -161,9 +164,12 @@ Rust의 `checked_rem`은 `i32::MIN % -1`에서 `None`을 준다(나눗셈이 넘
 
 ---
 
-## 6. 작업 분해 (확인 후)
+## 6. 작업 분해
 
 | 작업 | 수용 | 크기 |
 |---|---|---|
-| 1. codegen(연산 넷 + 변환, 모양별 실패 방출) · `abi.rs` · `ir.rs` 술어 · `.h`/`.pas` 선언 · 골든 · 컴파일러 테스트 | A · B · C · D · F · G(텍스트) | 한 PR |
-| 2. 오라클 값 · C 호스트 수용 D · 문서 · §9-69의 161행 재측정 | A · D · E · G · H · I | 한 PR |
+| 1. codegen(연산 넷 + 변환, 모양별 실패 방출) · `abi.rs` · `ir.rs` 술어 · `.h`/`.pas` 선언 · 골든 · 컴파일러 테스트 · 오라클 값 · 문서 | A · B · C · D · F · G · H · E(선언) | 한 PR |
+| 2. 실제 C 호스트가 `-3`을 받는다(수용 D) · §9-69의 161행 재측정 · 크기 변화(§5) | E · I | 한 PR |
+
+오라클 값과 문서는 작업 2에서 1로 옮겼다 — 작업 1이 머지되는 순간 `LANGUAGE.md`의 wrap 문단과
+`HOST_ABI.md` 표가 거짓이 되므로 같은 PR에서 고쳐야 했고, 그 문장들이 인용할 측정이 오라클 값이다.
diff --git a/hosts/rust-oracle/tests/checked_arithmetic.rs b/hosts/rust-oracle/tests/checked_arithmetic.rs
new file mode 100644
index 0000000..113110a
--- /dev/null
+++ b/hosts/rust-oracle/tests/checked_arithmetic.rs
@@ -0,0 +1,208 @@
+//! Checked i32 arithmetic in fallible bodies — the values a loaded module returns
+//! (`SPEC-checked-arithmetic` acceptance A, B, C, D, G and DP-O7, DP-O9).
+//!
+//! Every operation is measured on both sides of its boundary: the last input that fits returns
+//! the exact answer, the first that does not returns `ML_ST_OVERFLOW` and leaves the out value
+//! alone. The infallible twin beside it shows the rule is about the BODY, not the operator.
+#![cfg(windows)]
+
+use ml_oracle::Module;
+use mlc::emit::emit_artifacts;
+
+mod common;
+
+const OVERFLOW: i32 = mlc::abi::ML_ST_OVERFLOW;
+
+const SRC: &str = "
+const BIG = 2147483647
+export fn add(a: i32, b: i32) -> i32! { return a + b }
+export fn sub(a: i32, b: i32) -> i32! { return a - b }
+export fn mul(a: i32, b: i32) -> i32! { return a * b }
+export fn neg(a: i32) -> i32! { return -a }
+export fn div(a: i32, b: i32) -> i32! { return a / b }
+export fn rem(a: i32, b: i32) -> i32! { return a % b }
+export fn conv(x: f64) -> i32! { return x as i32 }
+export fn text(a: i32) -> string! { return (a * 2) as string }
+export fn arr(a: i32) -> [i32]! {
+  result 2
+  result[0] = 1
+  result[1] = a * 2
+}
+export fn add_wrap(a: i32, b: i32) -> i32 { return a + b }
+export fn lit() -> i32! { return 2147483647 + 1 }
+export fn via_const(a: i32) -> i32! { return BIG + a }
+fn twice(a: i32) -> i32 { return a * 2 }
+export fn via_helper(a: i32) -> i32! { return twice(a) }
+export fn mid(a: i32) -> i32! { return a * 2 / 2 }
+";
+
+type Bin = extern "C" fn(i32, i32, *mut i32) -> i32;
+type Un = extern "C" fn(i32, *mut i32) -> i32;
+type Conv = extern "C" fn(f64, *mut i32) -> i32;
+type Text = extern "C" fn(i32, *mut u8, i32, *mut i32) -> i32;
+type Arr = extern "C" fn(i32, *mut i32, i32, *mut i32) -> i32;
+type Wrap = extern "C" fn(i32, i32) -> i32;
+type Lit = extern "C" fn(*mut i32) -> i32;
+
+fn load(tag: &str) -> (common::TempOut, Module) {
+    let out = common::TempOut::new(&format!("checked_{tag}"));
+    let arts = emit_artifacts(SRC, "checked", &out).expect("emit checked");
+    let m = Module::load(arts.dll.to_str().unwrap()).expect("load checked.dll");
+    (out, m)
+}
+
+fn sym<T>(m: &Module, name: &[u8]) -> T {
+    let p = m.symbol(name).unwrap();
+    unsafe { std::mem::transmute_copy(&p) }
+}
+
+/// Status and out value; the out value stays at the sentinel when the call fails (D17).
+fn bin(f: Bin, a: i32, b: i32) -> (i32, i32) {
+    let mut v = -7;
+    (f(a, b, &mut v), v)
+}
+
+fn un(f: Un, a: i32) -> (i32, i32) {
+    let mut v = -7;
+    (f(a, &mut v), v)
+}
+
+/// **Acceptance A: each operation, both sides of its boundary.**
+#[test]
+fn each_operation_fails_at_its_boundary_and_not_before() {
+    let (_out, m) = load("ops");
+    let (add, sub, mul): (Bin, Bin, Bin) = (
+        sym(&m, b"mlx_add\0"),
+        sym(&m, b"mlx_sub\0"),
+        sym(&m, b"mlx_mul\0"),
+    );
+    let neg: Un = sym(&m, b"mlx_neg\0");
+
+    assert_eq!(bin(add, i32::MAX - 1, 1), (0, i32::MAX));
+    assert_eq!(bin(add, i32::MAX, 1), (OVERFLOW, -7));
+    assert_eq!(bin(sub, i32::MIN + 1, 1), (0, i32::MIN));
+    assert_eq!(bin(sub, i32::MIN, 1), (OVERFLOW, -7));
+    // 46340² fits, 46341² does not.
+    assert_eq!(bin(mul, 46340, 46340), (0, 2147395600));
+    assert_eq!(bin(mul, 46341, 46341), (OVERFLOW, -7));
+    assert_eq!(bin(mul, -46341, 46341), (OVERFLOW, -7));
+    assert_eq!(un(neg, i32::MIN + 1), (0, i32::MAX));
+    assert_eq!(un(neg, i32::MIN), (OVERFLOW, -7));
+    drop(m);
+}
+
+/// **Acceptance B: division and remainder — only the quotient that does not exist fails.**
+#[test]
+fn only_the_quotient_min_by_minus_one_fails() {
+    let (_out, m) = load("div");
+    let div: Bin = sym(&m, b"mlx_div\0");
+    let rem: Bin = sym(&m, b"mlx_rem\0");
+    assert_eq!(
+        bin(div, i32::MIN, -1),
+        (OVERFLOW, -7),
+        "2^31 has no i32 value"
+    );
+    assert_eq!(bin(div, i32::MIN, 1), (0, i32::MIN));
+    assert_eq!(bin(div, 7, 0), (0, 0), "DP-N4 is untouched: x / 0 is 0");
+    // DP-O5: the true remainder of MIN by -1 is 0, and 0 fits.
+    assert_eq!(bin(rem, i32::MIN, -1), (0, 0));
+    assert_eq!(bin(rem, 7, 0), (0, 0));
+    drop(m);
+}
+
+/// **Acceptance D: `f64 as i32` fails for NaN and for what truncates outside i32, only there.**
+#[test]
+fn a_conversion_with_no_i32_value_fails() {
+    let (_out, m) = load("conv");
+    let conv: Conv = sym(&m, b"mlx_conv\0");
+    let c = |x: f64| {
+        let mut v = -7;
+        (conv(x, &mut v), v)
+    };
+    assert_eq!(c(3.9), (0, 3));
+    assert_eq!(c(-3.9), (0, -3));
+    assert_eq!(c(2147483647.9), (0, i32::MAX), "truncates into range");
+    assert_eq!(c(-2147483648.9), (0, i32::MIN), "truncates into range");
+    for x in [
+        2147483648.0,
+        -2147483649.0,
+        f64::NAN,
+        f64::INFINITY,
+        f64::NEG_INFINITY,
+        3e9,
+    ] {
+        assert_eq!(c(x), (OVERFLOW, -7), "{x} has no i32 value");
+    }
+    drop(m);
+}
+
+/// **Acceptance A and G: the string and array shapes, and a repeat call gives the same answer.**
+#[test]
+fn string_and_array_bodies_are_checked_too() {
+    let (_out, m) = load("shapes");
+    let text: Text = sym(&m, b"mlx_text\0");
+    let mut buf = [0u8; 32];
+    let mut needed = -7;
+    assert_eq!(text(1073741823, buf.as_mut_ptr(), 32, &mut needed), 0);
+    assert_eq!(&buf[..needed as usize - 1], b"2147483646");
+    assert_eq!(
+        text(1073741824, buf.as_mut_ptr(), 32, &mut needed),
+        OVERFLOW
+    );
+
+    let arr: Arr = sym(&m, b"mlx_arr\0");
+    let mut out = [0i32; 2];
+    let mut n = -7;
+    assert_eq!(arr(3, out.as_mut_ptr(), 2, &mut n), 0);
+    assert_eq!(out, [1, 6]);
+    // After `result 2`: the buffer is undefined (DP-O6), and asking again changes nothing —
+    // -3 is not a truncation, so a retry loop keyed on `status < 0` would never converge.
+    for _ in 0..2 {
+        let mut n = -7;
+        assert_eq!(arr(1073741824, out.as_mut_ptr(), 2, &mut n), OVERFLOW);
+    }
+    drop(m);
+}
+
+/// **Acceptance C, DP-O7, DP-O9: the rule belongs to the body.**
+#[test]
+fn infallible_bodies_still_wrap_and_literals_are_checked() {
+    let (_out, m) = load("scope");
+    let add_wrap: Wrap = sym(&m, b"mlx_add_wrap\0");
+    assert_eq!(
+        add_wrap(i32::MAX, 1),
+        i32::MIN,
+        "an infallible body keeps wrapping"
+    );
+
+    // DP-O9: a literal-only overflow is not folded — it fails when it runs.
+    let lit: Lit = sym(&m, b"mlx_lit\0");
+    let mut v = -7;
+    assert_eq!((lit(&mut v), v), (OVERFLOW, -7));
+    let via_const: Un = sym(&m, b"mlx_via_const\0");
+    assert_eq!(un(via_const, 0), (0, i32::MAX));
+    assert_eq!(un(via_const, 1), (OVERFLOW, -7));
+
+    // DP-O7: an infallible helper is the escape hatch — it wraps even under a fallible caller.
+    let via_helper: Un = sym(&m, b"mlx_via_helper\0");
+    assert_eq!(un(via_helper, 1073741824), (0, i32::MIN));
+    drop(m);
+}
+
+/// **The cost the SPEC names (§0.3): a true answer that fits still fails if a step does not.**
+///
+/// `a * 2 / 2` is `a` for every i32, but the product is a value of its own and 2^31 is not an
+/// i32. Pinned because `LANGUAGE.md` states it as the price of the rule, and a stated price with
+/// no measurement is the kind of sentence that drifts.
+#[test]
+fn an_intermediate_overflow_fails_even_when_the_answer_fits() {
+    let (_out, m) = load("mid");
+    let mid: Un = sym(&m, b"mlx_mid\0");
+    assert_eq!(un(mid, 1073741823), (0, 1073741823));
+    assert_eq!(
+        un(mid, 1073741824),
+        (OVERFLOW, -7),
+        "the answer 2^30 fits; the product 2^31 does not"
+    );
+    drop(m);
+}