diff --git a/Test/Passes/CastsReconciliation/basic.mlir b/Test/Passes/CastsReconciliation/basic.mlir
index 8a89e9d7c..dda423d01 100644
--- a/Test/Passes/CastsReconciliation/basic.mlir
+++ b/Test/Passes/CastsReconciliation/basic.mlir
@@ -2,7 +2,6 @@
 
 "builtin.module"() ({
 
-  ^1():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^1(%0 : i64):
         %1 = "builtin.unrealized_conversion_cast"(%0) : (i64) -> i64
@@ -11,7 +10,6 @@
         "func.return"() : () -> ()
     }) : () -> ()
     
-  ^2():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^1(%0 : i64):
         %1 = "builtin.unrealized_conversion_cast"(%0) : (i64) -> !riscv.reg
@@ -21,7 +19,6 @@
         "func.return"() : () -> ()
     }) : () -> ()
     
-  ^3():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^1(%0 : i64):
         // the remaining cast is unused 
@@ -33,7 +30,6 @@
         "func.return"() : () -> ()
     }) : () -> ()
 
-  ^4():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^1(%0 : i64):
         // the remaining cast is used
@@ -48,7 +44,6 @@
         "func.return"() : () -> ()
     }) : () -> ()
     
-  ^5():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^1(%0 : i64):
         // identity cast and pairs of casts
@@ -61,7 +56,6 @@
         "func.return"() : () -> ()
     }) : () -> ()
   
-  ^6():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^1(%0 : i64):
         // pairs of casts
@@ -75,7 +69,6 @@
         "func.return"() : () -> ()
     }) : () -> ()
     
-  ^7():
     "func.func"()  <{function_type = (!riscv.reg) -> ()}> ({
       ^1(%0 : !riscv.reg):
         // identity cast on block argument
@@ -86,7 +79,6 @@
         "func.return"() : () -> ()
     }) : () -> ()
   
-  ^8():
     "func.func"()  <{function_type = (i8) -> ()}> ({
       ^1(%0 : i8):
         %1 = "builtin.unrealized_conversion_cast"(%0) : (i8) -> i8
@@ -95,7 +87,6 @@
         "func.return"() : () -> ()
     }) : () -> ()
     
-  ^9():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^1(%0 : i64):
         // pairs of casts
diff --git a/Test/Passes/CastsReconciliation/error.mlir b/Test/Passes/CastsReconciliation/error.mlir
index 4ce38a3c5..ceb2ce1da 100644
--- a/Test/Passes/CastsReconciliation/error.mlir
+++ b/Test/Passes/CastsReconciliation/error.mlir
@@ -2,7 +2,6 @@
 
 "builtin.module"() ({
 
-  ^1():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^1(%0 : i64):
         %1 = "builtin.unrealized_conversion_cast"(%0) : (i64) -> i8
@@ -14,7 +13,6 @@
         "func.return"() : () -> ()
     }) : () -> ()
 
-  ^2():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^1(%0 : i64):
         %1 = "builtin.unrealized_conversion_cast"(%0) : (i64) -> !riscv.reg
