diff --git a/docs/thesis.md b/docs/thesis.md
index 89d4afd..c7a100f 100644
--- a/docs/thesis.md
+++ b/docs/thesis.md
@@ -8,6 +8,11 @@ AI의 코드 생성 속도 >> 신뢰 확보 속도.
 1. 오류는 더 일찍: 컴파일 타임으로 최대한 끌어당김
    → null 없음(Option), Result, exhaustive matching, definite init,
      미선언 effect = compile error
+   ※ definite init은 문법이 이미 보장한다: let은 항상 초기화식을 요구하고
+     미초기화 바인딩을 쓸 방법이 없다. 별도 검사가 필요 없는 것이 맞다
+   ※ exhaustive matching은 interface hash가 enum 정의 본문을 입력으로 삼는
+     이유이기도 하다. upstream에 variant가 하나 늘면 downstream의 match가
+     깨져야 하는데, 이 검사가 없으면 깨질 것이 없다
 2. 검증은 더 빨리: 검증 속도가 언어 설계의 헌법
    → fast path(check) / slow path(release, deep verify) 분리
    → 컴파일을 느리게/비결정적으로 만드는 기능 원천 배제
diff --git a/lib/exhaust.ml b/lib/exhaust.ml
new file mode 100644
index 0000000..25158f4
--- /dev/null
+++ b/lib/exhaust.ml
@@ -0,0 +1,202 @@
+(* match exhaustiveness와 도달 불가 팔 검사 (Maranget의 usefulness 알고리즘).
+
+   철학 1의 대표 항목이다. 그리고 interface hash가 enum 정의 본문을 입력으로
+   삼는 이유이기도 하다 — upstream에 variant가 하나 늘면 downstream의 match가
+   깨져야 하는데, 이 검사가 없으면 깨질 것이 없다.
+
+   생성자 집합을 알 수 없는 타입(외부 타입, 미지수)은 검사하지 않는다.
+   모르는 것을 위반이라고 말하지 않는다. *)
+
+module T = Types
+
+(* 패턴을 검사용 형태로 줄인다. 바인딩은 와일드카드와 같다 —
+   무엇을 덮는가만 중요하다. *)
+type cpat = CWild | CCtor of string * cpat list
+type ctor = { c_name : string; c_args : T.t list }
+type ctors = Finite of ctor list | Infinite
+
+type env = {
+  (* enum 이름 -> variant 목록. 제네릭은 인스턴스화해서 넘어온다 *)
+  variants : string -> T.t list -> (string * T.t list) list option;
+  is_ctor : string -> bool;
+}
+
+let ctors_of env (t : T.t) : ctors =
+  match T.resolve t with
+  | T.TBool ->
+      Finite
+        [ { c_name = "true"; c_args = [] }; { c_name = "false"; c_args = [] } ]
+  | T.TUnit -> Finite [ { c_name = "unit"; c_args = [] } ]
+  | T.TCon ("Option", [ a ]) ->
+      Finite
+        [
+          { c_name = "Some"; c_args = [ a ] }; { c_name = "None"; c_args = [] };
+        ]
+  | T.TCon ("Result", [ a; b ]) ->
+      Finite
+        [
+          { c_name = "Ok"; c_args = [ a ] }; { c_name = "Err"; c_args = [ b ] };
+        ]
+  | T.TCon (n, args) -> (
+      match env.variants n args with
+      | Some vs ->
+          Finite
+            (List.map (fun (name, tys) -> { c_name = name; c_args = tys }) vs)
+      | None -> Infinite)
+  | _ -> Infinite
+
+let rec of_pattern env (p : Ast.pattern) : cpat =
+  match p with
+  | Ast.P_wild _ -> CWild
+  | Ast.P_lit (Ast.L_bool true, _) -> CCtor ("true", [])
+  | Ast.P_lit (Ast.L_bool false, _) -> CCtor ("false", [])
+  (* 리터럴은 인자 없는 생성자다. 와일드카드로 바꾸면 모든 값을 덮는 것이 되어
+     Int 리터럴 몇 개로 exhaustive가 되어버린다. 타입의 생성자 집합이 무한하므로
+     리터럴만으로는 결코 완전해지지 않는다. *)
+  | Ast.P_lit (Ast.L_int n, _) -> CCtor ("<" ^ n ^ ">", [])
+  | Ast.P_lit (Ast.L_str v, _) -> CCtor ("<" ^ String.escaped v ^ ">", [])
+  | Ast.P_bind (n, _) -> if env.is_ctor n then CCtor (n, []) else CWild
+  | Ast.P_ctor { name; args; _ } ->
+      if env.is_ctor name then CCtor (name, List.map (of_pattern env) args)
+      else CWild
+
+let wilds n = List.init n (fun _ -> CWild)
+
+(* 행렬을 생성자 c로 특수화한다 *)
+let specialize (c : ctor) (matrix : cpat list list) : cpat list list =
+  let arity = List.length c.c_args in
+  List.filter_map
+    (fun row ->
+      match row with
+      | CCtor (n, args) :: rest ->
+          if n = c.c_name then Some (args @ rest) else None
+      | CWild :: rest -> Some (wilds arity @ rest)
+      | [] -> None)
+    matrix
+
+let default_matrix (matrix : cpat list list) : cpat list list =
+  List.filter_map
+    (fun row ->
+      match row with
+      | CCtor _ :: _ -> None
+      | CWild :: rest -> Some rest
+      | [] -> None)
+    matrix
+
+let head_names (matrix : cpat list list) =
+  List.filter_map
+    (fun row -> match row with CCtor (n, _) :: _ -> Some n | _ -> None)
+    matrix
+
+(* 행렬이 덮지 못하는 반례 벡터를 찾는다. None이면 완전하다. *)
+let rec witness env (matrix : cpat list list) (tys : T.t list) :
+    cpat list option =
+  match tys with
+  | [] -> if matrix = [] then Some [] else None
+  | th :: rest -> (
+      let heads = head_names matrix in
+      match ctors_of env th with
+      | Finite cs
+        when List.for_all (fun c -> List.mem c.c_name heads) cs && cs <> [] ->
+          (* 모든 생성자가 나타났다: 각각으로 파고든다 *)
+          let rec try_each = function
+            | [] -> None
+            | c :: more -> (
+                let arity = List.length c.c_args in
+                match witness env (specialize c matrix) (c.c_args @ rest) with
+                | Some ws ->
+                    let args = List.filteri (fun i _ -> i < arity) ws in
+                    let tail = List.filteri (fun i _ -> i >= arity) ws in
+                    Some (CCtor (c.c_name, args) :: tail)
+                | None -> try_each more)
+          in
+          try_each cs
+      | kind -> (
+          (* 빠진 생성자가 있거나 집합이 무한하다 *)
+          match witness env (default_matrix matrix) rest with
+          | None -> None
+          | Some ws ->
+              let head =
+                match kind with
+                | Finite cs -> (
+                    match
+                      List.find_opt (fun c -> not (List.mem c.c_name heads)) cs
+                    with
+                    | Some c -> CCtor (c.c_name, wilds (List.length c.c_args))
+                    | None -> CWild)
+                | Infinite -> CWild
+              in
+              Some (head :: ws)))
+
+let rec show_cpat = function
+  | CWild -> "_"
+  | CCtor (n, []) -> n
+  | CCtor (n, args) ->
+      n ^ "(" ^ String.concat ", " (List.map show_cpat args) ^ ")"
+
+(* 행 q가 행렬 P에 대해 쓸모 있는가 = P가 덮지 못하는 값을 q가 덮는가 *)
+let useful env (matrix : cpat list list) (q : cpat list) (tys : T.t list) : bool
+    =
+  let rec go matrix q tys =
+    match (q, tys) with
+    | [], [] -> matrix = []
+    | qh :: qt, th :: tt -> (
+        match qh with
+        | CCtor (n, args) -> (
+            match ctors_of env th with
+            | Finite cs -> (
+                match List.find_opt (fun c -> c.c_name = n) cs with
+                | Some c -> go (specialize c matrix) (args @ qt) (c.c_args @ tt)
+                | None -> go (default_matrix matrix) qt tt)
+            | Infinite ->
+                let c =
+                  { c_name = n; c_args = List.map (fun _ -> T.TUnknown) args }
+                in
+                go (specialize c matrix) (args @ qt) (c.c_args @ tt))
+        | CWild -> (
+            let heads = head_names matrix in
+            match ctors_of env th with
+            | Finite cs
+              when List.for_all (fun c -> List.mem c.c_name heads) cs
+                   && cs <> [] ->
+                List.exists
+                  (fun c ->
+                    go (specialize c matrix)
+                      (wilds (List.length c.c_args) @ qt)
+                      (c.c_args @ tt))
+                  cs
+            | _ -> go (default_matrix matrix) qt tt))
+    | _ -> false
+  in
+  go matrix q tys
+
+type result = {
+  missing : string option; (* 빠진 경우의 반례 *)
+  unreachable : int list; (* 도달할 수 없는 팔의 번호 (0부터) *)
+}
+
+let check env (scrutinee : T.t) (pats : Ast.pattern list) : result =
+  match ctors_of env scrutinee with
+  | Infinite when T.resolve scrutinee = T.TUnknown ->
+      (* 생성자 집합을 모르면 검사하지 않는다 *)
+      { missing = None; unreachable = [] }
+  | _ ->
+      let rows = List.map (fun p -> [ of_pattern env p ]) pats in
+      let unreachable =
+        let acc = ref [] in
+        List.iteri
+          (fun i row ->
+            let before = List.filteri (fun j _ -> j < i) rows in
+            if not (useful env before row [ scrutinee ]) then acc := i :: !acc)
+          rows;
+        List.rev !acc
+      in
+      let missing =
+        (* 리터럴 패턴이 섞이면 정확한 반례를 만들 수 없다 — 그 열은 무한
+           집합이므로 와일드카드가 없으면 불완전으로 본다 *)
+        match witness env rows [ scrutinee ] with
+        | Some ws -> (
+            match ws with [ w ] -> Some (show_cpat w) | _ -> Some "_")
+        | None -> None
+      in
+      { missing; unreachable }
diff --git a/lib/typecheck.ml b/lib/typecheck.ml
index cda17d8..f1c67ee 100644
--- a/lib/typecheck.ml
+++ b/lib/typecheck.ml
@@ -216,6 +216,7 @@ let rec infer env (e : expr) : T.t =
           pop env)
         arms;
       if arms = [] then err env pos "match에 팔이 없습니다";
