diff --git a/src/syscall/syscall.c b/src/syscall/syscall.c
index 0902245c..541f7d7a 100644
--- a/src/syscall/syscall.c
+++ b/src/syscall/syscall.c
@@ -68,6 +68,7 @@
 #include "syscall/sys.h"
 #include "syscall/usbdev.h"
 #include "syscall/sysvipc.h"
+#include "syscall/syscall_names.h"
 #include "proved/timespec.h"
 
 #include "syscall/time.h"
@@ -2802,9 +2803,22 @@ int syscall_dispatch(hv_vcpu_t vcpu, guest_t *g, int *exit_code, bool verbose)
     if (verbose) {
         uint64_t elr = 0;
         hv_vcpu_get_sys_reg(vcpu, HV_SYS_REG_ELR_EL1, &elr);
+        const char *name = NULL;
+        if (x8 <= SC_MAX_SYSCALL_NUM) {
+            name = syscall_names[x8];
+        }
+
+        char nr_str[64];
+        if (name) {
+            snprintf(nr_str, sizeof(nr_str), "%s(%llu)", name,
+                     (unsigned long long) x8);
+        } else {
+            snprintf(nr_str, sizeof(nr_str), "%llu", (unsigned long long) x8);
+        }
         log_debug(
-            "syscall %llu@0x%llx(0x%llx, 0x%llx, 0x%llx, 0x%llx, "
+            "syscall %s@0x%llx(0x%llx, 0x%llx, 0x%llx, 0x%llx, "
             "0x%llx, 0x%llx)",
+            nr_str,
             (unsigned long long) x8,
             (unsigned long long) (elr >= 4 ? elr - 4 : elr),
             (unsigned long long) x0, (unsigned long long) x1,
diff --git a/src/syscall/syscall_names.h b/src/syscall/syscall_names.h
new file mode 100644
index 00000000..61413d73
--- /dev/null
+++ b/src/syscall/syscall_names.h
@@ -0,0 +1,15 @@
+#pragma once
+
+#include "dispatch.h"
+
+/* Name table generated from dispatch.tbl: shared with syscall.c so verbose
+ * logs can print syscall names. A new entry in dispatch.tbl automatically
+ * gains a name here; slots without a corresponding entry stay NULL and the
+ * caller falls back to printing the raw number.
+ */
+static const char *const syscall_names[SC_MAX_SYSCALL_NUM + 1] = {
+#define _(sys_name, sc_handler, extra) [sys_name] = #sys_name,
+    SYSCALL_TABLE_ENTRIES(_)
+#undef _
+};
+