diff --git a/Test/Passes/DCE/basic.mlir b/Test/Passes/DCE/basic.mlir
index d2970c801..51ce7a6e1 100644
--- a/Test/Passes/DCE/basic.mlir
+++ b/Test/Passes/DCE/basic.mlir
@@ -5,7 +5,6 @@
 "builtin.module"() ({
   
   // An operation that returns one unused result
-  ^4():
     "func.func"()  <{function_type = (i64) -> ()}> ({
       ^6(%1 : i64):
         %2 = "llvm.add"(%1, %1) : (i64, i64) -> i64
@@ -18,7 +17,6 @@
     }) : () -> ()
   
   // A chain of operations that is eventually unused
-  ^5():
     "func.func"()  <{function_type = () -> ()}> ({
       ^6():
         %1 = "arith.constant"() <{ "value" = 1 : i64 }> : () -> i64
@@ -34,7 +32,6 @@
     }) : () -> ()
   
   // A chain of operations that is eventually used
-  ^6():
     "func.func"()  <{function_type = () -> ()}> ({
       ^6():
         %1 = "arith.constant"() <{ "value" = 1 : i64 }> : () -> i64
diff --git a/Test/Tools/veir_mlir_same_verdict.sh b/Test/Tools/veir_mlir_same_verdict.sh
new file mode 100755
index 000000000..d7d369102
--- /dev/null
+++ b/Test/Tools/veir_mlir_same_verdict.sh
@@ -0,0 +1,39 @@
+#!/usr/bin/env bash
+#
+# Check that veir-opt and mlir-opt reach the same accept/reject verdict on a
+# single test file. Used by the `VEIR_MLIR_SAME_VERDICT` lit substitution (see Test/lit.cfg).
+#
+# Usage: veir_mlir_same_verdict.sh <veir-opt> <mlir-opt> <test-file>
+#
+# Exits 0 iff both tools verify the input (both accept) or both reject it (parse
+# or verification failure). Only the verdict is compared, not the diagnostic
+# text, which is not stable across mlir-opt versions.
+#
+# veir-opt natively accepts unregistered ops such as `test.test`; mlir-opt needs
+# `--allow-unregistered-dialect` to do the same, so the two invocations differ
+# only by that flag.
+
+set -u
+
+if [ "$#" -ne 3 ]; then
+  echo "veir_mlir_same_verdict.sh: expected 3 arguments, got $#" >&2
+  exit 2
+fi
+
+veir="$1"
+mlir="$2"
+file="$3"
+
+"$veir" "$file" >/dev/null 2>&1
+[ $? -eq 0 ] && veir_verdict=accept || veir_verdict=reject
+
+"$mlir" --allow-unregistered-dialect "$file" >/dev/null 2>&1
+[ $? -eq 0 ] && mlir_verdict=accept || mlir_verdict=reject
+
+if [ "$veir_verdict" = "$mlir_verdict" ]; then
+  echo "VEIR_MLIR_SAME_VERDICT: veir-opt and mlir-opt agree ($veir_verdict) on $file"
+  exit 0
+fi
+
+echo "VEIR_MLIR_SAME_VERDICT: DISAGREEMENT on $file: veir-opt=$veir_verdict mlir-opt=$mlir_verdict" >&2
+exit 1
diff --git a/Test/Verifier/dominance_back_edge.mlir b/Test/Verifier/dominance_back_edge.mlir
new file mode 100644
index 000000000..b3a5617a3
--- /dev/null
+++ b/Test/Verifier/dominance_back_edge.mlir
@@ -0,0 +1,24 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// %x is defined in the loop body but used in the loop header. The header is
+// reachable from ^entry without going through ^body, so ^body does not dominate
+// the header and the use of %x there is invalid.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = () -> i32, sym_name = "main"}> ({
+  ^entry():
+    "cf.br"() [^header] : () -> ()
+  ^body():
+    %x = "arith.constant"() <{"value" = 5 : i32}> : () -> i32
+    "cf.br"() [^header] : () -> ()
+  ^header():
+    %y = "arith.addi"(%x, %x) : (i32, i32) -> i32
+    %c = "arith.constant"() <{"value" = 1 : i1}> : () -> i1
+    "cf.cond_br"(%c) [^body, ^exit] <{"branch_weights" = array<i32>, "operandSegmentSizes" = array<i32: 1, 0, 0>}> : (i1) -> ()
+  ^exit():
+    "func.return"(%y) : (i32) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: arith.addi: operand 0 {{.*}} does not dominate its use
diff --git a/Test/Verifier/dominance_block_argument.mlir b/Test/Verifier/dominance_block_argument.mlir
new file mode 100644
index 000000000..86016c3f9
--- /dev/null
+++ b/Test/Verifier/dominance_block_argument.mlir
@@ -0,0 +1,19 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// Block arguments are subject to the same dominance rule as op results. %arg is
+// an argument of ^a, but it is used in ^b, and ^a does not dominate ^b (^b is
+// also reachable directly from ^entry).
+
+"builtin.module"() ({
+  "func.func"() <{function_type = (i1) -> i1, sym_name = "main"}> ({
+  ^entry(%c : i1):
+    "cf.cond_br"(%c, %c) [^a, ^b] <{"branch_weights" = array<i32>, "operandSegmentSizes" = array<i32: 1, 1, 0>}> : (i1, i1) -> ()
+  ^a(%arg : i1):
+    "cf.br"() [^b] : () -> ()
+  ^b:
+    "func.return"(%arg) : (i1) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: func.return: operand 0 {{.*}} does not dominate its use
diff --git a/Test/Verifier/dominance_cross_block.mlir b/Test/Verifier/dominance_cross_block.mlir
new file mode 100644
index 000000000..1959d5bc1
--- /dev/null
+++ b/Test/Verifier/dominance_cross_block.mlir
@@ -0,0 +1,20 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// %x is defined in ^a but used in ^b. ^a does not dominate ^b, because ^b is
+// also reachable directly from ^entry, so this violates SSA dominance even
+// though every name is assigned exactly once and every use is defined.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = (i1) -> i32, sym_name = "main"}> ({
+  ^entry(%c : i1):
+    "cf.cond_br"(%c) [^a, ^b] <{"branch_weights" = array<i32>, "operandSegmentSizes" = array<i32: 1, 0, 0>}> : (i1) -> ()
+  ^a:
+    %x = "arith.constant"() <{"value" = 42 : i32}> : () -> i32
+    "cf.br"() [^b] : () -> ()
+  ^b:
+    "func.return"(%x) : (i32) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: func.return: operand 0 {{.*}} does not dominate its use
diff --git a/Test/Verifier/dominance_graph_capture.mlir b/Test/Verifier/dominance_graph_capture.mlir
new file mode 100644
index 000000000..9d1b49937
--- /dev/null
+++ b/Test/Verifier/dominance_graph_capture.mlir
@@ -0,0 +1,30 @@
+// RUN: veir-opt %s | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// A graph region captures %x from ^A, and ^A does not dominate ^B (the block
+// that owns the graph region). The capture is used in a NON-entry block (^g1)
+// of the multi-block graph region. Like MLIR, dominance is only checked in
+// blocks reachable from their region's entry; ^g1 has no intra-region control
+// flow into it, so it is unreachable and the use is not checked. The program
+// therefore verifies. (A capture used in the graph region's entry block ^g0 is
+// still checked -- see dominance_graph_capture_result.mlir.)
+
+"builtin.module"() ({
+  "func.func"() <{function_type = (i1) -> (), sym_name = "m"}> ({
+  ^entry(%c : i1):
+    "cf.cond_br"(%c) [^A, ^B] <{"branch_weights" = array<i32>, "operandSegmentSizes" = array<i32: 1, 0, 0>}> : (i1) -> ()
+  ^A():
+    %x = "test.test"() : () -> i64
+    "cf.br"() [^B] : () -> ()
+  ^B():
+    "test.test"() ({
+    ^g0():
+      "test.test"() : () -> ()
+    ^g1():
+      "test.test"(%x) : (i64) -> ()
+    }) : () -> ()
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: "test.test"(%{{.*}}) : (i64) -> ()
diff --git a/Test/Verifier/dominance_graph_capture_block_argument.mlir b/Test/Verifier/dominance_graph_capture_block_argument.mlir
new file mode 100644
index 000000000..3841a3e7c
--- /dev/null
+++ b/Test/Verifier/dominance_graph_capture_block_argument.mlir
@@ -0,0 +1,24 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// The block argument %arg is only available along the path through ^b. Hiding
+// its use inside a nested graph region in sibling block ^a must not bypass the
+// enclosing SSACFG dominance requirement.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = (i1) -> (), sym_name = "main"}> ({
+  ^entry(%c : i1):
+    %v = "arith.constant"() <{"value" = 5 : i32}> : () -> i32
+    "cf.cond_br"(%c, %v) [^b, ^a] <{"branch_weights" = array<i32>, "operandSegmentSizes" = array<i32: 1, 1, 0>}> : (i1, i32) -> ()
+  ^b(%arg : i32):
+    "cf.br"() [^a] : () -> ()
+  ^a:
+    "test.test"() ({
+    ^inner:
+      "test.test"(%arg) : (i32) -> ()
+    }) : () -> ()
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: test.test: operand 0 {{.*}} does not dominate its use
diff --git a/Test/Verifier/dominance_graph_capture_result.mlir b/Test/Verifier/dominance_graph_capture_result.mlir
new file mode 100644
index 000000000..3193f9426
--- /dev/null
+++ b/Test/Verifier/dominance_graph_capture_result.mlir
@@ -0,0 +1,25 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// The use of %x is inside a graph region, where same-block operation order does
+// not matter. But %x is defined in sibling CFG block ^b, and ^b does not
+// dominate the graph-owning operation in ^a because ^a is reachable directly
+// from ^entry.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = (i1) -> (), sym_name = "main"}> ({
+  ^entry(%c : i1):
+    "cf.cond_br"(%c) [^b, ^a] <{"branch_weights" = array<i32>, "operandSegmentSizes" = array<i32: 1, 0, 0>}> : (i1) -> ()
+  ^b:
+    %x = "arith.constant"() <{"value" = 5 : i32}> : () -> i32
+    "cf.br"() [^a] : () -> ()
+  ^a:
+    "test.test"() ({
+    ^inner:
+      "test.test"(%x) : (i32) -> ()
+    }) : () -> ()
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: test.test: operand 0 {{.*}} does not dominate its use
diff --git a/Test/Verifier/dominance_graph_intra_ok.mlir b/Test/Verifier/dominance_graph_intra_ok.mlir
new file mode 100644
index 000000000..51c7df7f1
--- /dev/null
+++ b/Test/Verifier/dominance_graph_intra_ok.mlir
@@ -0,0 +1,22 @@
+// RUN: veir-opt %s | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// Inside a multi-block graph region there is no block ordering, so %a (defined in
+// ^g0) may be used in the sibling block ^g1. The captured value %v dominates the
+// graph-owning operation, so it is also a legal use. The program verifies.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = () -> (), sym_name = "m"}> ({
+  ^entry():
+    %v = "test.test"() : () -> i64
+    "test.test"() ({
+    ^g0():
+      %a = "test.test"() : () -> i64
+    ^g1():
+      "test.test"(%a, %v) : (i64, i64) -> ()
+    }) : () -> ()
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: "test.test"(%{{.*}}, %{{.*}}) : (i64, i64) -> ()
diff --git a/Test/Verifier/dominance_graph_region_ok.mlir b/Test/Verifier/dominance_graph_region_ok.mlir
new file mode 100644
index 000000000..bd73ce5ad
--- /dev/null
+++ b/Test/Verifier/dominance_graph_region_ok.mlir
@@ -0,0 +1,18 @@
+// RUN: veir-opt %s | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// Dominance is only required in SSACFG regions. The body of an unregistered op
+// is a graph region, where a value defined in one block may be used in another
+// block that it does not dominate, so this program verifies.
+
+"builtin.module"() ({
+  "test.test"() ({
+  ^bb0:
+    %v = "test.test"() : () -> i32
+  ^bb1:
+    "test.test"(%v) : (i32) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK:      %[[V:.*]] = "test.test"() : () -> i32
+// CHECK:      "test.test"(%[[V]]) : (i32) -> ()
diff --git a/Test/Verifier/dominance_sibling_branch.mlir b/Test/Verifier/dominance_sibling_branch.mlir
new file mode 100644
index 000000000..b16c121fb
--- /dev/null
+++ b/Test/Verifier/dominance_sibling_branch.mlir
@@ -0,0 +1,20 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// %x is defined in ^then and used in the sibling block ^else. Neither branch of
+// the conditional dominates the other, so the use in ^else is not dominated by
+// its definition.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = (i1) -> i32, sym_name = "main"}> ({
+  ^entry(%c : i1):
+    "cf.cond_br"(%c) [^then, ^else] <{"branch_weights" = array<i32>, "operandSegmentSizes" = array<i32: 1, 0, 0>}> : (i1) -> ()
+  ^then:
+    %x = "arith.constant"() <{"value" = 7 : i32}> : () -> i32
+    "func.return"(%x) : (i32) -> ()
+  ^else:
+    "func.return"(%x) : (i32) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: func.return: operand 0 {{.*}} does not dominate its use
diff --git a/Test/Verifier/dominance_unreachable_ok.mlir b/Test/Verifier/dominance_unreachable_ok.mlir
new file mode 100644
index 000000000..65eadc71c
--- /dev/null
+++ b/Test/Verifier/dominance_unreachable_ok.mlir
@@ -0,0 +1,20 @@
+// RUN: veir-opt %s | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// Like LLVM/MLIR, the dominance check is skipped for unreachable blocks. ^dead
+// has no predecessors (^entry returns), so its use of %v imposes no dominance
+// requirement and the program verifies.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = () -> i32, sym_name = "main"}> ({
+  ^entry():
+    %v = "arith.constant"() <{"value" = 0 : i32}> : () -> i32
+    "func.return"(%v) : (i32) -> ()
+  ^dead():
+    "func.return"(%v) : (i32) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK:      %[[V:.*]] = "arith.constant"() <{"value" = 0 : i32}> : () -> i32
+// CHECK-NEXT: "func.return"(%[[V]]) : (i32) -> ()
+// CHECK:      "func.return"(%[[V]]) : (i32) -> ()
diff --git a/Test/Verifier/entry_block_predecessor.mlir b/Test/Verifier/entry_block_predecessor.mlir
new file mode 100644
index 000000000..70b1103a6
--- /dev/null
+++ b/Test/Verifier/entry_block_predecessor.mlir
@@ -0,0 +1,18 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// The entry block of a region may not have predecessors. Here ^bb1 branches back
+// to the entry block ^bb0, which would mean the region is re-entered through its
+// entry block and breaks the assumption that the entry block dominates the rest
+// of the region.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = () -> (), sym_name = "main"}> ({
+  ^bb0():
+    "cf.br"() [^bb1] : () -> ()
+  ^bb1():
+    "cf.br"() [^bb0] : () -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: entry block of a region may not have predecessors
diff --git a/Test/Verifier/graph_region_multi_block.mlir b/Test/Verifier/graph_region_multi_block.mlir
new file mode 100644
index 000000000..f5bda60a1
--- /dev/null
+++ b/Test/Verifier/graph_region_multi_block.mlir
@@ -0,0 +1,15 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// builtin.module is a registered op with a graph region, so its region may have
+// at most one block. (Unregistered ops and the test dialect are exempt and may
+// use multi-block graph regions.)
+
+"builtin.module"() ({
+^bb0:
+  "func.func"() <{function_type = () -> (), sym_name = "a"}> ({ ^e0: "func.return"() : () -> () }) : () -> ()
+^bb1:
+  "func.func"() <{function_type = () -> (), sym_name = "b"}> ({ ^e1: "func.return"() : () -> () }) : () -> ()
+}) : () -> ()
+
+// CHECK: expects graph region 0 to have 0 or 1 blocks
diff --git a/Test/Verifier/isolation_from_above.mlir b/Test/Verifier/isolation_from_above.mlir
new file mode 100644
index 000000000..4a6eddf0e
--- /dev/null
+++ b/Test/Verifier/isolation_from_above.mlir
@@ -0,0 +1,20 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// func.func is isolated from above: the body of @inner may not reference %k,
+// which is defined in the enclosing function @outer.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = () -> (), sym_name = "outer"}> ({
+  ^bb0():
+    %k = "arith.constant"() <{"value" = 1 : i64}> : () -> i64
+    "func.func"() <{function_type = () -> (), sym_name = "inner"}> ({
+    ^bb1():
+      "test.test"(%k) : (i64) -> ()
+      "func.return"() : () -> ()
+    }) : () -> ()
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: uses a value defined outside the isolated region
diff --git a/Test/Verifier/isolation_nested_region_ok.mlir b/Test/Verifier/isolation_nested_region_ok.mlir
new file mode 100644
index 000000000..79564c6e4
--- /dev/null
+++ b/Test/Verifier/isolation_nested_region_ok.mlir
@@ -0,0 +1,20 @@
+// RUN: veir-opt %s | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// A non-isolated nested region (the body of an unregistered test.test op) may
+// reference values from an enclosing region. Only IsolatedFromAbove ops, such as
+// func.func, form a barrier, so this program verifies.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = (i64) -> (), sym_name = "f"}> ({
+  ^bb0(%a : i64):
+    "test.test"() ({
+    ^bb1():
+      "test.test"(%a) : (i64) -> ()
+    }) : () -> ()
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK:      ^{{.*}}(%[[A:.*]] : i64):
+// CHECK:        "test.test"(%[[A]]) : (i64) -> ()
diff --git a/Test/Verifier/ssa_single_assignment.mlir b/Test/Verifier/ssa_single_assignment.mlir
new file mode 100644
index 000000000..a797bf94a
--- /dev/null
+++ b/Test/Verifier/ssa_single_assignment.mlir
@@ -0,0 +1,16 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// SSA requires that each name is assigned exactly once. Defining %a twice is
+// rejected by the parser, before verification runs.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = () -> i32, sym_name = "main"}> ({
+  ^bb0():
+    %a = "arith.constant"() <{"value" = 0 : i32}> : () -> i32
+    %a = "arith.constant"() <{"value" = 1 : i32}> : () -> i32
+    "func.return"(%a) : (i32) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: value %a has already been defined
diff --git a/Test/Verifier/ssa_undefined_value.mlir b/Test/Verifier/ssa_undefined_value.mlir
new file mode 100644
index 000000000..5674f26c1
--- /dev/null
+++ b/Test/Verifier/ssa_undefined_value.mlir
@@ -0,0 +1,14 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// Every used SSA name must be defined somewhere. A use of a name that is never
+// assigned is rejected by the parser, before verification runs.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = () -> i32, sym_name = "main"}> ({
+  ^bb0():
+    "func.return"(%missing) : (i32) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: use of undefined value %missing
diff --git a/Test/Verifier/successor_nonterminator_not_last.mlir b/Test/Verifier/successor_nonterminator_not_last.mlir
new file mode 100644
index 000000000..5208a6f3f
--- /dev/null
+++ b/Test/Verifier/successor_nonterminator_not_last.mlir
@@ -0,0 +1,19 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+// RUN: VEIR_MLIR_SAME_VERDICT
+
+// MLIR's generic verifier requires any operation with block successors to
+// terminate its parent block, even if the operation is not a registered
+// terminator. Otherwise non-terminator ops can smuggle CFG edges that ordinary
+// terminator-based analyses do not see.
+
+"builtin.module"() ({
+  "func.func"() <{function_type = () -> (), sym_name = "main"}> ({
+  ^entry:
+    "test.test"() [^side] : () -> ()
+    "func.return"() : () -> ()
+  ^side:
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK: operation with block successors must terminate its parent block
diff --git a/Test/lit.cfg b/Test/lit.cfg
index e65a71b88..d34521221 100644
--- a/Test/lit.cfg
+++ b/Test/lit.cfg
@@ -57,12 +57,19 @@ if mlir_opt:
 	#    messages. We'd rather test the error message of `veir-opt`.
     config.substitutions.append(("MLIR_INVALID",
      "not mlir-opt --mlir-print-op-generic --mlir-print-local-scope %s"))
+    # Assert that veir-opt and mlir-opt reach the same accept/reject verdict on
+    # %s. Backed by a helper script so we can compare exit codes (lit's internal
+    # shell cannot). Only the verdict is compared, not the diagnostic text.
+    config.substitutions.append(("VEIR_MLIR_SAME_VERDICT",
+     f"bash {veir_root}/Test/Tools/veir_mlir_same_verdict.sh {veir_root}/.lake/build/bin/veir-opt{exe_suffix} {mlir_opt} %s"))
   else:
     print(f"'mlir-opt' version {version_short} ({version}) detected, but only {mlir_versions_supported} supported. Skipping MLIR compatibility tests")
     config.substitutions.append(("MLIR_ROUNDTRIP", "true"))
     config.substitutions.append(("MLIR_UNREGISTERED_ROUNDTRIP", "true"))
     config.substitutions.append(("MLIR_INVALID", "true"))
+    config.substitutions.append(("VEIR_MLIR_SAME_VERDICT", "true"))
 else:
   config.substitutions.append(("MLIR_ROUNDTRIP", "true"))
   config.substitutions.append(("MLIR_UNREGISTERED_ROUNDTRIP", "true"))
   config.substitutions.append(("MLIR_INVALID", "true"))
+  config.substitutions.append(("VEIR_MLIR_SAME_VERDICT", "true"))
diff --git a/UnitTest/DataFlowFramework/Dominance.lean b/UnitTest/DataFlowFramework/Dominance.lean
index 298a28343..3038732f7 100644
--- a/UnitTest/DataFlowFramework/Dominance.lean
+++ b/UnitTest/DataFlowFramework/Dominance.lean
@@ -19,6 +19,24 @@ private structure ExpectedOperationDominance where
   dominates : Bool
   properDom : Bool
 
+/--
+Whether `block` lies in a graph region. In graph regions there is no SSA source
+order, so dominance is reflexive even for the proper variant: a block (or op)
+properly dominates itself, and a dominator properly dominates every block it
+dominates, including itself.
+-/
+private def blockInGraphRegion (block : BlockPtr) (irCtx : IRContext OpCode) : Bool :=
+  match (block.get! irCtx).parent with
+  | some region =>
+    match (region.get! irCtx).parent with
+    | some parentOp =>
+      let parent := parentOp.get! irCtx
+      match parent.opType.getRegionKind (parent.regions.idxOf region) with
+      | .Graph => true
+      | .SSACFG => false
+    | none => false
+  | none => false
+
 /--
 Compare one expected dominator label against the observed dominance information.
 
@@ -34,11 +52,14 @@ private def compareExpectedDominator
     (irCtx : IRContext OpCode) : MismatchReport := Id.run do
   let some expectedBlock := recovered.blocks[expectedDom]?
     | return #[s!"dominators {expected.name}: missing block label {expectedDom}"]
-  let shouldProperlyDom := expectedDom ≠ expected.name
+  -- In a graph region every dominator (including the block itself) properly
+  -- dominates the block; in an SSACFG region a block does not properly dominate
+  -- itself.
+  let shouldProperlyDom := blockInGraphRegion block irCtx || expectedDom ≠ expected.name
   let mut report := #[]
-  if !expectedBlock.dominates block dfCtx irCtx then
+  if !expectedBlock.dominatesByAnalysis block dfCtx irCtx then
     report := report.push s!"dominators {expected.name}: missing expected dominator {expectedDom}"
-  if expectedBlock.properlyDominates block dfCtx irCtx ≠ shouldProperlyDom then
+  if expectedBlock.properlyDominatesByAnalysis block dfCtx irCtx ≠ shouldProperlyDom then
     report := report.push
       s!"dominators {expected.name}: unexpected properlyDominates result for {expectedDom}"
   return report
@@ -56,15 +77,18 @@ private def compareObservedDominator
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
     (irCtx : IRContext OpCode) : MismatchReport := Id.run do
-  let observedByRelation := observedBlock.dominates block dfCtx irCtx
-  let observedProperly := observedBlock.properlyDominates block dfCtx irCtx
+  let inGraph := blockInGraphRegion block irCtx
+  let observedByRelation := observedBlock.dominatesByAnalysis block dfCtx irCtx
+  let observedProperly := observedBlock.properlyDominatesByAnalysis block dfCtx irCtx
   let mut report := #[]
-  if observedProperly ≠ (observedByRelation && observedBlock ≠ block) then
+  -- In a graph region proper dominance coincides with dominance (self included);
+  -- in an SSACFG region a block does not properly dominate itself.
+  if observedProperly ≠ (observedByRelation && (inGraph || observedBlock ≠ block)) then
     report := report.push
       s!"dominators {expected.name}: dominates/properlyDominates disagree on {observedName}"
   if observedByRelation && !expected.doms.contains observedName then
     report := report.push s!"dominators {expected.name}: unexpected dominator {observedName}"
-  if observedProperly && (!expected.doms.contains observedName || observedName = expected.name) then
+  if observedProperly && (!expected.doms.contains observedName || (!inGraph && observedName = expected.name)) then
     report := report.push s!"dominators {expected.name}: unexpected proper dominator {observedName}"
   report
 
@@ -173,8 +197,8 @@ private def compareOperationDominance
   let some dominated := getNamedOperation? recovered expected.dominated irCtx
     | return #[s!"op dominance {expected.dominator}->{expected.dominated}: missing dominated op"]
 
-  let observedDominates := dominator.dominates dominated dfCtx irCtx
-  let observedProperly := dominator.properlyDominates dominated dfCtx irCtx
+  let observedDominates := dominator.dominatesByAnalysis dominated dfCtx irCtx
+  let observedProperly := dominator.properlyDominatesByAnalysis dominated dfCtx irCtx
   let mut report := #[]
   if observedDominates ≠ expected.dominates then
     report := report.push
@@ -252,14 +276,14 @@ def runOperationDominance
 -/
 def testDomLoop : String :=
   run
-    "\"builtin.module\"() ({\n\
-^bb0:\n\
-  \"test.test\"() [^bb1] : () -> ()\n\
-^bb1:\n\
-  \"test.test\"() [^bb2] : () -> ()\n\
-^bb2:\n\
-  \"test.test\"() [^bb1] : () -> ()\n\
-}) : () -> ()"
+    r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({
+^bb0:
+  "test.test"() [^bb1] : () -> ()
+^bb1:
+  "test.test"() [^bb2] : () -> ()
+^bb2:
+  "test.test"() [^bb1] : () -> ()
+}) : () -> ()"#
     #[ { name := "bb0", doms := { "bb0" },               immediateDom := "bb0" }
      , { name := "bb1", doms := { "bb0", "bb1" },        immediateDom := "bb0" }
      , { name := "bb2", doms := { "bb0", "bb1", "bb2" }, immediateDom := "bb1" }
@@ -279,16 +303,16 @@ def testDomLoop : String :=
 -/
 def testDomDiamond : String :=
   run
-    "\"builtin.module\"() ({\n\
-^bb0:\n\
-  \"test.test\"() [^bb1, ^bb2] : () -> ()\n\
-^bb1:\n\
-  \"test.test\"() [^bb3] : () -> ()\n\
-^bb2:\n\
-  \"test.test\"() [^bb3] : () -> ()\n\
-^bb3:\n\
-  \"test.test\"() : () -> ()\n\
-}) : () -> ()"
+    r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({
+^bb0:
+  "test.test"() [^bb1, ^bb2] : () -> ()
+^bb1:
+  "test.test"() [^bb3] : () -> ()
+^bb2:
+  "test.test"() [^bb3] : () -> ()
+^bb3:
+  "test.test"() : () -> ()
+}) : () -> ()"#
     #[ { name := "bb0", doms := { "bb0" },        immediateDom := "bb0" }
      , { name := "bb1", doms := { "bb0", "bb1" }, immediateDom := "bb0" }
      , { name := "bb2", doms := { "bb0", "bb2" }, immediateDom := "bb0" }
@@ -315,16 +339,16 @@ def testDomDiamond : String :=
 -/
 def testDomLine : String :=
   run
-    "\"builtin.module\"() ({\n\
-^bb0:\n\
-  \"test.test\"() [^bb1] : () -> ()\n\
-^bb1:\n\
-  \"test.test\"() [^bb2] : () -> ()\n\
-^bb2:\n\
-  \"test.test\"() [^bb3] : () -> ()\n\
-^bb3:\n\
-  \"test.test\"() : () -> ()\n\
-}) : () -> ()"
+    r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({
+^bb0:
+  "test.test"() [^bb1] : () -> ()
+^bb1:
+  "test.test"() [^bb2] : () -> ()
+^bb2:
+  "test.test"() [^bb3] : () -> ()
+^bb3:
+  "test.test"() : () -> ()
+}) : () -> ()"#
     #[ { name := "bb0", doms := { "bb0" },                      immediateDom := "bb0" }
      , { name := "bb1", doms := { "bb0", "bb1" },               immediateDom := "bb0" }
      , { name := "bb2", doms := { "bb0", "bb1", "bb2" },        immediateDom := "bb1" }
@@ -351,24 +375,24 @@ def testDomLine : String :=
 -/
 def testDomIfLoopIf : String :=
   run
-    "\"builtin.module\"() ({\n\
-^bb0:\n\
-  \"test.test\"() [^bb1, ^bb2] : () -> ()\n\
-^bb1:\n\
-  \"test.test\"() [^bb5] : () -> ()\n\
-^bb2:\n\
-  \"test.test\"() [^bb3, ^bb4] : () -> ()\n\
-^bb3:\n\
-  \"test.test\"() [^bb6] : () -> ()\n\
-^bb4:\n\
-  \"test.test\"() [^bb6] : () -> ()\n\
-^bb5:\n\
-  \"test.test\"() [^bb1, ^bb7] : () -> ()\n\
-^bb6:\n\
-  \"test.test\"() [^bb7] : () -> ()\n\
-^bb7:\n\
-  \"test.test\"() : () -> ()\n\
-}) : () -> ()"
+    r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({
+^bb0:
+  "test.test"() [^bb1, ^bb2] : () -> ()
+^bb1:
+  "test.test"() [^bb5] : () -> ()
+^bb2:
+  "test.test"() [^bb3, ^bb4] : () -> ()
+^bb3:
+  "test.test"() [^bb6] : () -> ()
+^bb4:
+  "test.test"() [^bb6] : () -> ()
+^bb5:
+  "test.test"() [^bb1, ^bb7] : () -> ()
+^bb6:
+  "test.test"() [^bb7] : () -> ()
+^bb7:
+  "test.test"() : () -> ()
+}) : () -> ()"#
     #[ { name := "bb0", doms := { "bb0" },               immediateDom := "bb0" }
      , { name := "bb1", doms := { "bb0", "bb1" },        immediateDom := "bb0" }
      , { name := "bb2", doms := { "bb0", "bb2" },        immediateDom := "bb0" }
@@ -424,7 +448,7 @@ def testDomNestedRegions : String :=
           └───────┘
 -/
 def testDomDiamondNestedJoin : String :=
-  run r#""builtin.module"() ({
+  run r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({
 ^bb0:
   "test.test"() [^bb1, ^bb2] : () -> ()
 ^bb1:
@@ -488,7 +512,7 @@ def testDomTwoLevelNested : String :=
   └────────┘
 -/
 def testDomDiamondLoop: String :=
-  run r#""builtin.module"() ({
+  run r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({
 ^bb0:
   "test.test"() [^bb1, ^bb2] : () -> ()
 ^bb1:
@@ -522,12 +546,15 @@ def testOpDomNestedRegions : String :=
     %siblingInner = "test.test"() : () -> i32
   }) : () -> i32
 }) : () -> ()"#
-    #[ { dominator := "outer",      dominated := "outer",        dominates := true,  properDom := false }
+    #[ -- `outer` and `otherOuter` share the module's graph region, so source order
+       -- is ignored: each properly dominates itself and `otherOuter` dominates
+       -- `inner` (nested in `outer`) despite appearing later.
+       { dominator := "outer",      dominated := "outer",        dominates := true,  properDom := true  }
      , { dominator := "outer",      dominated := "inner",        dominates := true,  properDom := true  }
      , { dominator := "outer",      dominated := "otherOuter",   dominates := true,  properDom := true  }
      , { dominator := "outer",      dominated := "siblingInner", dominates := true,  properDom := true  }
      , { dominator := "inner",      dominated := "siblingInner", dominates := false, properDom := false }
-     , { dominator := "otherOuter", dominated := "inner",        dominates := false, properDom := false }
+     , { dominator := "otherOuter", dominated := "inner",        dominates := true,  properDom := true  }
      , { dominator := "otherOuter", dominated := "siblingInner", dominates := true,  properDom := true  }
      ]
 
@@ -548,28 +575,23 @@ def testOpDomTwoLevelNested : String :=
     #[ { dominator := "top",    dominated := "middle", dominates := true, properDom := true  }
      , { dominator := "top",    dominated := "leaf",   dominates := true, properDom := true  }
      , { dominator := "middle", dominated := "leaf",   dominates := true, properDom := true  }
-     , { dominator := "leaf",   dominated := "leaf",   dominates := true, properDom := false }
+     , { dominator := "leaf",   dominated := "leaf",   dominates := true, properDom := true  }
      ]
 
 /-
   Test: operation dominance across two blocks in the same nested region.
 -/
 def testOpDomSameRegionTwoBlocks : String :=
-  runOperationDominance r#""builtin.module"() ({
-^bb0:
-  %outer = "test.test"() ({
-  ^bb1:
-    %entry = "test.test"() : () -> i32
-    "test.test"() [^bb2] : () -> ()
-  ^bb2:
-    %exit = "test.test"() : () -> i32
-  }) : () -> i32
+  runOperationDominance r#""func.func"() <{function_type = () -> (), sym_name = "f"}> ({
+^bb1:
+  %entry = "test.test"() : () -> i32
+  "test.test"() [^bb2] : () -> ()
+^bb2:
+  %exit = "test.test"() : () -> i32
 }) : () -> ()"#
     #[ { dominator := "entry", dominated := "entry", dominates := true,  properDom := false }
      , { dominator := "entry", dominated := "exit",  dominates := true,  properDom := true  }
      , { dominator := "exit",  dominated := "entry", dominates := false, properDom := false }
-     , { dominator := "outer", dominated := "entry", dominates := true,  properDom := true  }
-     , { dominator := "outer", dominated := "exit",  dominates := true,  properDom := true  }
      ]
 /--
 info: "ok"
diff --git a/Veir/Dominance.lean b/Veir/Dominance.lean
index 9ec6c198b..8f87f98dd 100644
--- a/Veir/Dominance.lean
+++ b/Veir/Dominance.lean
@@ -119,6 +119,16 @@ SSA dominance.
 /--
   A predicate that states that the values in the IR context are used in operations that
   are dominated by the operation or block that defines them.
+
+  `WfIRContext.verifyDominance` (in `Veir/Verifier.lean`) is the executable decision
+  procedure for this predicate: it visits every in-bounds operation and every operand,
+  and for each checks `value.dominatesIp (InsertPoint.before op) ctx` via the dominance
+  analysis. A successful run is intended to witness exactly `ctx.Dom`; the checker is
+  written so that each step matches a clause of this definition for reachable SSACFG
+  blocks. For graph regions, the executable checker follows MLIR's region-aware
+  dominance rule: same-block order is ignored inside the graph region, but values
+  captured into its entry block must still dominate the graph-owning operation. As in
+  MLIR, the check is skipped for blocks that are unreachable from their region's entry.
 -/
 def WfIRContext.Dom (ctx : WfIRContext OpInfo) : Prop :=
   ∀ {op : OperationPtr} (_opInBounds : op.InBounds ctx.raw) {value : ValuePtr},
diff --git a/Veir/GlobalOpInfo.lean b/Veir/GlobalOpInfo.lean
index a66965a8b..ee42d2b3b 100644
--- a/Veir/GlobalOpInfo.lean
+++ b/Veir/GlobalOpInfo.lean
@@ -370,6 +370,19 @@ def OpCode.getRegionKind (opCode : OpCode) (_index : Nat) : RegionKind :=
   | .test .test => .Graph
   | _ => .SSACFG
 
+/--
+  Whether this operation defines `IsolatedFromAbove` regions: operations nested
+  inside its regions may not reference SSA values defined outside the operation.
+  This mirrors MLIR, where symbol-table ops like modules and functions are
+  isolated from above.
+-/
+def OpCode.isIsolatedFromAbove (opCode : OpCode) : Bool :=
+  match opCode with
+  | .builtin .module
+  | .func .func
+  | .llvm .func => true
+  | _ => false
+
 /--
   Does this OpCode count as an MLIR basic block terminator?
 -/
diff --git a/Veir/IR/Dominance.lean b/Veir/IR/Dominance.lean
index ff95fa532..730a3bae4 100644
--- a/Veir/IR/Dominance.lean
+++ b/Veir/IR/Dominance.lean
@@ -26,6 +26,20 @@ private partial def normalizeInsertPoint
   let parentOp ← (parentRegion.get! irCtx).parent
   normalizeInsertPoint region (.before parentOp) irCtx
 
+/--
+Whether this region has MLIR-style SSA dominance. In graph regions, operations
+in the same block may use each other without respecting source order, but values
+defined outside the graph region must still dominate the operation that owns the
+graph region.
+-/
+private def RegionPtr.hasSSADominanceByKind
+    (region : RegionPtr) (irCtx : IRContext OpCode) : Bool :=
+  match (region.get! irCtx).parent with
+  | some parentOp =>
+    let parent := parentOp.get! irCtx
+    parent.opType.getRegionKind (parent.regions.idxOf region) = .SSACFG
+  | none => true
+
 /--
 Check dominance between two blocks that are already known
 to lie in the same region.
@@ -38,10 +52,14 @@ private partial def BlockPtr.dominatesWithinRegion
     (dfCtx : DataFlowContext)
     (irCtx : IRContext OpCode) : Bool := Id.run do
   if dominator = block then
-    true
-  else
-    let some idom := block.getIDom? dfCtx irCtx | return false
-    idom ≠ block && dominatesWithinRegion dominator idom dfCtx irCtx
+    return true
+  -- In a graph region there is no block ordering, so every block dominates every
+  -- other block in the region.
+  if let some region := (block.get! irCtx).parent then
+    if !region.hasSSADominanceByKind irCtx then
+      return true
+  let some idom := block.getIDom? dfCtx irCtx | return false
+  return idom ≠ block && dominatesWithinRegion dominator idom dfCtx irCtx
 
 
 /--
@@ -70,6 +88,10 @@ to lie in the same block.
 private def dominatesWithinBlock
     (dominator point : InsertPoint)
     (irCtx : IRContext OpCode) : Bool := Id.run do
+  let some block := dominator.block! irCtx | return false
+  let some region := (block.get! irCtx).parent | return false
+  if !region.hasSSADominanceByKind irCtx then
+    return true
   if dominator = point then
     return true
   match dominator, point with
@@ -116,6 +138,13 @@ private def dominates
 /--
 Proper dominance query between two insertion points.
 
+From the MLIR documentation: "If A and B are in the same block and A
+properly dominates B within the block, or if the block that contains A
+properly dominates the block that contains B. In an SSACFG region,
+Operation A dominates Operation B in the same block if A preceeds
+B. In a Graph region, all operations in a block properly dominate all
+operations in the same block."
+
 An insertion point does not properly dominate itself. Otherwise this is the same query as `InsertPoint.dominates`.
 -/
 private def properlyDominates
@@ -123,7 +152,15 @@ private def properlyDominates
     (point : InsertPoint)
     (dfCtx : DataFlowContext)
     (irCtx : IRContext OpCode) : Bool :=
-  dominator ≠ point && dominator.dominates point dfCtx irCtx
+  if dominator = point then
+    match dominator.block! irCtx with
+    | some block =>
+      match (block.get! irCtx).parent with
+      | some region => !region.hasSSADominanceByKind irCtx
+      | none => false
+    | none => false
+  else
+    dominator.dominates point dfCtx irCtx
 
 
 end InsertPoint
@@ -144,7 +181,7 @@ def immediateDominator?
 /--
 Dominance query between two blocks, where a block dominates itself.
 -/
-def dominates
+def dominatesByAnalysis
     [FactSpec .dominator]
     (dominator block : BlockPtr)
     (dfCtx : DataFlowContext)
@@ -154,7 +191,7 @@ def dominates
 /--
 Dominance query between two blocks, where a block does not dominate itself.
 -/
-def properlyDominates
+def properlyDominatesByAnalysis
     [FactSpec .dominator]
     (dominator block : BlockPtr)
     (dfCtx : DataFlowContext)
@@ -169,7 +206,7 @@ namespace OperationPtr
 /--
 Dominance query between two operations, where an operation dominates itself.
 -/
-def dominates
+def dominatesByAnalysis
     (dominator op : OperationPtr)
     (dfCtx : DataFlowContext)
     (irCtx : IRContext OpCode) : Bool :=
@@ -178,7 +215,7 @@ def dominates
 /--
 Dominance query between two operations, where an operation does not dominate itself.
 -/
-def properlyDominates
+def properlyDominatesByAnalysis
     (dominator op : OperationPtr)
     (dfCtx : DataFlowContext)
     (irCtx : IRContext OpCode) : Bool :=
diff --git a/Veir/Pass.lean b/Veir/Pass.lean
index 488b6537d..4ce5f9b9a 100644
--- a/Veir/Pass.lean
+++ b/Veir/Pass.lean
@@ -67,7 +67,7 @@ def run (pipeline : PassPipeline OpCode)
     if h : moduleOp.InBounds currentCtx.raw then
       let ctx' ← try pass.run currentCtx moduleOp h
                  catch errMsg => throw s!"pass '{pass.name}' failed: {errMsg}"
-      if let .error errMsg := ctx'.verify then
+      if let .error errMsg := WfIRContext.verify ctx' (some moduleOp) then
         throw s!"verification failed after pass '{pass.name}': {errMsg}"
       currentCtx := ctx'
     else
diff --git a/Veir/Verifier.lean b/Veir/Verifier.lean
index 3172b8f17..66b1cc485 100644
--- a/Veir/Verifier.lean
+++ b/Veir/Verifier.lean
@@ -1,6 +1,7 @@
 module
 
 public import Veir.IR.Basic
+public import Veir.IR.Dominance
 public import Veir.IR.Fields
 public import Veir.Properties
 public import Veir.GlobalOpInfo
@@ -865,14 +866,125 @@ def RegionPtr.getRegionKind (region : RegionPtr) (ctx : WfIRContext OpCode) : Re
   | none => .SSACFG
 
 /--
-  Verify that a terminator only ever appears as the last operation of its block:
-  an operation that is a terminator must not be followed by another operation.
+  Verify operation/block control-flow position rules: a terminator only ever
+  appears as the last operation of its block, and any operation with block
+  successors must also terminate its parent block. The second rule matches
+  MLIR's generic verifier and catches malformed successor-bearing unknown/test
+  ops even when they are not registered terminators.
 -/
 def OperationPtr.verifyTerminatorPosition (op : OperationPtr) (ctx : WfIRContext OpCode)
     (opIn : op.InBounds ctx.raw) : Except String PUnit := do
   let operation := op.get ctx.raw opIn
   if operation.opType.isTerminator && operation.next.isSome then
     throw "Expected a terminator to be the last operation of its block"
+  if op.getNumSuccessors ctx.raw opIn ≠ 0 && operation.next.isSome then
+    throw "operation with block successors must terminate its parent block"
+
+/--
+  Verify that no operation branches to the entry block of a region. The entry
+  block of a region may not have predecessors: it is the unique block that the
+  region is entered through, and dominance assumes it dominates every other block
+  in the region.
+-/
+def OperationPtr.verifyDoesNotBranchToEntryBlock (op : OperationPtr) (ctx : WfIRContext OpCode)
+    (opIn : op.InBounds ctx.raw) : Except String PUnit := do
+  for succ in op.getSuccessors ctx.raw opIn do
+    match (succ.get! ctx.raw).parent with
+    | some region =>
+      if (region.get! ctx.raw).firstBlock = some succ then
+        throw "entry block of a region may not have predecessors"
+    | none => pure ()
+
+/--
+  Verify that every successor of an operation lies in the same region as the
+  operation itself. Control flow may not branch out of its enclosing region.
+
+  This cannot be expressed in the textual format (block labels are region-scoped,
+  so the parser already rejects a reference to a block in another region), but it
+  guards against passes that build malformed cross-region control flow.
+-/
+def OperationPtr.verifySuccessorsInSameRegion (op : OperationPtr) (ctx : WfIRContext OpCode)
+    (opIn : op.InBounds ctx.raw) : Except String PUnit := do
+  match (op.get ctx.raw opIn).parent with
+  | none => pure ()
+  | some block =>
+    let blockRegion := (block.get! ctx.raw).parent
+    for succ in op.getSuccessors ctx.raw opIn do
+      if (succ.get! ctx.raw).parent ≠ blockRegion then
+        throw "branching to a block of a different region"
+
+/--
+  Starting from `region` (the region containing a use) and walking outward, decide
+  whether an `IsolatedFromAbove` barrier is crossed before reaching `defRegion`
+  (the region containing the used value's definition). Reaching `defRegion` first
+  means the use is in scope; crossing a barrier first means the value escapes it.
+-/
+private partial def regionEscapesIsolation
+    (defRegion region : RegionPtr) (ctx : WfIRContext OpCode) : Bool :=
+  if region = defRegion then
+    false
+  else
+    match (region.get! ctx.raw).parent with
+    | none => false
+    | some parentOp =>
+      if (parentOp.getOpType! ctx.raw).isIsolatedFromAbove then
+        true
+      else
+        match (parentOp.get! ctx.raw).parent with
+        | none => false
+        | some parentBlock =>
+          match (parentBlock.get! ctx.raw).parent with
+          | none => false
+          | some parentRegion => regionEscapesIsolation defRegion parentRegion ctx
+
+/--
+  Verify the `IsolatedFromAbove` property: an operation nested inside an isolated
+  region may not use a value defined outside the nearest enclosing isolated
+  operation.
+-/
+def OperationPtr.verifyOperandIsolation (op : OperationPtr) (ctx : WfIRContext OpCode)
+    (opIn : op.InBounds ctx.raw) : Except String PUnit := do
+  match (op.get ctx.raw opIn).parent with
+  | none => pure ()
+  | some useBlock =>
+    match (useBlock.get! ctx.raw).parent with
+    | none => pure ()
+    | some useRegion =>
+      let instrName := String.fromUTF8! (op.getOpType ctx.raw opIn).name
+      for i in [0:op.getNumOperands ctx.raw opIn] do
+        let value := op.getOperand! ctx.raw i
+        let defBlock? : Option BlockPtr :=
+          match value with
+          | .opResult result => (result.op.get! ctx.raw).parent
+          | .blockArgument arg => some arg.block
+        match defBlock? with
+        | none => pure ()
+        | some defBlock =>
+          match (defBlock.get! ctx.raw).parent with
+          | none => pure ()
+          | some defRegion =>
+            if regionEscapesIsolation defRegion useRegion ctx then
+              throw s!"{instrName}: operand {i} ({reprStr value}) uses a value defined outside the isolated region that encloses its use"
+
+/--
+  Verify that graph regions of registered operations contain at most one block.
+  Like MLIR, this restriction limits the cases transforms must handle; it applies
+  only to registered operations, so unregistered ops and the test dialect may
+  still use multi-block graph regions.
+-/
+def OperationPtr.verifyGraphRegionBlockCount (op : OperationPtr) (ctx : WfIRContext OpCode)
+    (opIn : op.InBounds ctx.raw) : Except String PUnit := do
+  let opCode := op.getOpType ctx.raw opIn
+  match opCode with
+  | .builtin .unregistered | .test .test => pure ()
+  | _ =>
+    for i in [0:op.getNumRegions ctx.raw opIn] do
+      if opCode.getRegionKind i = .Graph then
+        match (op.getRegion! ctx.raw i |>.get! ctx.raw).firstBlock with
+        | some b =>
+          if (b.get! ctx.raw).next.isSome then
+            throw s!"expects graph region {i} to have 0 or 1 blocks"
+        | none => pure ()
 
 /--
   Check that a block is non-empty and its last operation is a
@@ -887,25 +999,135 @@ def BlockPtr.verifyTerminator (block : BlockPtr) (ctx : WfIRContext OpCode)
     if !(lastOp.getOpType! ctx.raw).isTerminator then
       throw "Expected the last operation of a block to be a terminator"
 
+/--
+  Decide the per-operand condition of `WfIRContext.Dom` (see `Veir/Dominance.lean`):
+  whether `value` dominates the program point immediately before `useOp`, i.e. the
+  proposition `value.dominatesIp (InsertPoint.before useOp) ctx`.
+
+  The two `ValuePtr` cases mirror the two ways a value is defined:
+
+  * `.opResult result` — the result is available immediately after `result.op`, so
+    it dominates the point before `useOp` exactly when `result.op` *strictly*
+    dominates `useOp` (mirroring `OperationPtr.dominatesIp_before`, which relates
+    `dominatesIp (.before _)` to `strictlyDominates`). `properlyDominatesByAnalysis`
+    decides precisely that strict-dominance fact.
+
+  * `.blockArgument arg` — a block argument is live from the top of `arg.block`, so
+    it dominates the point before `useOp` exactly when `arg.block` dominates
+    `useOp`'s block (reflexively — the same block counts, since the argument
+    precedes every operation in it). `dominatesByAnalysis` decides that.
+
+  So `dominatesBeforeOp? value useOp = true` is exactly the clause `ctx.Dom`
+  demands of the `(value, useOp)` pair.
+-/
+def ValuePtr.dominatesBeforeOp?
+    (value : ValuePtr) (useOp : OperationPtr)
+    (dfCtx : DataFlowContext) (ctx : IRContext OpCode) : Bool :=
+  match value with
+  | .opResult result =>
+      OperationPtr.properlyDominatesByAnalysis result.op useOp dfCtx ctx
+  | .blockArgument arg =>
+      match (useOp.get! ctx).parent with
+      | some useBlock => BlockPtr.dominatesByAnalysis arg.block useBlock dfCtx ctx
+      | none => false
+
+def OperationPtr.verifyOperandDominance
+    (op : OperationPtr) (ctx : WfIRContext OpCode)
+    (dfCtx : DataFlowContext) (opIn : op.InBounds ctx.raw) :
+    Except String PUnit := do
+  -- As in LLVM/MLIR, dominance is only checked in blocks reachable from their
+  -- region's entry. This matches MLIR's verifier, which gates the operand
+  -- dominance check on `DominanceInfo::isReachableFromEntry(block)`
+  -- (`mlir/lib/IR/Verifier.cpp`): the region's entry block is always reachable,
+  -- and every other block is reachable iff the region's dominator tree says so.
+  -- A block carries a dominator fact in exactly those cases, so fact presence is
+  -- the executable form of `isReachableFromEntry`.
+  --
+  -- A consequence, shared with MLIR, is that a use hidden in a *non-entry* block
+  -- of a graph region with no intra-region control-flow edges is unreachable and
+  -- therefore not checked, even if it captures a value that does not dominate the
+  -- graph-owning operation. (A capture used in the graph region's *entry* block
+  -- is still checked, because the entry block is always reachable.)
+  let shouldCheck : Bool := Id.run do
+    let some useBlock := (op.get ctx.raw opIn).parent | return false
+    return (useBlock.getDominatorFact? dfCtx ctx.raw).isSome
+  if shouldCheck then
+    let instrName := String.fromUTF8! (op.getOpType ctx.raw opIn).name
+    -- The inner `∀ value ∈ op.getOperands!` of `ctx.Dom`: these indices enumerate
+    -- exactly `op.getOperands!`, and `dominatesBeforeOp?` decides the required
+    -- `value.dominatesIp (InsertPoint.before op) ctx` for each one.
+    for i in [0:op.getNumOperands ctx.raw opIn] do
+      let value := op.getOperand! ctx.raw i
+      if !value.dominatesBeforeOp? op dfCtx ctx.raw then
+        throw s!"{instrName}: operand {i} ({reprStr value}) does not dominate its use in operation {reprStr op}"
+
+/--
+  Executable decision procedure for `WfIRContext.Dom` (defined in `Veir/Dominance.lean`).
+
+  `ctx.Dom` is:
+
+      ∀ (op) (_ : op.InBounds ctx.raw) (value),
+        value ∈ op.getOperands! ctx.raw →
+        value.dominatesIp (InsertPoint.before op) ctx
+
+  and this checker discharges that proposition clause for clause:
+
+  * `forOpsDepM` visits every in-bounds operation — the outer `∀ op`.
+  * `verifyOperandDominance` iterates `op`'s operands — the inner
+    `∀ value ∈ op.getOperands!`.
+  * `ValuePtr.dominatesBeforeOp?` decides `value.dominatesIp (InsertPoint.before op) ctx`
+    for each operand (see its docstring for the `opResult`/`blockArgument` cases).
+
+  Therefore `verifyDominance ctx top = .ok ()` means every operand of every operation
+  in a reachable block dominates its use according to the region-aware dominance
+  relation used by MLIR: SSACFG regions enforce control-flow and same-block order,
+  graph regions ignore same-block order, and values captured into the *entry* block of
+  a graph region must still dominate the enclosing operation in the parent region. As in
+  MLIR, blocks that are not reachable from their region's entry are not checked, so a
+  capture used in a non-entry, edgeless graph-region block is left unverified.
+
+  This is still an executable checker, not a Lean proof of `ctx.Dom`; it is written so
+  that each step lines up with a clause of the definition, which is what makes the
+  implication "the check succeeds ⇒ `ctx.Dom`" clear.
+-/
+def WfIRContext.verifyDominance
+    (ctx : WfIRContext OpCode) (top : OperationPtr) : Except String Unit := do
+  if _ : top.InBounds ctx.raw then
+    let some dfCtx := fixpointSolve top #[DominanceAnalysis] ctx.raw
+      | throw "dominance analysis did not terminate"
+    ctx.raw.forOpsDepM fun op opIn =>
+      op.verifyOperandDominance ctx dfCtx opIn
+  else
+    throw s!"dominance root operation is not in bounds: {reprStr top}"
+
 public section
 
 /--
-  Verify that all operations in the IRContext satisfy their local invariants.
+  Verify that all operations in the IRContext satisfy their local invariants. If `top?` is
+  provided, also run the dynamic SSA dominance checker rooted at that operation.
 -/
-def WfIRContext.verify (ctx : WfIRContext OpCode) : Except String Unit := do
+def WfIRContext.verify (ctx : WfIRContext OpCode)
+    (top? : Option OperationPtr := none) : Except String Unit := do
   ctx.raw.forOpsDepM (fun op opIn => do
     op.verifyLocalInvariants ctx opIn
     if let .riscv _ := op.getOpType ctx.raw opIn then
       op.verifyRISCVRegisterTypes ctx opIn
     match (op.get ctx.raw opIn).parent with
     | some _ => op.verifyTerminatorPosition ctx opIn
-    | none => pure ())
+    | none => pure ()
+    op.verifyDoesNotBranchToEntryBlock ctx opIn
+    op.verifySuccessorsInSameRegion ctx opIn
+    op.verifyGraphRegionBlockCount ctx opIn
+    op.verifyOperandIsolation ctx opIn)
   ctx.raw.forBlocksDepM (fun block blockIn => do
     match (block.get ctx.raw blockIn).parent with
     | some region =>
       if region.getRegionKind ctx = .SSACFG then
         block.verifyTerminator ctx blockIn
     | none => pure ())
+  match top? with
+  | some top => ctx.verifyDominance top
+  | none => pure ()
 
 /--
 Assert that all operations in the IRContext satisfy their local invariants.
diff --git a/VeirInterpret.lean b/VeirInterpret.lean
index 7ee81de89..d7525875a 100644
--- a/VeirInterpret.lean
+++ b/VeirInterpret.lean
@@ -97,7 +97,7 @@ def main (args : List String) : IO Unit := do
   | [filename] =>
     match ← parseOperation filename with
     | .ok (ctx, op) =>
-      match ctx.verify with
+      match WfIRContext.verify ctx (some op) with
       | .ok _ =>
         let rawCtx : IRContext OpCode := ctx
         let mainOp ← resolveEntryPoint rawCtx op
diff --git a/VeirOpt.lean b/VeirOpt.lean
index ef56fd1fa..ef1f24dac 100644
--- a/VeirOpt.lean
+++ b/VeirOpt.lean
@@ -134,7 +134,7 @@ def main (args : List String) : IO Unit := do
       IO.eprintln errMsg
       IO.Process.exit 1
     | .ok (ctx, op) =>
-      match ctx.verify with
+      match WfIRContext.verify ctx (some op) with
       | .error errMsg =>
         IO.eprintln s!"Error verifying input program: {errMsg}"
         IO.Process.exit 1