diff --git a/apps/sel4test-tests/src/tests/vcpu.c b/apps/sel4test-tests/src/tests/vcpu.c
new file mode 100644
index 00000000..2ee4781b
--- /dev/null
+++ b/apps/sel4test-tests/src/tests/vcpu.c
@@ -0,0 +1,26 @@
+/*
+ * Copyright 2023
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+/* This file contains tests related to vCPU syscalls. */
+
+#include <stdio.h>
+#include <sel4/sel4.h>
+#include <sel4test/testutil.h>
+#include <sel4test/macros.h>
+
+#include "../helpers.h"
+
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+int test_vcpu_inject_without_tcb(env_t env)
+{
+  vka_object_t vcpu;
+  int error = vka_alloc_vcpu(&env->vka, &vcpu);
+
+  error = seL4_ARM_VCPU_InjectIRQ(vcpu.cptr, 0, 0, 0, 0);
+  // TODO: check for error
+}
+DEFINE_TEST(VCPU0001, "Inject IRQ without TCB associated with vCPU", test_vcpu_inject_without_tcb, true)
+#endif