diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj
index f035353..6204be4 100644
--- a/jolt-core/jolt/passes.clj
+++ b/jolt-core/jolt/passes.clj
@@ -794,6 +794,7 @@
 (def ^:private rtenv-box (atom {}))   ;; "ns/name" -> inferred return type
 (def ^:private calls-box (atom []))   ;; collected [ "ns/name" [arg-types...] ]
 (def ^:private escapes-box (atom #{})) ;; var-keys used as a VALUE (not a call head)
+(def ^:private diag-box (atom []))    ;; success-type-check diagnostics (RFC 0006)
 ;; jolt-d6u: a var reference's VALUE type — a fn var is :truthy (non-nil), a def
 ;; var carries its inferred init type (e.g. a color table -> {:vec :struct-map}).
 ;; The orchestrator populates this from sealed (opt-mode) cell roots + def inits.
@@ -1034,6 +1035,121 @@
 
 (defn- infer-top [node] (nth (infer node {}) 1))
 
+;; ---------------------------------------------------------------------------
+;; Success-type checking (RFC 0006). Reuse the inference above as a loose type
+;; checker: flag a core-fn call ONLY when an argument's inferred type is
+;; concrete AND lies in that op's error domain (the op provably throws on it).
+;; Everything ambiguous — :any, :truthy (true/char/...), :nil — is accepted, so
+;; there are no false positives. The table is curated to genuinely-throwing
+;; cases; lenient ops ((get 5 :k) -> nil, (:k 5) -> nil) are NOT listed.
+
+;; concrete non-numbers: arithmetic provably throws on these.
+(defn- not-number? [t]
+  (or (= t :str) (= t :kw) (= t :phm)
+      (struct-type? t) (vec-type? t) (set-type? t)))
+
+;; concrete non-seqable scalars: seq/count/first/nth provably throw on these.
+;; (Strings and collections ARE seqable/countable; :truthy is ambiguous; :nil
+;; and :any are accepted.)
+(defn- not-seqable? [t] (or (= t :num) (= t :kw)))
+
+;; arithmetic / numeric ops: EVERY argument must be a number.
+(def ^:private num-ops
+  #{"+" "-" "*" "/" "inc" "dec" "mod" "rem" "quot" "min" "max" "abs"
+    "bit-and" "bit-or" "bit-xor" "bit-not" "bit-shift-left" "bit-shift-right"})
+;; seq/count/index ops: argument 0 must be seqable/countable.
+(def ^:private seq-ops #{"count" "first" "rest" "next" "seq" "nth"})
+
+(defn- type-name
+  "Render an inferred type for an error message."
+  [t]
+  (cond (struct-type? t) "a map"
+        (vec-type? t) "a vector"
+        (set-type? t) "a set"
+        (= t :str) "a string"
+        (= t :kw) "a keyword"
+        (= t :num) "a number"
+        (= t :phm) "a map"
+        :else (str t)))
+
+(defn- check-invoke
+  "If node is a core-op call whose argument type is provably in the error domain,
+  conj a diagnostic. arg-types is the vector of inferred argument types."
+  [cn args arg-types]
+  (cond
+    (contains? num-ops cn)
+    (reduce (fn [_ i]
+              (let [t (nth arg-types i)]
+                (when (not-number? t)
+                  (swap! diag-box conj
+                         {:op cn :argpos i :type (type-name t)
+                          :msg (str "`" cn "` requires a number, but argument "
+                                    (inc i) " is " (type-name t))})))
+              nil)
+            nil (range (count args)))
+    (and (contains? seq-ops cn) (> (count args) 0))
+    (let [t (nth arg-types 0)]
+      (when (not-seqable? t)
+        (swap! diag-box conj
+               {:op cn :argpos 0 :type (type-name t)
+                :msg (str "`" cn "` requires "
+                          (if (= cn "count") "a countable collection" "a seqable")
+                          ", but argument 1 is " (type-name t))})))
+    :else nil))
+
+(defn- check-walk
+  "Walk the IR, inferring argument types and recording diagnostics for
+  provably-wrong core-fn calls. Threads tenv through binders exactly like infer."
+  [node tenv]
+  (let [op (get node :op)]
+    (cond
+      (= op :invoke)
+      (let [fnode (get node :fn)
+            args (get node :args)
+            cn (when (and (= :var (get fnode :op)) (= "clojure.core" (get fnode :ns)))
+                 (get fnode :name))]
+        (when cn
+          (check-invoke cn args (mapv (fn [a] (nth (infer a tenv) 0)) args)))
+        (check-walk fnode tenv)
+        (reduce (fn [_ a] (check-walk a tenv) nil) nil args))
+      (= op :let)
+      (let [te (reduce (fn [e b]
+                         (check-walk (nth b 1) e)
+                         (assoc e (nth b 0) (nth (infer (nth b 1) e) 0)))
+                       tenv (get node :bindings))]
+        (check-walk (get node :body) te))
+      (= op :if)
+      (do (check-walk (get node :test) tenv)
+          (check-walk (get node :then) tenv)
+          (check-walk (get node :else) tenv))
+      (= op :do)
+      (do (reduce (fn [_ s] (check-walk s tenv) nil) nil (get node :statements))
+          (check-walk (get node :ret) tenv))
+      (= op :fn)
+      (reduce (fn [_ a]
+                (let [pe (reduce (fn [e p] (assoc e p :any)) tenv (get a :params))
+                      pe (if (get a :rest) (assoc pe (get a :rest) :any) pe)]
+                  (check-walk (get a :body) pe))
+                nil)
+              nil (get node :arities))
+      (= op :loop)
+      (do (reduce (fn [_ b] (check-walk (nth b 1) tenv) nil) nil (get node :bindings))
+          (check-walk (get node :body) tenv))
+      (= op :recur)
+      (reduce (fn [_ a] (check-walk a tenv) nil) nil (get node :args))
+      (= op :def) (check-walk (get node :init) tenv)
+      (= op :throw) (check-walk (get node :expr) tenv)
+      (= op :vector) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items))
+      (= op :set) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items))
+      (= op :map)
+      (reduce (fn [_ pr] (check-walk (nth pr 0) tenv) (check-walk (nth pr 1) tenv) nil)
+              nil (get node :pairs))
+      (= op :try)
+      (do (check-walk (get node :body) tenv)
+          (when (get node :catch-body) (check-walk (get node :catch-body) tenv))
+          (when (get node :finally) (check-walk (get node :finally) tenv)))
+      :else nil)))
+
 ;; --- Inter-procedural driver API (jolt-767) consumed by the back end --------
 (defn set-rtenv!
   "Install the current return-type estimates (a map \"ns/name\" -> type) used to
@@ -1053,6 +1169,16 @@
 (defn reset-escapes! [] (reset! escapes-box #{}))
 (defn collected-escapes [] (vec @escapes-box))
 
+(defn check-form
+  "Success-type check a single analyzed form (RFC 0006). Returns a vector of
+  diagnostics [{:op :argpos :type :msg} ...] for provably-wrong core-fn calls;
+  empty when nothing is provably wrong. Runs independently of specialization so
+  it is usable in normal builds (the decoupled checking path)."
+  [node]
+  (reset! diag-box [])
+  (check-walk node {})
+  (vec @diag-box))
+
 (defn infer-body
   "Type `body` under tenv (local-name -> type). Returns [ret-type node' calls],
   where calls is the [[\"ns/name\" [arg-types...]] ...] this body invokes (for
diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet
index f9247e7..7cdf9e3 100644
--- a/src/jolt/backend.janet
+++ b/src/jolt/backend.janet
@@ -613,6 +613,27 @@
   [ctx]
   (build-compiler! ctx))
 
+(defn type-check!
+  "Success-type check the analyzed IR (RFC 0006). Looks up jolt.passes/check-form
+  (absent during pre-passes bootstrap -> no-op), runs it protected so a checker
+  bug never breaks compilation, then reports each diagnostic per strictness:
+  `warn` prints to stderr, `error` throws (failing this form's compilation).
+  Because the checker only fires on PROVABLY-wrong code, a correct program has
+  nothing to report under either level."
+  [ctx ir strictness ns]
+  (def cf (ns-find (ctx-find-ns ctx "jolt.passes") "check-form"))
+  (when cf
+    (def r (protect ((var-get cf) ir)))
+    (when (r 0)
+      (def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1)))
+      (when (and diags (> (length diags) 0))
+        (def loc (if ns (string ns) "?"))
+        (each d diags
+          (def msg (string "type error in " loc ": " (get d :msg)))
+          (if (= strictness "error")
+            (error msg)
+            (eprint "  " msg)))))))
+
 (defn analyze-form
   "Run the portable Clojure analyzer (jolt.analyzer/analyze) on a reader form,
   returning host-neutral IR."
@@ -645,14 +666,23 @@
   # Resolved lazily; absent during the pre-passes bootstrap window.
   (def pv (unless (= "1" (os/getenv "JOLT_NO_IR_PASSES"))
             (ns-find (ctx-find-ns ctx "jolt.passes") "run-passes")))
-  (if pv
-    (let [pr (protect ((var-get pv) (r 1) ctx))]
-      # the pass runs interpreted; a throw inside it unwinds past the
-      # interpreter's ns restores — put the compile ns back either way, or
-      # the REST of this compilation resolves in jolt.passes
-      (ctx-set-current-ns ctx saved-ns)
-      (if (pr 0) (pr 1) (r 1)))
-    (r 1)))
+  (def result
+    (if pv
+      (let [pr (protect ((var-get pv) (r 1) ctx))]
+        # the pass runs interpreted; a throw inside it unwinds past the
+        # interpreter's ns restores — put the compile ns back either way, or
+        # the REST of this compilation resolves in jolt.passes
+        (ctx-set-current-ns ctx saved-ns)
+        (if (pr 0) (pr 1) (r 1)))
+      (r 1)))
+  # Success-type check (RFC 0006), decoupled from specialization: runs whenever
+  # JOLT_TYPE_CHECK is warn/error, regardless of :inline?. Read at runtime so it
+  # needs no rebuild. The analyzed IR (r 1) carries no specialization; the
+  # checker does its own inference.
+  (def tc (os/getenv "JOLT_TYPE_CHECK"))
+  (when (and tc (not= tc "off") (not= tc "0"))
+    (type-check! ctx (r 1) tc saved-ns))
+  result)
 
 # The analyzer's deliberate punt signal — (uncompilable why) throws the string
 # "jolt/uncompilable: <why>". Anything else escaping the compile step is an
diff --git a/test/integration/type-check-test.janet b/test/integration/type-check-test.janet
new file mode 100644
index 0000000..0804c0c
--- /dev/null
+++ b/test/integration/type-check-test.janet
@@ -0,0 +1,57 @@
+# Success-type checking (RFC 0006, jolt-y3b). The structural inference of
+# RFC 0005, reused as a loose checker: flag a core-fn call ONLY when an argument
+# is PROVABLY the wrong type (concrete and in the op's throwing error domain).
+# Ambiguous cases (:any, unions, :truthy) are accepted — no false positives.
+(import ../../src/jolt/api :as api)
+(import ../../src/jolt/backend :as backend)
+(import ../../src/jolt/types :as types)
+(import ../../src/jolt/reader :as reader)
+
+(print "Success-type checking (jolt-y3b)...")
+
+(os/setenv "JOLT_DIRECT_LINK" "1")
+(def ctx (api/init {:compile? true}))
+(def pns (types/ctx-find-ns ctx "jolt.passes"))
+(def check (types/var-get (types/ns-find pns "check-form")))
+
+# diagnostics (a Janet tuple of diag structs) for a source form
+(defn diags [src]
+  (api/normalize-pvecs (check (backend/analyze-form ctx (reader/parse-string src)))))
+(defn nd [src] (length (diags src)))
+
+# --- provably wrong: REPORTED ------------------------------------------------
+(assert (= 1 (nd "(inc \"x\")")) "inc on a string")
+(assert (= 1 (nd "(+ 1 \"x\")")) "+ with a string arg")
+(assert (= 1 (nd "(count :foo)")) "count of a keyword")
+(assert (= 1 (nd "(count 5)")) "count of a number")
+(assert (= 1 (nd "(first 42)")) "first of a number")
+(assert (= 1 (nd "(nth :k 0)")) "nth of a keyword")
+(assert (= 1 (nd "(let [n \"x\"] (inc n))")) "inc on a let-bound string")
+(assert (= 1 (nd "(inc (count :k))")) "inner count of keyword reported (inc of :num is fine)")
+
+# --- ambiguous / lenient: ACCEPTED (no false positive) -----------------------
+(assert (= 0 (nd "(:k 5)")) "keyword lookup on a number returns nil, not an error")
+(assert (= 0 (nd "(get 5 :k)")) "get on a number returns nil, not an error")
+(assert (= 0 (nd "(fn [x] (inc x))")) "inc on an unknown (:any) param accepted")
+(assert (= 0 (nd "(fn [c] (inc (if c 1 \"x\")))")) "inc on a {:num | :str} branch -> :any, accepted")
+(assert (= 0 (nd "(count \"ab\")")) "count of a string is fine")
+(assert (= 0 (nd "(count [1 2 3])")) "count of a vector is fine")
+(assert (= 0 (nd "(first [1 2 3])")) "first of a vector is fine")
+(assert (= 0 (nd "(inc (count [1 2 3]))")) "count of vector + inc of :num both fine")
+(assert (= 0 (nd "(inc (first [1 2 3]))")) "first of vector -> :num, inc fine")
+
+# --- the diagnostic carries op + type + a message ----------------------------
+(def one (in (diags "(inc \"x\")") 0))
+(assert (= "inc" (get one :op)) "diagnostic names the op")
+(assert (string/find "number" (get one :msg)) "message says a number is required")
+
+# --- end-to-end: strictness drives compilation (decoupled from :inline?) -----
+# error mode aborts a provably-wrong form's compilation; a correct form compiles.
+(os/setenv "JOLT_TYPE_CHECK" "error")
+(assert (not (first (protect (api/eval-string ctx "(count :nope)"))))
+        "error mode aborts a provably-wrong form")
+(assert (first (protect (api/eval-string ctx "(count [1 2 3])")))
+        "error mode accepts a correct form")
+(os/setenv "JOLT_TYPE_CHECK" "off")
+
+(print "Success-type checking passed!")