diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index b2b8b44b4e..eb3dd9a47d 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -462,6 +462,16 @@ Note that it is the caller's job to remove the file after use.
 -/
 @[extern "lean_io_create_tempfile"] opaque createTempFile : IO (Handle × FilePath)
 
+/--
+Creates a temporary directory in the most secure manner possible. There are no race conditions in the
+directory’s creation. The directory is readable and writable only by the creating user ID.
+
+Returns the new directory's path.
+
+It is the caller's job to remove the directory after use.
+-/
+@[extern "lean_io_create_tempdir"] opaque createTempDir : IO FilePath
+
 end FS
 
 @[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String)
@@ -474,17 +484,6 @@ namespace FS
 def withFile (fn : FilePath) (mode : Mode) (f : Handle → IO α) : IO α :=
   Handle.mk fn mode >>= f
 
-/--
-Like `createTempFile` but also takes care of removing the file after usage.
--/
-def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → FilePath → m α) :
-    m α := do
-  let (handle, path) ← createTempFile
-  try
-    f handle path
-  finally
-    removeFile path
-
 def Handle.putStrLn (h : Handle) (s : String) : IO Unit :=
   h.putStr (s.push '\n')
 
@@ -675,8 +674,10 @@ def appDir : IO FilePath := do
     | throw <| IO.userError s!"System.IO.appDir: unexpected filename '{p}'"
   FS.realPath p
 
+namespace FS
+
 /-- Create given path and all missing parents as directories. -/
-partial def FS.createDirAll (p : FilePath) : IO Unit := do
+partial def createDirAll (p : FilePath) : IO Unit := do
   if ← p.isDir then
     return ()
   if let some parent := p.parent then
@@ -693,7 +694,7 @@ partial def FS.createDirAll (p : FilePath) : IO Unit := do
 /--
   Fully remove given directory by deleting all contained files and directories in an unspecified order.
   Fails if any contained entry cannot be deleted or was newly created during execution. -/
-partial def FS.removeDirAll (p : FilePath) : IO Unit := do
+partial def removeDirAll (p : FilePath) : IO Unit := do
   for ent in (← p.readDir) do
     if (← ent.path.isDir : Bool) then
       removeDirAll ent.path
@@ -701,6 +702,32 @@ partial def FS.removeDirAll (p : FilePath) : IO Unit := do
       removeFile ent.path
   removeDir p
 
