diff --git a/specification/wasm-3.0/7.1-soundness.configurations.spectec b/specification/wasm-3.0/7.1-soundness.configurations.spectec
index 3ef64d767b..055fb5f324 100644
--- a/specification/wasm-3.0/7.1-soundness.configurations.spectec
+++ b/specification/wasm-3.0/7.1-soundness.configurations.spectec
@@ -26,9 +26,9 @@ rule Instr_ok2/frame:
   -- Expr_ok2: s; C' |- instr* : t^n
 
 rule Instr_ok2/handler:
-  s; C |- HANDLER_ n `{catch*} instr* : t_1* -> t_2*
+  s; C |- HANDLER_ n `{catch*} instr* : eps -> t*
   -- (Catch_ok: C |- catch : OK)*
-  -- Instrs_ok2: s; C |- instr* : t_1* ->_(x*) t_2*
+  -- Instrs_ok2: s; C |- instr* : eps ->_(x*) t*
 
 rule Instr_ok2/trap:
   s; C |- TRAP : t_1* -> t_2*
diff --git a/specification/wasm-latest/7.1-soundness.configurations.spectec b/specification/wasm-latest/7.1-soundness.configurations.spectec
index 3ef64d767b..055fb5f324 100644
--- a/specification/wasm-latest/7.1-soundness.configurations.spectec
+++ b/specification/wasm-latest/7.1-soundness.configurations.spectec
@@ -26,9 +26,9 @@ rule Instr_ok2/frame:
   -- Expr_ok2: s; C' |- instr* : t^n
 
 rule Instr_ok2/handler:
-  s; C |- HANDLER_ n `{catch*} instr* : t_1* -> t_2*
+  s; C |- HANDLER_ n `{catch*} instr* : eps -> t*
   -- (Catch_ok: C |- catch : OK)*
-  -- Instrs_ok2: s; C |- instr* : t_1* ->_(x*) t_2*
+  -- Instrs_ok2: s; C |- instr* : eps ->_(x*) t*
 
 rule Instr_ok2/trap:
   s; C |- TRAP : t_1* -> t_2*
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index 15c60d0f10..66bf13eeca 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -8235,11 +8235,11 @@ relation Instr_ok2: `%;%|-%:%`(store, context, instr, instrtype)
     -- Frame_ok: `%|-%:%`(s, f, C')
     -- Expr_ok2: `%;%|-%:%`(s, C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`}))
 
-  ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:28.1-31.52
-  rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*, `x*` : idx*}:
-    `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`})))
+  ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:28.1-31.49
+  rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t*` : valtype*, `x*` : idx*}:
+    `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t <- `t*`})))
     -- (Catch_ok: `%|-%:OK`(C, catch))*{catch <- `catch*`}
-    -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`})))
+    -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([]), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`})))
 
   ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:33.1-35.42
   rule trap{s : store, C : context, `t_1*` : valtype*, `t_2*` : valtype*}:
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index 1253a23f3c..5734cf0610 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -14165,9 +14165,9 @@ $$
 \frac{
 (C \vdash {\mathit{catch}} : \mathsf{ok})^\ast
  \qquad
-s ; C \vdash {{\mathit{instr}}^\ast} : {t_1^\ast} \rightarrow_{{x^\ast}} {t_2^\ast}
+s ; C \vdash {{\mathit{instr}}^\ast} : \epsilon \rightarrow_{{x^\ast}} {t^\ast}
 }{
-s ; C \vdash {{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}}~{{\mathit{instr}}^\ast} : {t_1^\ast} \rightarrow {t_2^\ast}
+s ; C \vdash {{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}}~{{\mathit{instr}}^\ast} : \epsilon \rightarrow {t^\ast}
 } \, {[\textsc{\scriptsize Instr\_ok2{-}handler}]}
 \qquad
 \end{array}
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 526d41eb0b..b8b959fd83 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -7758,11 +7758,11 @@ relation Instr_ok2: `%;%|-%:%`(store, context, instr, instrtype)
     -- Frame_ok: `%|-%:%`(s, f, C')
     -- Expr_ok2: `%;%|-%:%`(s, C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`}))
 
-  ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:28.1-31.52
-  rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*, `x*` : idx*}:
-    `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`})))
+  ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:28.1-31.49
+  rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t*` : valtype*, `x*` : idx*}:
+    `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t <- `t*`})))
     -- (Catch_ok: `%|-%:OK`(C, catch))*{catch <- `catch*`}
-    -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`})))
+    -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([]), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`})))
 
   ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:33.1-35.42
   rule trap{s : store, C : context, `t_1*` : valtype*, `t_2*` : valtype*}:
