diff --git a/src/Std/Internal/Async/Timer.lean b/src/Std/Internal/Async/Timer.lean
index e3fd6a77d66c..72cf604fb775 100644
--- a/src/Std/Internal/Async/Timer.lean
+++ b/src/Std/Internal/Async/Timer.lean
@@ -90,7 +90,7 @@ Setup up an `Interval` that waits for `duration` milliseconds.
 This function only initializes but does not yet start the timer.
 -/
 @[inline]
-def mk (duration : Std.Time.Millisecond.Offset) : IO Interval := do
+def mk (duration : Std.Time.Millisecond.Offset) (_ : 0 < duration := by decide) : IO Interval := do
   let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 true
   return ofNative native
 
diff --git a/tests/lean/run/async_surface_sleep.lean b/tests/lean/run/async_surface_sleep.lean
index b548fd058f2c..23f6cf30b27e 100644
--- a/tests/lean/run/async_surface_sleep.lean
+++ b/tests/lean/run/async_surface_sleep.lean
@@ -63,7 +63,7 @@ def oneSleep : IO Unit := do
   assert! (← task.block) == 37
 where
   go : IO (AsyncTask Nat) := do
-    let interval ← Interval.mk BASE_DURATION
+    let interval ← Interval.mk BASE_DURATION sorry
     (← interval.tick).mapIO fun _ => do
       interval.stop
       return 37
@@ -73,7 +73,7 @@ def doubleSleep : IO Unit := do
   assert! (← task.block) == 37
 where
   go : IO (AsyncTask Nat) := do
-    let interval ← Interval.mk BASE_DURATION
+    let interval ← Interval.mk BASE_DURATION sorry
     (← interval.tick).bindIO fun _ => do
     (← interval.tick).mapIO fun _ => do
       interval.stop
@@ -84,7 +84,7 @@ def resetSleep : IO Unit := do
   assert! (← task.block) == 37
 where
   go : IO (AsyncTask Nat) := do
-    let interval ← Interval.mk BASE_DURATION
+    let interval ← Interval.mk BASE_DURATION sorry
     (← interval.tick).bindIO fun _ => do
       let waiter ← interval.tick
       interval.reset