+/--
+Like `createTempFile`, but also takes care of removing the file after usage.
+-/
+def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → FilePath → m α) :
+    m α := do
+  let (handle, path) ← createTempFile
+  try
+    f handle path
+  finally
+    removeFile path
+
+/--
+Like `createTempDir`, but also takes care of removing the directory after usage.
+
+All files in the directory are recursively deleted, regardless of how or when they were created.
+-/
+def withTempDir [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : FilePath → m α) :
+    m α := do
+  let path ← createTempDir
+  try
+    f path
+  finally
+    removeDirAll path
+
+end FS
+
 namespace Process
 
 /-- Returns the current working directory of the calling process. -/
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 44f18cc587..8768c740b8 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -1140,6 +1140,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_tempfile(lean_object * /* w */) {
     strcat(path, file_pattern);
 
     uv_fs_t req;
+    // Differences from lean_io_create_tempdir start here
     ret = uv_fs_mkstemp(NULL, &req, path, NULL);
     if (ret < 0) {
         // If mkstemp throws an error we cannot rely on path to contain a proper file name.
@@ -1151,6 +1152,48 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_tempfile(lean_object * /* w */) {
     }
 }
 
+/* createTempDir : IO FilePath */
+extern "C" LEAN_EXPORT obj_res lean_io_create_tempdir(lean_object * /* w */) {
+    char path[PATH_MAX];
+    size_t base_len = PATH_MAX;
+    int ret = uv_os_tmpdir(path, &base_len);
+    if (ret < 0) {
+        return io_result_mk_error(decode_uv_error(ret, nullptr));
+    } else if (base_len == 0) {
+        return lean_io_result_mk_error(decode_uv_error(UV_ENOENT, mk_string("")));
+    }
+
+#if defined(LEAN_WINDOWS)
+    // On Windows `GetTempPathW` always returns a path ending in \, but libuv removes it.
+    // https://learn.microsoft.com/en-us/windows/win32/fileio/creating-and-using-a-temporary-file
+    if (path[base_len - 1] != '\\') {
+        lean_always_assert(PATH_MAX >= base_len + 1 + 1);
+        strcat(path, "\\");
+    }
+#else
+    // No guarantee that we have a trailing / in TMPDIR.
+    if (path[base_len - 1] != '/') {
+        lean_always_assert(PATH_MAX >= base_len + 1 + 1);
+        strcat(path, "/");
+    }
+#endif
+
+    const char* file_pattern = "tmp.XXXXXXXX";
+    const size_t file_pattern_size = strlen(file_pattern);
+    lean_always_assert(PATH_MAX >= strlen(path) + file_pattern_size + 1);
+    strcat(path, file_pattern);
+
+    uv_fs_t req;
+    // Differences from lean_io_create_tempfile start here
+    ret = uv_fs_mkdtemp(NULL, &req, path, NULL);
+    if (ret < 0) {
+        // If mkdtemp throws an error we cannot rely on path to contain a proper file name.
+        return io_result_mk_error(decode_uv_error(ret, nullptr));
+    } else {
+        return lean_io_result_mk_ok(mk_string(req.path));
+    }
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg fname, obj_arg) {
     if (std::remove(string_cstr(fname)) == 0) {
         return io_result_mk_ok(box(0));
diff --git a/tests/lean/run/tempfile.lean b/tests/lean/run/tempfile.lean
index cd7ba0f495..6387c0a826 100644
--- a/tests/lean/run/tempfile.lean
+++ b/tests/lean/run/tempfile.lean
@@ -1,10 +1,100 @@
+/-!
+# Temporary Files
+
+These tests check that temporary files and directories can be created and used.
+-/
+
+/--
+Tests temporary file creation.
+-/
 def test : IO Unit := do
   let (handle, path) ← IO.FS.createTempFile
-  let toWrite := "Hello World"
-  handle.putStr toWrite
-  let handle2 ← IO.FS.Handle.mk path .read
-  let content ← handle2.getLine
-  assert! (content == toWrite)
-  IO.FS.removeFile path
+  try
+    let toWrite := "Hello World"
+    handle.putStr toWrite
+    handle.flush
+    let handle2 ← IO.FS.Handle.mk path .read
+    let content ← handle2.getLine
+    assert! (content == toWrite)
+  finally
+    IO.FS.removeFile path
 
 #eval test
+
+/--
+Tests temporary file helper.
+-/
+def testWithFile : IO Unit := do
+  let pathRef ← IO.mkRef none
+  IO.FS.withTempFile fun handle path => do
+    pathRef.set (some path)
+    assert! (← path.pathExists)
+    let toWrite := "Hello World"
+    handle.putStr toWrite
+    handle.flush
+    let handle2 ← IO.FS.Handle.mk path .read
+    let content ← handle2.getLine
+    assert! (content == toWrite)
+  match (← pathRef.get) with
+  | none => assert! false
+  | some p => assert! (! (← p.pathExists))
+
+#eval testWithFile
+
+/--
+Tests temporary directory creation and ensures that files can be created in it.
+-/
+def testDir : IO Unit := do
+  let path ← IO.FS.createTempDir
+  try
+    assert! (← path.isDir)
+
+    let fileList ← path.readDir
+    assert! (fileList.isEmpty)
+
+    let toWrite := "Hello World"
+    for i in [0:3] do
+      IO.FS.withFile (path / s!"{i}.txt") .write fun h => do
+        h.putStr toWrite
+        h.putStr (toString i)
+    for i in [0:3] do
+      IO.FS.withFile (path / s!"{i}.txt") .read fun h => do
+        let content ← h.getLine
+        assert! (content == toWrite ++ toString i)
+
+    let fileList := ((← path.readDir).map (·.fileName)).qsortOrd
+    assert! (fileList == #["0.txt",  "1.txt", "2.txt"])
+  finally
+    IO.FS.removeDirAll path
+
+#eval testDir
+
+/--
+Tests temporary directory helper.
+-/
+def testWithDir : IO Unit := do
+  let pathRef ← IO.mkRef none
+  IO.FS.withTempDir fun path => do
+    pathRef.set (some path)
+    assert! (← path.isDir)
+
+    let fileList ← path.readDir
+    assert! (fileList.isEmpty)
+
+    let toWrite := "Hello World"
+    for i in [0:3] do
+      IO.FS.withFile (path / s!"{i}.txt") .write fun h => do
+        h.putStr toWrite
+        h.putStr (toString i)
+    for i in [0:3] do
+      IO.FS.withFile (path / s!"{i}.txt") .read fun h => do
+        let content ← h.getLine
+        assert! (content == toWrite ++ toString i)
+
+    let fileList := ((← path.readDir).map (·.fileName)).qsortOrd
+    assert! (fileList == #["0.txt",  "1.txt", "2.txt"])
+  match (← pathRef.get) with
+  | none => assert! false
+  | some p => assert! (! (← p.pathExists))
+
+#eval testWithDir