diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 15b0d8c58391..b2b8b44b4e4d 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -802,6 +802,9 @@ def run (args : SpawnArgs) : IO String := do
 
 end Process
 
+/-- Returns the thread ID of the calling thread. -/
+@[extern "lean_io_get_tid"] opaque getTID : BaseIO UInt64
+
 structure AccessRight where
   read : Bool := false
   write : Bool := false
diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp
index 9d74634edcb5..13c3c30d40f8 100644
--- a/src/runtime/process.cpp
+++ b/src/runtime/process.cpp
@@ -27,6 +27,10 @@ Author: Jared Roesch
 #include <limits.h> // NOLINT
 #endif
 
+#ifdef __linux
+#include <sys/syscall.h>
+#endif
+
 #include "runtime/object.h"
 #include "runtime/io.h"
 #include "runtime/array_ref.h"
@@ -80,6 +84,10 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
     return lean_io_result_mk_ok(box_uint32(GetCurrentProcessId()));
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
+    return lean_io_result_mk_ok(box_uint64(GetCurrentThreadId()));
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
     HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
     DWORD exit_code;
@@ -316,6 +324,20 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
     return lean_io_result_mk_ok(box_uint32(getpid()));
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
+    uint64_t tid;
+#ifdef __APPLE__
+    lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
+#elif defined(LEAN_EMSCRIPTEN)
+    tid = 0;
+#else
+    // since Linux 2.4.11, our glibc 2.27 requires at least 3.2
+    // glibc 2.30 would provide a wrapper
+    tid = (pid_t)syscall(SYS_gettid);
+#endif
+    return lean_io_result_mk_ok(box_uint64(tid));
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
     static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
     pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));