+      check_exhaustive env s arms pos;
       result
   | E_scope { name; parent; body; pos } ->
       (match lookup env parent with
@@ -276,6 +277,40 @@ let rec infer env (e : expr) : T.t =
           if not (T.unify a b) then mismatch env pos a b "같은 타입끼리만 비교할 수 있습니다";
           T.TBool)
 
+(* exhaustiveness: 철학 1의 대표 항목이자 interface hash가 enum 본문을
+   입력으로 삼는 이유다 *)
+and check_exhaustive env scrutinee arms pos =
+  let eenv : Exhaust.env =
+    {
+      variants =
+        (fun name args ->
+          match Hashtbl.find_opt env.enums name with
+          | None -> None
+          | Some (gen, variants) ->
+              let sub =
+                try List.map2 (fun v a -> (v, a)) gen args
+                with Invalid_argument _ -> []
+              in
+              Some
+                (List.map
+                   (fun (n, tys) -> (n, List.map (T.subst sub []) tys))
+                   variants));
+      is_ctor =
+        (fun n ->
+          Hashtbl.mem env.ctors n || List.mem n [ "Ok"; "Err"; "Some"; "None" ]);
+    }
+  in
+  let r = Exhaust.check eenv scrutinee (List.map (fun a -> a.arm_pat) arms) in
+  (match r.missing with
+  | None -> ()
+  | Some w -> err env pos (Printf.sprintf "match가 모든 경우를 덮지 않습니다 (빠진 경우: %s)" w));
+  List.iter
+    (fun i ->
+      match List.nth_opt arms i with
+      | Some a -> err env a.arm_pos "이 팔은 앞의 팔들에 가려 도달할 수 없습니다"
+      | None -> ())
+    r.unreachable
+
 and nullary_ctor env enum name =
   match Hashtbl.find_opt env.enums enum with
   | None -> T.TUnknown