@@ -19610,11 +19610,11 @@ relation Instr_ok2: `%;%|-%:%`(store, context, instr, instrtype)
     -- Frame_ok: `%|-%:%`(s, f, C')
     -- Expr_ok2: `%;%|-%:%`(s, C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`}))
 
-  ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:28.1-31.52
-  rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*, `x*` : idx*}:
-    `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`})))
+  ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:28.1-31.49
+  rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t*` : valtype*, `x*` : idx*}:
+    `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t <- `t*`})))
     -- (Catch_ok: `%|-%:OK`(C, catch))*{catch <- `catch*`}
-    -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`})))
+    -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([]), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`})))
 
   ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:33.1-35.42
   rule trap{s : store, C : context, `t_1*` : valtype*, `t_2*` : valtype*}:
@@ -31657,11 +31657,11 @@ relation Instr_ok2: `%;%|-%:%`(store, context, instr, instrtype)
     -- Frame_ok: `%|-%:%`(s, f, C')
     -- Expr_ok2: `%;%|-%:%`(s, C', instr*{instr <- `instr*`}, `%`_resulttype(t^n{t <- `t*`}))
 
-  ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:28.1-31.52
-  rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*, `x*` : idx*}:
-    `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`})))
+  ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:28.1-31.49
+  rule handler{s : store, C : context, n : n, `catch*` : catch*, `instr*` : instr*, `t*` : valtype*, `x*` : idx*}:
+    `%;%|-%:%`(s, C, `HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t <- `t*`})))
     -- (Catch_ok: `%|-%:OK`(C, catch))*{catch <- `catch*`}
-    -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`})))
+    -- Instrs_ok2: `%;%|-%:%`(s, C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype([]), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`})))
 
   ;; ../../../../specification/wasm-latest/7.1-soundness.configurations.spectec:33.1-35.42
   rule trap{s : store, C : context, `t_1*` : valtype*, `t_2*` : valtype*}:
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index 79ee43a15f..ec0313651c 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -17987,13 +17987,15 @@ The frame :math:`\{ \mathsf{locals}~{({{\mathit{val}}^?})^\ast},\;\allowbreak \m
 
       * The instruction :math:`{\mathit{instr}}` is of the form :math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}}^\ast}~\}~{{\mathit{instr}''}^\ast})`.
 
+      * The value type sequence :math:`{{\mathit{valtype}}^\ast}` is empty.
+
       * The local index sequence :math:`{{\mathit{localidx}}^\ast}` is empty.
 
       * For all :math:`{\mathit{catch}}` in :math:`{{\mathit{catch}}^\ast}`:
 
          * The catch clause :math:`{\mathit{catch}}` is :ref:`valid <valid-val>`.
 
-      * :math:`{{\mathit{instr}''}^\ast}` is valid with :math:`{{\mathit{valtype}}^\ast}~{\rightarrow}_{{x^\ast}}\,{{\mathit{valtype}'}^\ast}`.
+      * :math:`{{\mathit{instr}''}^\ast}` is valid with :math:`\epsilon~{\rightarrow}_{{x^\ast}}\,{{\mathit{valtype}'}^\ast}`.
    * Or:
 
       * The instruction :math:`{\mathit{instr}}` is of the form :math:`\mathsf{trap}`.
@@ -18041,14 +18043,14 @@ The frame :math:`\{ \mathsf{locals}~{({{\mathit{val}}^?})^\ast},\;\allowbreak \m
 
 
 
-:math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}}^\ast}~\}~{{\mathit{instr}}^\ast})` is valid with :math:`{t_1^\ast}~\rightarrow~{t_2^\ast}` if:
+:math:`({{\mathsf{handler}}_{n}}{\{}~{{\mathit{catch}}^\ast}~\}~{{\mathit{instr}}^\ast})` is valid with :math:`\epsilon~\rightarrow~{t^\ast}` if:
 
 
    * For all :math:`{\mathit{catch}}` in :math:`{{\mathit{catch}}^\ast}`:
 
       * The catch clause :math:`{\mathit{catch}}` is :ref:`valid <valid-val>`.
 
-   * :math:`{{\mathit{instr}}^\ast}` is valid with :math:`{t_1^\ast}~{\rightarrow}_{{x^\ast}}\,{t_2^\ast}`.
+   * :math:`{{\mathit{instr}}^\ast}` is valid with :math:`\epsilon~{\rightarrow}_{{x^\ast}}\,{t^\ast}`.
 
 
 
@@ -29764,10 +29766,11 @@ Instr_ok2
     - instr''* is valid with valtype'^n.
   - Or:
     - instr is (HANDLER_ n { catch* } instr''*).
+    - valtype* is [].
     - localidx* is [].
     - For all catch in catch*:
       - the catch clause catch is valid.
-    - instr''* is valid with valtype* ->_ x* valtype'*.
+    - instr''* is valid with [] ->_ x* valtype'*.
   - Or:
     - instr is TRAP.
     - localidx* is [].
@@ -29792,10 +29795,10 @@ Instr_ok2/frame
   - instr* is valid with t^n.
 
 Instr_ok2/handler
-- (HANDLER_ n { catch* } instr*) is valid with t_1* -> t_2* if:
+- (HANDLER_ n { catch* } instr*) is valid with [] -> t* if:
   - For all catch in catch*:
     - the catch clause catch is valid.
-  - instr* is valid with t_1* ->_ x* t_2*.
+  - instr* is valid with [] ->_ x* t*.
 
 Instr_ok2/trap
 - TRAP is valid with t_1* -> t_2* if: