diff --git a/doc/dev/ffi.md b/doc/dev/ffi.md
index 98d8e69005..632965f216 100644
--- a/doc/dev/ffi.md
+++ b/doc/dev/ffi.md
@@ -111,6 +111,15 @@ if (lean_io_result_is_ok(res)) {
 lean_io_mark_end_initialization();
 ```
 
+In addition, any other thread not spawned by the Lean runtime itself must be initialized for Lean use by calling
+```c
+void lean_initialize_thread();
+```
+and should be finalized in order to free all thread-local resources by calling
+```c
+void lean_finalize_thread();
+```
+
 ## `@[extern]` in the Interpreter
 
 The interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes `@[extern]` declarations.
diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp
index e742fe1e41..6aab3fbc6d 100644
--- a/src/runtime/thread.cpp
+++ b/src/runtime/thread.cpp
@@ -46,18 +46,26 @@ void reset_thread_local() {
 
 using runnable = std::function<void()>;
 
-static void thread_main(void * p) {
+extern "C" LEAN_EXPORT void lean_initialize_thread() {
 #ifdef LEAN_SMALL_ALLOCATOR
     init_thread_heap();
 #endif
+}
+
+extern "C" LEAN_EXPORT void lean_finalize_thread() {
+    run_thread_finalizers();
+    run_post_thread_finalizers();
+}
+
+static void thread_main(void * p) {
+    lean_initialize_thread();
     std::unique_ptr<runnable> f;
     f.reset(reinterpret_cast<runnable *>(p));
 
     (*f)();
     f.reset();
 
-    run_thread_finalizers();
-    run_post_thread_finalizers();
+    lean_finalize_thread();
 }
 
 #if defined(LEAN_MULTI_THREAD)
diff --git a/src/runtime/thread.h b/src/runtime/thread.h
index decebaeae0..0d45928202 100644
--- a/src/runtime/thread.h
+++ b/src/runtime/thread.h
@@ -217,9 +217,14 @@ static T & GETTER_NAME() {                                              \
 }
 
 namespace lean {
+// module initializer pair (NOT for initializing individual threads!)
 void initialize_thread();
 void finalize_thread();
 
+// thread initializer pair, for reverse FFI
+extern "C" LEAN_EXPORT void lean_initialize_thread();
+extern "C" LEAN_EXPORT void lean_finalize_thread();
+
 typedef void (*thread_finalizer)(void *); // NOLINT
 LEAN_EXPORT void register_post_thread_finalizer(thread_finalizer fn, void * p);
 LEAN_EXPORT void register_thread_finalizer(thread_finalizer fn, void * p);