diff --git a/samples/11_exhaustiveness.cool b/samples/11_exhaustiveness.cool
new file mode 100644
index 0000000..dd5e30e
--- /dev/null
+++ b/samples/11_exhaustiveness.cool
@@ -0,0 +1,108 @@
+// 11. exhaustiveness 검사기가 거부해야 하는 코드
+//
+// 철학 1의 대표 항목이자, interface hash가 enum 정의 본문을 입력으로 삼는 이유다.
+// upstream에 variant가 하나 늘면 downstream의 match가 깨져야 하는데,
+// 이 검사가 없으면 깨질 것이 없다.
+
+pub enum Shape {
+    Circle(Int),
+    Rect(Int, Int),
+    Point,
+}
+
+// --- 통과해야 하는 것 ---
+
+pub fn area(s: Shape) -> Int {
+    match s {
+        Circle(r) => r * r,
+        Rect(w, h) => w * h,
+        Point => 0,
+    }
+}
+
+pub fn with_wildcard(s: Shape) -> Int {
+    match s {
+        Circle(r) => r,
+        _ => 0,
+    }
+}
+
+pub fn nested_full(o: Option[Shape]) -> Int {
+    match o {
+        Some(Circle(r)) => r,
+        Some(Rect(w, h)) => w * h,
+        Some(Point) => 0,
+        None => 0,
+    }
+}
+
+pub fn results(r: Result[Int, Int]) -> Int {
+    match r {
+        Ok(n) => n,
+        Err(e) => e,
+    }
+}
+
+pub fn flags(b: Bool) -> Int {
+    match b {
+        true => 1,
+        false => 0,
+    }
+}
+
+// --- 여기서부터 전부 오류다 ---
+
+// [E-match-missing] variant 하나가 빠졌다
+pub fn missing_variant(s: Shape) -> Int {
+    match s {
+        Circle(r) => r,
+        Rect(w, h) => w * h,
+    }
+}
+
+// [E-match-missing] Bool도 생성자 집합이 유한하다
+pub fn missing_false(b: Bool) -> Int {
+    match b {
+        true => 1,
+    }
+}
+
+// [E-match-missing] Option
+pub fn missing_none(o: Option[Int]) -> Int {
+    match o {
+        Some(n) => n,
+    }
+}
+
+// [E-match-missing] 중첩된 자리에서 빠진 경우도 찾는다
+pub fn missing_nested(o: Option[Shape]) -> Int {
+    match o {
+        Some(Circle(r)) => r,
+        None => 0,
+    }
+}
+
+// [E-match-missing] Int 리터럴은 생성자 집합이 무한하다
+pub fn missing_literal(n: Int) -> Int {
+    match n {
+        0 => 1,
+        1 => 2,
+    }
+}
+
+// [E-match-unreachable] 앞의 와일드카드에 가린다
+pub fn shadowed(s: Shape) -> Int {
+    match s {
+        _ => 0,
+        Point => 1,
+    }
+}
+
+// [E-match-unreachable] 같은 생성자가 두 번
+pub fn duplicated(s: Shape) -> Int {
+    match s {
+        Circle(r) => r,
+        Circle(x) => x,
+        _ => 0,
+    }
+}
diff --git a/samples/README.md b/samples/README.md
index a8ba546..9a451f9 100644
--- a/samples/README.md
+++ b/samples/README.md
@@ -18,6 +18,7 @@
 | 08_syntax_errors | **파서가** 거부해야 하는 코드 |
 | 09_type_errors | **타입 검사기가** 거부해야 하는 코드 (외부 타입 0개) |
 | 10_effect_errors | **effect 검사기가** 거부해야 하는 코드 (capability를 직접 정의) |
