diff --git a/tests/slow/tokio-proofs/expected b/tests/slow/tokio-proofs/expected
index 4ed6220f349b..c35c41928fd3 100644
--- a/tests/slow/tokio-proofs/expected
+++ b/tests/slow/tokio-proofs/expected
@@ -1 +1 @@
-Complete - 13 successfully verified harnesses, 0 failures, 13 total.
+Complete - 27 successfully verified harnesses, 0 failures, 27 total.
diff --git a/tests/slow/tokio-proofs/src/tokio/io_chain.rs b/tests/slow/tokio-proofs/src/tokio/io_chain.rs
index 6987c0dd79ce..a3fa94ebf528 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_chain.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_chain.rs
@@ -12,9 +12,8 @@
 use tokio::io::AsyncReadExt;
 use tokio_test::assert_ok;
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn chain() {
     let mut buf = Vec::new();
     let rd1: &[u8] = b"hello ";
diff --git a/tests/slow/tokio-proofs/src/tokio/io_copy.rs b/tests/slow/tokio-proofs/src/tokio/io_copy.rs
index b93e27521c05..e87024092919 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_copy.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_copy.rs
@@ -17,7 +17,7 @@ use tokio_test::assert_ok;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn copy() {
@@ -47,7 +47,7 @@ async fn copy() {
     assert_eq!(wr, b"hello world");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn proxy() {
diff --git a/tests/slow/tokio-proofs/src/tokio/io_lines.rs b/tests/slow/tokio-proofs/src/tokio/io_lines.rs
index aafeae912e15..d9720639f638 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_lines.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_lines.rs
@@ -12,7 +12,7 @@
 use tokio::io::AsyncBufReadExt;
 use tokio_test::assert_ok;
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires memchr
 #[kani::proof]
 #[kani::unwind(2)]
 async fn lines_inherent() {
diff --git a/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs b/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs
index d013af942b9b..0cc90ba2ac73 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs
@@ -11,7 +11,7 @@
 
 use tokio::io::{AsyncReadExt, AsyncWriteExt, duplex};
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn ping_pong() {
@@ -29,7 +29,7 @@ async fn ping_pong() {
 }
 
 // Kani does not support this one yet because it uses spawn
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn across_tasks() {
@@ -54,7 +54,7 @@ async fn across_tasks() {
 }
 
 // Kani does not support this one yet because it uses spawn
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn disconnect() {
@@ -79,7 +79,7 @@ async fn disconnect() {
 }
 
 // Kani does not support this one yet because it uses spawn
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn disconnect_reader() {
@@ -101,7 +101,7 @@ async fn disconnect_reader() {
 }
 
 // Kani does not support this one yet because it uses spawn
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn max_write_size() {
@@ -124,7 +124,7 @@ async fn max_write_size() {
 }
 
 // Kani does not support this one yet because it uses select
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn duplex_is_cooperative() {
diff --git a/tests/slow/tokio-proofs/src/tokio/io_read.rs b/tests/slow/tokio-proofs/src/tokio/io_read.rs
index b346fa8b20e3..f11029599aa4 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_read.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_read.rs
@@ -71,11 +71,9 @@ impl AsyncRead for BadAsyncRead {
     }
 }
 
-#[cfg(disabled)] // because Kani does not support should_panic
 #[kani::proof]
 #[kani::unwind(2)]
-#[tokio::test]
-#[should_panic]
+#[kani::should_panic]
 async fn read_buf_bad_async_read() {
     let mut buf = Vec::with_capacity(10);
     BadAsyncRead::new().read_buf(&mut buf).await.unwrap();
diff --git a/tests/slow/tokio-proofs/src/tokio/io_read_buf.rs b/tests/slow/tokio-proofs/src/tokio/io_read_buf.rs
index c59864bae5af..9e0a8c8b5083 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_read_buf.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_read_buf.rs
@@ -16,7 +16,6 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(12)]
 async fn read_buf() {
diff --git a/tests/slow/tokio-proofs/src/tokio/io_read_line.rs b/tests/slow/tokio-proofs/src/tokio/io_read_line.rs
index 23dfc0671def..f62faa74405c 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_read_line.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_read_line.rs
@@ -15,7 +15,7 @@ use tokio_test::{assert_ok, io::Builder};
 
 use std::io::Cursor;
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line() {
@@ -39,7 +39,7 @@ async fn read_line() {
     assert_eq!(buf, "");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line_not_all_ready() {
@@ -68,7 +68,7 @@ async fn read_line_not_all_ready() {
     assert_eq!(line.as_str(), "2");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line_invalid_utf8() {
@@ -83,7 +83,7 @@ async fn read_line_invalid_utf8() {
     assert_eq!(line.as_str(), "Foo");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line_fail() {
@@ -101,7 +101,7 @@ async fn read_line_fail() {
     assert_eq!(line.as_str(), "FooHello Wor");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line_fail_and_utf8_fail() {
diff --git a/tests/slow/tokio-proofs/src/tokio/io_read_to_end.rs b/tests/slow/tokio-proofs/src/tokio/io_read_to_end.rs
index 215343d59c3d..ddd9eb816ebe 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_read_to_end.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_read_to_end.rs
@@ -14,9 +14,8 @@ use std::task::{Context, Poll};
 use tokio::io::{AsyncRead, AsyncReadExt, ReadBuf};
 use tokio_test::assert_ok;
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn read_to_end() {
     let mut buf = vec![];
     let mut rd: &[u8] = b"hello world";
@@ -75,9 +74,8 @@ impl AsyncRead for UninitTest {
     }
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(65)]
 async fn read_to_end_uninit() {
     let mut buf = Vec::with_capacity(64);
     let mut test = UninitTest { num_init: 0, state: State::Initializing };
diff --git a/tests/slow/tokio-proofs/src/tokio/io_read_to_string.rs b/tests/slow/tokio-proofs/src/tokio/io_read_to_string.rs
index 85f8a0e88d16..9b6823304897 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_read_to_string.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_read_to_string.rs
@@ -14,9 +14,9 @@ use tokio::io::AsyncReadExt;
 use tokio_test::assert_ok;
 use tokio_test::io::Builder;
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC takes more than 15 minutes
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn read_to_string() {
     let mut buf = String::new();
     let mut rd: &[u8] = b"hello world";
@@ -26,7 +26,7 @@ async fn read_to_string() {
     assert_eq!(buf[..], "hello world"[..]);
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn to_string_does_not_truncate_on_utf8_error() {
@@ -43,7 +43,7 @@ async fn to_string_does_not_truncate_on_utf8_error() {
     assert_eq!(s, "abc");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn to_string_does_not_truncate_on_io_error() {
@@ -62,7 +62,7 @@ async fn to_string_does_not_truncate_on_io_error() {
     assert_eq!(s, "abc");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn to_string_appends() {
diff --git a/tests/slow/tokio-proofs/src/tokio/io_read_until.rs b/tests/slow/tokio-proofs/src/tokio/io_read_until.rs
index c91cb188575d..5bc33722aa96 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_read_until.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_read_until.rs
@@ -13,7 +13,7 @@ use std::io::ErrorKind;
 use tokio::io::{AsyncBufReadExt, BufReader, Error};
 use tokio_test::{assert_ok, io::Builder};
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires memchr
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_until() {
@@ -33,7 +33,7 @@ async fn read_until() {
     assert_eq!(buf, []);
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_until_not_all_ready() {
@@ -62,7 +62,7 @@ async fn read_until_not_all_ready() {
     assert_eq!(chunk, b"2");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_until_fail() {
diff --git a/tests/slow/tokio-proofs/src/tokio/io_take.rs b/tests/slow/tokio-proofs/src/tokio/io_take.rs
index 6cf484eb08b2..7cc9e13fd89e 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_take.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_take.rs
@@ -68,11 +68,9 @@ impl AsyncRead for BadReader {
     }
 }
 
-#[cfg(disabled)] //  because Kani does not support should_panic
 #[kani::proof]
 #[kani::unwind(2)]
-#[tokio::test]
-#[should_panic]
+#[kani::should_panic]
 async fn bad_reader_fails() {
     let mut buf = Vec::with_capacity(10);
 
diff --git a/tests/slow/tokio-proofs/src/tokio/io_util_empty.rs b/tests/slow/tokio-proofs/src/tokio/io_util_empty.rs
index f40813c6a4e5..ff3dae8261fb 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_util_empty.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_util_empty.rs
@@ -11,10 +11,9 @@
 #![cfg(feature = "full")]
 use tokio::io::{AsyncBufReadExt, AsyncReadExt};
 
-#[cfg(disabled)] // because Kani does not support select yet
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
-#[tokio::test]
 async fn empty_read_is_cooperative() {
     tokio::select! {
         biased;
@@ -29,10 +28,9 @@ async fn empty_read_is_cooperative() {
     }
 }
 
-#[cfg(disabled)] // because Kani does not support select yet
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
-#[tokio::test]
 async fn empty_buf_reads_are_cooperative() {
     tokio::select! {
         biased;
diff --git a/tests/slow/tokio-proofs/src/tokio/io_write.rs b/tests/slow/tokio-proofs/src/tokio/io_write.rs
index 5b6db57d1c75..abed83e8bc51 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_write.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_write.rs
@@ -17,9 +17,8 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn write2() {
     struct Wr {
         buf: BytesMut,
diff --git a/tests/slow/tokio-proofs/src/tokio/io_write_all.rs b/tests/slow/tokio-proofs/src/tokio/io_write_all.rs
index 751272a23db8..c14daf4ab7b7 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_write_all.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_write_all.rs
@@ -18,9 +18,8 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn write_all() {
     struct Wr {
         buf: BytesMut,
diff --git a/tests/slow/tokio-proofs/src/tokio/io_write_all_buf.rs b/tests/slow/tokio-proofs/src/tokio/io_write_all_buf.rs
index 61ff4ffc8850..ead86a93f451 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_write_all_buf.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_write_all_buf.rs
@@ -18,7 +18,7 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires write
 #[kani::proof]
 #[kani::unwind(2)]
 async fn write_all_buf() {
@@ -62,9 +62,8 @@ async fn write_all_buf() {
     assert!(!buf.has_remaining());
 }
 
-#[cfg(disabled)] // because of missing functions
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn write_buf_err() {
     /// Error out after writing the first 4 bytes
     struct Wr {
diff --git a/tests/slow/tokio-proofs/src/tokio/io_write_buf.rs b/tests/slow/tokio-proofs/src/tokio/io_write_buf.rs
index e83db9200e00..e19b65270af8 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_write_buf.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_write_buf.rs
@@ -18,9 +18,8 @@ use std::io::{self, Cursor};
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn write_all1() {
     struct Wr {
         buf: BytesMut,
diff --git a/tests/slow/tokio-proofs/src/tokio/io_write_int.rs b/tests/slow/tokio-proofs/src/tokio/io_write_int.rs
index f4a5cd38d7ac..e058e42f572f 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_write_int.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_write_int.rs
@@ -15,7 +15,6 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn write_int_should_err_if_write_count_0() {
diff --git a/tests/slow/tokio-proofs/src/tokio/sync_mpsc.rs b/tests/slow/tokio-proofs/src/tokio/sync_mpsc.rs
index f132b8a3ba37..ebe61ebc6688 100644
--- a/tests/slow/tokio-proofs/src/tokio/sync_mpsc.rs
+++ b/tests/slow/tokio-proofs/src/tokio/sync_mpsc.rs
@@ -33,7 +33,6 @@ trait AssertSend: Send {}
 impl AssertSend for mpsc::Sender<i32> {}
 impl AssertSend for mpsc::Receiver<i32> {}
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn send_recv_with_buffer() {
@@ -170,7 +169,6 @@ fn buffer_gteq_one() {
     mpsc::channel::<i32>(0);
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn send_recv_unbounded() {
@@ -222,7 +220,6 @@ async fn send_recv_stream_unbounded() {
     assert_eq!(None, rx.next().await);
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn no_t_bounds_buffer() {
@@ -240,7 +237,6 @@ async fn no_t_bounds_buffer() {
     assert!(rx.recv().await.is_some());
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn no_t_bounds_unbounded() {
@@ -289,7 +285,6 @@ async fn send_recv_buffer_limited() {
     assert!(rx.recv().await.is_some());
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn recv_close_gets_none_idle() {
@@ -331,7 +326,6 @@ async fn recv_close_gets_none_reserved() {
     assert!(rx.recv().await.is_none());
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn tx_close_gets_none() {
@@ -339,7 +333,6 @@ async fn tx_close_gets_none() {
     assert!(rx.recv().await.is_none());
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn try_send_fail() {
@@ -362,7 +355,6 @@ async fn try_send_fail() {
     assert!(rx.recv().await.is_none());
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn try_send_fail_with_try_recv() {
@@ -385,7 +377,6 @@ async fn try_send_fail_with_try_recv() {
     assert_eq!(rx.try_recv(), Err(TryRecvError::Disconnected));
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn try_reserve_fails() {
@@ -429,7 +420,6 @@ async fn drop_permit_releases_permit() {
     assert_ready_ok!(reserve2.poll());
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn dropping_rx_closes_channel() {
@@ -443,7 +433,6 @@ async fn dropping_rx_closes_channel() {
     assert_eq!(1, Arc::strong_count(&msg));
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 fn dropping_rx_closes_channel_for_try() {
@@ -461,7 +450,6 @@ fn dropping_rx_closes_channel_for_try() {
     assert_eq!(1, Arc::strong_count(&msg));
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 fn unconsumed_messages_are_dropped() {
@@ -564,7 +552,6 @@ async fn permit_available_not_acquired_close() {
     assert!(rx.recv().await.is_none());
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 fn try_recv_bounded() {
@@ -628,7 +615,6 @@ fn try_recv_unbounded() {
     }
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 fn try_recv_close_while_empty_bounded() {
@@ -639,7 +625,6 @@ fn try_recv_close_while_empty_bounded() {
     assert_eq!(Err(TryRecvError::Disconnected), rx.try_recv());
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 fn try_recv_close_while_empty_unbounded() {
@@ -650,7 +635,6 @@ fn try_recv_close_while_empty_unbounded() {
     assert_eq!(Err(TryRecvError::Disconnected), rx.try_recv());
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 // #[tokio::test(start_paused = true)]
diff --git a/tests/slow/tokio-proofs/src/tokio_stream/stream_chain.rs b/tests/slow/tokio-proofs/src/tokio_stream/stream_chain.rs
index 58a0e85ea8c1..f12ccfed9765 100644
--- a/tests/slow/tokio-proofs/src/tokio_stream/stream_chain.rs
+++ b/tests/slow/tokio-proofs/src/tokio_stream/stream_chain.rs
@@ -10,7 +10,6 @@ use crate::tokio_stream::support::mpsc;
 use tokio_stream::{self as stream, Stream, StreamExt};
 use tokio_test::{assert_pending, assert_ready, task};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn basic_usage_chain() {
diff --git a/tests/slow/tokio-proofs/src/tokio_stream/stream_merge.rs b/tests/slow/tokio-proofs/src/tokio_stream/stream_merge.rs
index 8cf789024004..d277b29b0640 100644
--- a/tests/slow/tokio-proofs/src/tokio_stream/stream_merge.rs
+++ b/tests/slow/tokio-proofs/src/tokio_stream/stream_merge.rs
@@ -11,7 +11,6 @@ use tokio_stream::{self as stream, Stream, StreamExt};
 use tokio_test::task;
 use tokio_test::{assert_pending, assert_ready};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(8)]
 async fn merge_sync_streams() {
diff --git a/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs b/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs
index 72c4d486daf8..c9baae12e63c 100644
--- a/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs
+++ b/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs
@@ -30,7 +30,7 @@ macro_rules! assert_ready_none {
     };
 }
 
-#[cfg(disabled)] // because an assertion about unreachable code failed
+#[cfg(disabled)] // requires syscall
 #[kani::proof]
 #[kani::unwind(2)]
 async fn empty() {
diff --git a/tests/slow/tokio-proofs/src/tokio_test/block_on.rs b/tests/slow/tokio-proofs/src/tokio_test/block_on.rs
index 3bf00ac0a5a7..cae1e41dcf41 100644
--- a/tests/slow/tokio-proofs/src/tokio_test/block_on.rs
+++ b/tests/slow/tokio-proofs/src/tokio_test/block_on.rs
@@ -11,7 +11,7 @@
 use tokio::time::{Duration, Instant, sleep_until};
 use tokio_test::block_on;
 
-#[cfg(disabled)] // because epoll is missing
+#[cfg(disabled)] // CBMC takes more than 15 minutes
 #[kani::proof]
 #[kani::unwind(2)]
 fn async_block() {
@@ -22,7 +22,7 @@ async fn five() -> u8 {
     5
 }
 
-#[cfg(disabled)] // because epoll is missing
+#[cfg(disabled)] // CBMC takes more than 15 minutes
 #[kani::proof]
 #[kani::unwind(2)]
 fn async_fn() {
diff --git a/tests/slow/tokio-proofs/src/tokio_test/io.rs b/tests/slow/tokio-proofs/src/tokio_test/io.rs
index dd92d220349f..b2d825793729 100644
--- a/tests/slow/tokio-proofs/src/tokio_test/io.rs
+++ b/tests/slow/tokio-proofs/src/tokio_test/io.rs
@@ -12,7 +12,7 @@ use std::io;
 use tokio::io::{AsyncReadExt, AsyncWriteExt};
 use tokio_test::io::Builder;
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC takes more than 15 minutes
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read1() {
@@ -27,7 +27,7 @@ async fn read1() {
     assert_eq!(&buf[..n], b"world!");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_error() {
@@ -50,7 +50,7 @@ async fn read_error() {
     assert_eq!(&buf[..n], b"world!");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn write1() {
@@ -60,7 +60,7 @@ async fn write1() {
     mock.write_all(b"world!").await.expect("write 2");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn write_error() {
diff --git a/tests/slow/tokio-proofs/src/tokio_util/io_reader_stream.rs b/tests/slow/tokio-proofs/src/tokio_util/io_reader_stream.rs
index 95e2ca177f47..f3f92d923ea3 100644
--- a/tests/slow/tokio-proofs/src/tokio_util/io_reader_stream.rs
+++ b/tests/slow/tokio-proofs/src/tokio_util/io_reader_stream.rs
@@ -43,7 +43,7 @@ impl AsyncRead for Reader {
     }
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC takes more than 15 minutes
 #[kani::proof]
 #[kani::unwind(2)]
 async fn correct_behavior_on_errors() {
diff --git a/tests/slow/tokio-proofs/src/tokio_util/io_stream_reader.rs b/tests/slow/tokio-proofs/src/tokio_util/io_stream_reader.rs
index ef71a5d29f27..e3dff80d9fee 100644
--- a/tests/slow/tokio-proofs/src/tokio_util/io_stream_reader.rs
+++ b/tests/slow/tokio-proofs/src/tokio_util/io_stream_reader.rs
@@ -13,9 +13,8 @@ use tokio::io::AsyncReadExt;
 use tokio_stream::iter;
 use tokio_util::io::StreamReader;
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(8)]
 async fn test_stream_reader() -> std::io::Result<()> {
     let stream = iter(vec![
         std::io::Result::Ok(Bytes::from_static(&[])),