diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 1cacbe6009..cbcc705e79 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -712,8 +712,17 @@ structure Child (cfg : StdioConfig) where
 
 @[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)
 
+/--
+Block until the child process has exited and return its exit code.
+-/
 @[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
+/--
+Check whether the child has exited yet. If it hasn't return none, otherwise its exit code.
+-/
+@[extern "lean_io_process_child_try_wait"] opaque Child.tryWait {cfg : @& StdioConfig} : @& Child cfg →
+    IO (Option UInt32)
+
 /-- Terminates the child process using the SIGTERM signal or a platform analogue.
     If the process was started using `SpawnArgs.setsid`, terminates the entire process group instead. -/
 @[extern "lean_io_process_child_kill"] opaque Child.kill {cfg : @& StdioConfig} : @& Child cfg → IO Unit
diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp
index 035442d186..b073e69592 100644
--- a/src/runtime/process.cpp
+++ b/src/runtime/process.cpp
@@ -92,6 +92,22 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg c
     return lean_io_result_mk_ok(box_uint32(exit_code));
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_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;
+    DWORD ret = WaitForSingleObject(h, 0);
+    if (ret == WAIT_FAILED) {
+        return io_result_mk_error((sstream() << GetLastError()).str());
+    } else if (ret == WAIT_TIMEOUT) {
+        return io_result_mk_ok(mk_option_none());
+    } else {
+        if (!GetExitCodeProcess(h, &exit_code)) {
+            return io_result_mk_error((sstream() << GetLastError()).str());
+        }
+        return lean_io_result_mk_ok(mk_option_some(box_uint32(exit_code)));
+    }
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child, obj_arg) {
     HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
     if (!TerminateProcess(h, 1)) {
@@ -309,6 +325,28 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg c
     }
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_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 *));
+    int status;
+    int ret = waitpid(pid, &status, WNOHANG);
+    if (ret == -1) {
+        return io_result_mk_error(decode_io_error(errno, nullptr));
+    } else if (ret == 0) {
+        return io_result_mk_ok(mk_option_none());
+    } else {
+        if (WIFEXITED(status)) {
+            obj_res output = box_uint32(static_cast<unsigned>(WEXITSTATUS(status)));
+            return lean_io_result_mk_ok(mk_option_some(output));
+        } else {
+            lean_assert(WIFSIGNALED(status));
+            // use bash's convention
+            obj_res output = box_uint32(128 + static_cast<unsigned>(WTERMSIG(status)));
+            return lean_io_result_mk_ok(mk_option_some(output));
+        }
+    }
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(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 *));
diff --git a/tests/lean/Process.lean b/tests/lean/Process.lean
index 863a22350e..b2107c2c47 100644
--- a/tests/lean/Process.lean
+++ b/tests/lean/Process.lean
@@ -57,3 +57,12 @@ def usingIO {α} (x : IO α) : IO α := x
   let (stdin, lean) ← lean.takeStdin
   stdin.putStr "#exit\n"
   lean.wait
+
+#eval usingIO do
+  let child ← spawn { cmd := "sh", args := #["-c", "cat"], stdin := .piped, stdout := .piped }
+  IO.println (← child.tryWait)
+  -- We take stdin in here such that it is closed automatically by dropping the object right away.
+  -- This will kill the `cat` process.
+  let (stdin, child) ← child.takeStdin
+  IO.sleep 1000
+  child.tryWait
diff --git a/tests/lean/Process.lean.expected.out b/tests/lean/Process.lean.expected.out
index fbeb40bc4b..600e4f2544 100644
--- a/tests/lean/Process.lean.expected.out
+++ b/tests/lean/Process.lean.expected.out
@@ -11,3 +11,5 @@ flush of broken pipe failed
 0
 0
 0
+none
+some 0