+| 11_exhaustiveness | **exhaustiveness 검사기가** 거부해야 하는 코드 |
 
 05, 08, 09, 10은 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가
 기대 진단이며, 넷의 목적이 다르다 — **08은 파서가, 09는 타입 검사기가,
diff --git a/test/test_coollang.ml b/test/test_coollang.ml
index 656cf18..f77e8fd 100644
--- a/test/test_coollang.ml
+++ b/test/test_coollang.ml
@@ -583,7 +583,8 @@ let () =
         f <> "05_move_errors.cool"
         && f <> "08_syntax_errors.cool"
         && f <> "09_type_errors.cool"
-        && f <> "10_effect_errors.cool")
+        && f <> "10_effect_errors.cool"
+        && f <> "11_exhaustiveness.cool")
     |> List.sort compare
   in
   List.iter
@@ -603,9 +604,12 @@ let () =
   (match Driver.typecheck (Filename.concat dir "10_effect_errors.cool") with
   | Ok () -> check "10은 effect 오류를 내야 한다" false
   | Error errors -> check "10의 effect 오류" (List.length errors >= 6));
-  match Driver.typecheck (Filename.concat dir "05_move_errors.cool") with
+  (match Driver.typecheck (Filename.concat dir "05_move_errors.cool") with
   | Ok () -> check "05는 move 오류를 내야 한다" false
-  | Error errors -> check "05의 move 오류" (List.length errors >= 9)
+  | Error errors -> check "05의 move 오류" (List.length errors >= 9));
+  match Driver.typecheck (Filename.concat dir "11_exhaustiveness.cool") with
+  | Ok () -> check "11은 exhaustiveness 오류를 내야 한다" false
+  | Error errors -> check "11의 exhaustiveness 오류" (List.length errors >= 7)
 
 (* ================================================================== *)
 (* effect / capability 검사                                            *)
