diff --git a/reuse-mlir/include/ReuseIR/IR/ReuseIRTypes.h b/reuse-mlir/include/ReuseIR/IR/ReuseIRTypes.h
index 6b95091..eb6ccf6 100644
--- a/reuse-mlir/include/ReuseIR/IR/ReuseIRTypes.h
+++ b/reuse-mlir/include/ReuseIR/IR/ReuseIRTypes.h
@@ -14,6 +14,7 @@
 #include "mlir/Support/LLVM.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/TypeSwitch.h"
 #include "llvm/Support/Alignment.h"
 #include "llvm/Support/TypeSize.h"
 #include <algorithm>
@@ -30,3 +31,14 @@ void populateLLVMTypeConverter(CompositeLayoutCache &cache,
                                mlir::LLVMTypeConverter &converter);
 } // namespace reuse_ir
 } // namespace mlir
+
+namespace mlir {
+namespace REUSE_IR_DECL_SCOPE {
+inline bool isProjectable(mlir::Type type) {
+  return llvm::TypeSwitch<mlir::Type, bool>(type)
+      .Case<CompositeType>([](auto &&) { return true; })
+      .Case<ArrayType>([](auto &&) { return true; })
+      .Default([](auto &&) { return false; });
+}
+} // namespace REUSE_IR_DECL_SCOPE
+} // namespace mlir
\ No newline at end of file
diff --git a/reuse-mlir/src/cxx/IR/ReuseIROps.cpp b/reuse-mlir/src/cxx/IR/ReuseIROps.cpp
index 4acf212..9415f8e 100644
--- a/reuse-mlir/src/cxx/IR/ReuseIROps.cpp
+++ b/reuse-mlir/src/cxx/IR/ReuseIROps.cpp
@@ -40,18 +40,35 @@ mlir::reuse_ir::LogicalResult ValueToRefOp::verify() {
                        "same type of the input");
   return mlir::reuse_ir::success();
 }
+
 // ProjOp
 mlir::reuse_ir::LogicalResult ProjOp::verify() {
-  mlir::Type innerType;
-  if (auto type = llvm::dyn_cast<RefType>(getObject().getType()))
-    innerType = type.getPointee();
-
-  if (auto type = llvm::dyn_cast<RcType>(getObject().getType()))
-    innerType = type.getPointee();
-
-  innerType = innerType ? innerType : getObject().getType();
+  RefType input = getObject().getType();
+  if (!isProjectable(input.getPointee()))
+    return emitOpError("must operate on a reference to a composite or an array");
+  auto targetType =
+      llvm::TypeSwitch<mlir::Type, mlir::Type>(input.getPointee())
+          .Case<CompositeType>([&](const CompositeType &ty) {
+            size_t size = ty.getMemberTypes().size();
+            return getIndex() < size ? ty.getMemberTypes()[getIndex()]
+                                     : mlir::Type{};
+          })
+          .Case<ArrayType>([&](const ArrayType &ty) {
+            if (getIndex() >= ty.getSizes()[0])
+              return mlir::Type{};
+            if (ty.getSizes().size() == 0)
+              return ty.getElementType();
+            return cast<mlir::Type>(ArrayType::get(
+                getContext(), ty.getElementType(), ty.getSizes().drop_front()));
+          })
+          .Default([](auto &&) { return mlir::Type{}; });
+  if (!targetType)
+    return emitOpError("cannot project with an out-of-bound index");
+  if (targetType != getType().getPointee())
+    return emitOpError("expected to return a reference to ")
+           << targetType << ", but found a reference to "
+           << getType().getPointee();
 
-  // TODO: handle verification recursively.
   return mlir::reuse_ir::success();
 }
 
diff --git a/reuse-mlir/test/integration/basic/invalid_projection_index.mlir b/reuse-mlir/test/integration/basic/invalid_projection_index.mlir
new file mode 100644
index 0000000..06bcc38
--- /dev/null
+++ b/reuse-mlir/test/integration/basic/invalid_projection_index.mlir
@@ -0,0 +1,13 @@
+// RUN: %not %reuse-opt %s 2>&1 | %FileCheck %s
+!test = !reuse_ir.composite<!reuse_ir.composite<i32, i32, f128>, i32>
+module @test {
+    func.func @projection(%0: !reuse_ir.rc<!test, nonatomic, nonfreezing>) {
+        %1 = reuse_ir.borrow %0 : 
+            !reuse_ir.rc<!test, nonatomic, nonfreezing>
+            -> !reuse_ir.ref<!test, nonfreezing>
+        // CHECK: error: 'reuse_ir.proj' op cannot project with an out-of-bound index
+        %2 = reuse_ir.proj %1[114514] : 
+            !reuse_ir.ref<!test, nonfreezing> -> !reuse_ir.ref<!reuse_ir.composite<i32, i32>, nonfreezing>
+        return
+    }
+}
diff --git a/reuse-mlir/test/integration/basic/invalid_projection_type.mlir b/reuse-mlir/test/integration/basic/invalid_projection_type.mlir
new file mode 100644
index 0000000..58db033
--- /dev/null
+++ b/reuse-mlir/test/integration/basic/invalid_projection_type.mlir
@@ -0,0 +1,13 @@
+// RUN: %not %reuse-opt %s 2>&1 | %FileCheck %s
+!test = !reuse_ir.composite<!reuse_ir.composite<i32, i32, f128>, i32>
+module @test {
+    func.func @projection(%0: !reuse_ir.rc<!test, nonatomic, nonfreezing>) {
+        %1 = reuse_ir.borrow %0 : 
+            !reuse_ir.rc<!test, nonatomic, nonfreezing>
+            -> !reuse_ir.ref<!test, nonfreezing>
+        // CHECK: error: 'reuse_ir.proj' op expected to return a reference to '!reuse_ir.composite<i32, i32, f128>', but found a reference to '!reuse_ir.composite<i32, i32>'
+        %2 = reuse_ir.proj %1[0] : 
+            !reuse_ir.ref<!test, nonfreezing> -> !reuse_ir.ref<!reuse_ir.composite<i32, i32>, nonfreezing>
+        return
+    }
+}