diff --git a/library/alloc/src/collections/vec_deque/mod.rs b/library/alloc/src/collections/vec_deque/mod.rs
index 5b1147ead0a0c..d217dc7a234a6 100644
--- a/library/alloc/src/collections/vec_deque/mod.rs
+++ b/library/alloc/src/collections/vec_deque/mod.rs
@@ -3088,12 +3088,13 @@ impl<T, const N: usize> From<[T; N]> for VecDeque<T> {
 mod verify {
     use core::kani;
     use crate::collections::VecDeque;
+    use core::kani::implies;
 
     #[kani::proof]
-    // Stubbing is currently not possible for functions returning pointers as 
-    // Arbitrary trait hasn't been implemented for them
-    // #[kani::stub_verified(<*mut u32>::add)]
     fn check_vecdeque_swap() {
+        // The array's length is set to an arbitrary value, which defines its size.
+        // In this case, implementing a dynamic array is not possible using any_array
+        // The more elements in the array the longer the veification time.
         const ARRAY_LEN: usize = 40;
         let mut arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array();
         let mut deque: VecDeque<u32> = VecDeque::from(arr);
diff --git a/library/core/src/option.rs b/library/core/src/option.rs
index cb6d79de083aa..052cff05faf80 100644
--- a/library/core/src/option.rs
+++ b/library/core/src/option.rs
@@ -2580,9 +2580,6 @@ mod verify {
     use crate::option::Option;
 
     #[kani::proof]
-    // Stubbing is currently not possible for functions returning pointers as 
-    // Arbitrary trait hasn't been implemented for them
-    // #[kani::stub_verified(<*const u32>::byte_add)]
     fn verify_as_slice() {
         if kani::any() {
             // Case 1: Option is Some
@@ -2601,4 +2598,4 @@ mod verify {
             assert!(empty_slice.is_empty()); // Explicit check for emptiness
         }
     }
-}
\ No newline at end of file
+}