@@ -817,3 +821,95 @@ let () =
 
 let () =
   check "모르는 타입은 copyable로 본다" (move_ok "fn f(x: Widget) -> Widget {\n  x\n}")
+
+(* ================================================================== *)
+(* exhaustiveness                                                      *)
+(* ================================================================== *)
+
+let e3 = "enum E {\n  A(Int),\n  B,\n  C,\n}\n"
+
+let () =
+  check "모든 variant를 덮으면 통과"
+    (type_ok
+       (e3
+      ^ "fn f(x: E) -> Int {\n\
+        \  match x {\n\
+        \    A(n) => n,\n\
+        \    B => 1,\n\
+        \    C => 2,\n\
+        \  }\n\
+         }"));
+  check "빠진 variant를 이름으로 말한다"
+    (type_has
+       (e3
+      ^ "fn f(x: E) -> Int {\n  match x {\n    A(n) => n,\n    B => 1,\n  }\n}"
+       )
+       "빠진 경우: C");
+  check "와일드카드가 나머지를 덮는다"
+    (type_ok
+       (e3
+      ^ "fn f(x: E) -> Int {\n  match x {\n    A(n) => n,\n    _ => 0,\n  }\n}"
+       ));
+  check "Bool의 생성자 집합도 유한하다"
+    (type_has "fn f(b: Bool) -> Int {\n  match b {\n    true => 1,\n  }\n}"
+       "빠진 경우: false");
+  check "Option"
+    (type_has
+       "fn f(o: Option[Int]) -> Int {\n  match o {\n    Some(n) => n,\n  }\n}"
+       "빠진 경우: None");
+  check "Result"
+    (type_ok
+       "fn f(r: Result[Int, Int]) -> Int {\n\
+       \  match r {\n\
+       \    Ok(n) => n,\n\
+       \    Err(e) => e,\n\
+       \  }\n\
+        }");
+  check "중첩된 자리의 반례도 찾는다"
+    (type_has
+       (e3
+      ^ "fn f(o: Option[E]) -> Int {\n\
+        \  match o {\n\
+        \    Some(A(n)) => n,\n\
+        \    None => 0,\n\
+        \  }\n\
+         }")
+       "Some(B)");
+  check "Int 리터럴만으로는 완전해지지 않는다"
+    (type_has
+       "fn f(n: Int) -> Int {\n  match n {\n    0 => 1,\n    1 => 2,\n  }\n}"
+       "모든 경우를 덮지 않습니다");
+  check "와일드카드가 있으면 리터럴 match도 통과"
+    (type_ok
+       "fn f(n: Int) -> Int {\n  match n {\n    0 => 1,\n    _ => 2,\n  }\n}")
+
+let () =
+  check "와일드카드 뒤의 팔은 도달할 수 없다"
+    (type_has
+       (e3
+      ^ "fn f(x: E) -> Int {\n  match x {\n    _ => 0,\n    B => 1,\n  }\n}")
+       "도달할 수 없습니다");
+  check "같은 생성자를 두 번 쓰면 뒤가 죽는다"
+    (type_has
+       (e3
+      ^ "fn f(x: E) -> Int {\n\
+        \  match x {\n\
+        \    A(n) => n,\n\
+        \    A(m) => m,\n\
+        \    _ => 0,\n\
+        \  }\n\
+         }")
+       "도달할 수 없습니다");
+  check "생성자 집합을 모르면 검사하지 않는다"
+    (type_ok "fn f(w: Widget) -> Int {\n  match w {\n    _ => 0,\n  }\n}")
+
+(* upstream의 variant 추가가 downstream match를 깨뜨린다 —
+   interface hash가 enum 본문을 입력으로 삼는 이유 *)
+let () =
+  let two = "enum E {\n  A,\n  B,\n}\n" in
+  let three = "enum E {\n  A,\n  B,\n  C,\n}\n" in
+  let user =
+    "fn f(x: E) -> Int {\n  match x {\n    A => 0,\n    B => 1,\n  }\n}"
+  in
+  check "variant 둘일 때는 통과" (type_ok (two ^ user));
+  check "variant가 늘면 같은 코드가 깨진다" (type_has (three ^ user) "빠진 경우: C")