diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs
index fd0bc2ef7..66fb886ab 100644
--- a/ostd/src/mm/kspace/mod.rs
+++ b/ostd/src/mm/kspace/mod.rs
@@ -148,8 +148,17 @@ pub exec static KERNEL_PAGE_TABLE: OnceImpl<PageTable<KernelPtConfig>, TrivialPr
     OnceImpl::new(Ghost(TrivialPred));
 
 
-#[derive(Clone, Debug)]
-pub(crate) struct KernelPtConfig {}
+#[derive(Debug)]
+pub struct KernelPtConfig {}
+
+#[verus_verify]
+impl Clone for KernelPtConfig {
+    #[inline(always)]
+    #[verus_spec(returns self)]
+    fn clone(&self) -> Self {
+        KernelPtConfig {}
+    }
+}
 
 // We use the first available PTE bit to mark the frame as tracked.
 // SAFETY: `item_into_raw` and `item_from_raw` are implemented correctly,
diff --git a/ostd/src/mm/tlb.rs b/ostd/src/mm/tlb.rs
index cb8ea85ea..0dfaf4e6d 100644
--- a/ostd/src/mm/tlb.rs
+++ b/ostd/src/mm/tlb.rs
@@ -188,7 +188,7 @@ impl<'a  /*, G: PinCurrentCpu*/ > TlbFlusher<'a  /*, G*/ > {
 }
 
 /// The operation to flush TLB entries.
-#[derive(Debug, Clone, PartialEq, Eq)]
+#[derive(Debug, PartialEq, Eq)]
 pub enum TlbFlushOp {
     /// Flush all TLB entries except for the global entries.
     All,
@@ -198,6 +198,17 @@ pub enum TlbFlushOp {
     Range(Range<Vaddr>),
 }
 
+impl Clone for TlbFlushOp {
+    #[verus_spec(returns self)]
+    fn clone(&self) -> Self {
+        match self {
+            TlbFlushOp::All => TlbFlushOp::All,
+            TlbFlushOp::Address(addr) => TlbFlushOp::Address(*addr),
+            TlbFlushOp::Range(range) => TlbFlushOp::Range(range.clone()),
+        }
+    }
+}
+
 impl TlbFlushOp {
     /// Performs the TLB flush operation on the current CPU.
     #[verifier::external_body]
diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs
index 0c70dc4ad..54e67d11b 100644
--- a/ostd/src/mm/vm_space.rs
+++ b/ostd/src/mm/vm_space.rs
@@ -1185,9 +1185,18 @@ pub(super) fn get_activated_vm_space() -> *const VmSpace {
 }*/
 
 /// The configuration for user page tables.
-#[derive(Clone, Debug)]
+#[derive(Debug)]
 pub struct UserPtConfig {}
 
+#[verus_verify]
+impl Clone for UserPtConfig {
+    #[inline(always)]
+    #[verus_spec(returns self)]
+    fn clone(&self) -> Self {
+        Self {}
+    }
+}
+
 /// The item that can be mapped into the [`VmSpace`].
 pub struct MappedItem {
     pub frame: UFrame,
diff --git a/ostd/src/util/either.rs b/ostd/src/util/either.rs
index 3cb20a48c..a0820fe58 100644
--- a/ostd/src/util/either.rs
+++ b/ostd/src/util/either.rs
@@ -6,7 +6,7 @@
 use vstd::prelude::*;
 
 #[verus_verify]
-#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+#[derive(Copy, PartialEq, Eq, Debug)]
 pub enum Either<L, R> {
     /// Contains the left value
     Left(L),
@@ -14,6 +14,27 @@ pub enum Either<L, R> {
     Right(R),
 }
 
+#[verus_verify]
+impl<L, R> Clone for Either<L, R>
+where
+    L: Clone,
+    R: Clone,
+{
+    #[inline(always)]
+    #[verus_spec(r =>
+      ensures
+          (forall|l1, l2: L| call_ensures(L::clone, (l1,), l2) ==> l1 == l2) &&
+          (forall|r1, r2: R| call_ensures(R::clone, (r1,), r2) ==> r1 == r2)
+            ==> r == self,
+    )]
+    fn clone(&self) -> Self {
+        match self {
+            Self::Left(left) => Self::Left(left.clone()),
+            Self::Right(right) => Self::Right(right.clone()),
+        }
+    }
+}
+
 impl<L, R> Either<L, R> {
     #[verus_verify(dual_spec)]
     /// Converts to the left value, if any.