diff --git a/ostd/src/sync/mod.rs b/ostd/src/sync/mod.rs
index 4908e75f4..3e6552813 100644
--- a/ostd/src/sync/mod.rs
+++ b/ostd/src/sync/mod.rs
@@ -20,7 +20,7 @@ pub use self::{
     rwarc::{RoArc, RwArc},
     rwlock::{RwLock, RwLockReadGuard, RwLockUpgradeableGuard, RwLockWriteGuard},
     rwmutex::{RwMutex, RwMutexReadGuard, RwMutexUpgradeableGuard, RwMutexWriteGuard},
-    spin::{SpinLock, SpinLockGuard},
+    spin::{SpinLock, SpinLockGuard, SpinLockPredicate, TrivialSpinLockPredicate},
     wait::{WaitQueue, Waiter, Waker},
 };
 /*
diff --git a/ostd/src/sync/spin.rs b/ostd/src/sync/spin.rs
index 7083a2275..304d61570 100644
--- a/ostd/src/sync/spin.rs
+++ b/ostd/src/sync/spin.rs
@@ -15,6 +15,117 @@ use core::{
 use super::{guard::SpinGuardian, LocalIrqDisabled /*, PreemptDisabled*/};
 //use crate::task::atomic_mode::AsAtomicModeGuard;
 
+verus! {
+
+/// A user-supplied invariant for data protected by a [`SpinLock`].
+///
+/// `State` is tracked state transferred together with the permission for the
+/// protected value. The invariant is required to hold
+/// while the state is stored in an unlocked spin lock. A lock guard may
+/// temporarily break it, but must restore it before returning the state when
+/// the guard is dropped.
+pub trait SpinLockPredicate<T>: Sized {
+    /// Immutable ghost data fixed when a spin lock is created.
+    type Constant;
+
+    /// Tracked state used to relate the protected value to external ghost
+    /// state.
+    type State;
+
+    /// The relation that must hold between the protected value and its tracked
+    /// state while the spin lock is unlocked.
+    spec fn inv(constant: Self::Constant, value: T, state: Self::State) -> bool;
+}
+
+/// A spin-lock invariant that imposes no condition on the protected value.
+///
+/// This predicate allows existing `SpinLock` users to opt out of a custom
+/// invariant.
+pub struct TrivialSpinLockPredicate;
+
+impl<T> SpinLockPredicate<T> for TrivialSpinLockPredicate {
+    type Constant = ();
+    type State = ();
+
+    open spec fn inv(_constant: (), _value: T, _state: ()) -> bool {
+        true
+    }
+}
+
+/// The tracked resources transferred from the unlocked spin lock to its guard
+/// when the lock is acquired, and returned to the lock when the guard is dropped.
+tracked struct SpinLockResource<T, P: SpinLockPredicate<T>> {
+    tracked perm: PointsTo<T>,
+    tracked state: P::State,
+}
+
+impl<T, P: SpinLockPredicate<T>> SpinLockResource<T, P> {
+    pub closed spec fn cell_id(self) -> cell::CellId {
+        self.perm.id()
+    }
+
+    pub closed spec fn value(self) -> T {
+        *self.perm.value()
+    }
+
+    pub closed spec fn predicate_state(self) -> P::State {
+        self.state
+    }
+}
+
+/// The following structs adapt [`SpinLockPredicate`] to [`AtomicBool`]'s invariant by pairing the
+/// protected [`PCell`]'s id with the user-supplied predicate constant. The atomic predicate
+/// ensures that the stored [`PointsTo`] permission belongs to that cell and satisfies the user
+/// invariant. Atomic operations may update the lock bit and tracked resource, while this paired
+/// constant remains fixed for the lifetime of the [`AtomicBool`].
+ghost struct SpinLockConstant<C> {
+    cell_id: cell::CellId,
+    user_constant: C,
+}
+
+impl<C> SpinLockConstant<C> {
+    pub closed spec fn cell_id(self) -> cell::CellId {
+        self.cell_id
+    }
+
+    pub closed spec fn user_constant(self) -> C {
+        self.user_constant
+    }
+}
+
+struct SpinLockAtomicPredicate<T, P: SpinLockPredicate<T>> {
+    phantom: PhantomData<(T, P)>,
+}
+
+impl<T, P: SpinLockPredicate<T>>
+    AtomicInvariantPredicate<
+        SpinLockConstant<P::Constant>,
+        bool,
+        Option<SpinLockResource<T, P>>,
+    > for SpinLockAtomicPredicate<T, P>
+{
+    open spec fn atomic_inv(
+        constant: SpinLockConstant<P::Constant>,
+        locked: bool,
+        resource: Option<SpinLockResource<T, P>>,
+    ) -> bool {
+        match resource {
+            None => locked,
+            Some(resource) => {
+                &&& !locked
+                &&& resource.cell_id() == constant.cell_id()
+                &&& P::inv(
+                    constant.user_constant(),
+                    resource.value(),
+                    resource.predicate_state(),
+                )
+            }
+        }
+    }
+}
+
+} // verus!
+
 /// A spin lock.
 ///
 /// # Guard behavior
@@ -45,28 +156,29 @@ use super::{guard::SpinGuardian, LocalIrqDisabled /*, PreemptDisabled*/};
 /// We present its formally verified version and invariant below.
 ///
 /// The `lock` field is extended with a [`PointsTo<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PointsTo.html)
-/// ghost permission to track the ownership of the protected data. This ghost permission is also checked by Rust's ownership and borrowing rules and cannot be duplicated,
-/// thereby ensuring exclusive access to the protected data.
+/// ghost permission and the state associated with a user-supplied [`SpinLockPredicate`].
+/// These tracked resources are also checked by Rust's ownership and borrowing rules and cannot be
+/// duplicated, thereby ensuring exclusive access to the protected data and predicate state.
 /// The `val` field is a [`PCell<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PCell.html), which behaves like [`UnsafeCell<T>`](https://doc.rust-lang.org/std/cell/struct.UnsafeCell.html) used in the Asterinas mainline, but
 /// only allows verified access through the ghost permission.
 ///
-/// When the internal `AtomicBool` is `true`, the permission has been transferred to a `SpinLockGuard` and no one else can acquire the lock.
-/// When it is `false`, the permission to access the `PCell<T>` is stored in the lock, and it must match the `val`'s id.
+/// When the internal `AtomicBool` is `true`, both resources have been transferred to a
+/// `SpinLockGuard`, so the user predicate may temporarily be broken. When it is `false`, both
+/// resources are stored in the lock, the permission must match the `val`'s ID, and the user
+/// predicate must hold.
 /// ```rust
-/// struct_with_invariants! {
-/// struct SpinLockInner<T> {
-///    lock: AtomicBool<_,Option<PointsTo<T>>,_>,
+/// struct SpinLockInner<T, P: SpinLockPredicate<T>> {
+///    lock: AtomicBool<
+///        SpinLockConstant<P::Constant>,
+///        Option<SpinLockResource<T, P>>,
+///        SpinLockAtomicPredicate<T, P>,
+///    >,
 ///    val: PCell<T>,
 /// }
 ///
 /// closed spec fn wf(self) -> bool {
-///    invariant on lock with (val) is (v:bool, g:Option<PointsTo<T>>) {
-///        match g {
-///            None => v == true,
-///            Some(perm) => perm.id() == val.id() && !v
-///        }
-///    }
-/// }
+///    self.lock.well_formed()
+///        && self.lock.constant().cell_id() == self.val.id()
 /// }
 /// ```
 ///
@@ -83,40 +195,39 @@ use super::{guard::SpinGuardian, LocalIrqDisabled /*, PreemptDisabled*/};
 #[repr(transparent)]
 #[verus_verify]
 //pub struct SpinLock<T: ?Sized, G = PreemptDisabled> {
-pub struct SpinLock<T, G> {
+pub struct SpinLock<T, G, P: SpinLockPredicate<T> = TrivialSpinLockPredicate> {
     phantom: PhantomData<G>,
     /// Only the last field of a struct may have a dynamically sized type.
     /// That's why SpinLockInner is put in the last field.
-    inner: SpinLockInner<T>,
+    inner: SpinLockInner<T, P>,
 }
 
-struct_with_invariants! {
-struct SpinLockInner<T> {
-    lock: AtomicBool<_,Option<PointsTo<T>>,_>,
+#[verus_verify]
+struct SpinLockInner<T, P: SpinLockPredicate<T>> {
+    lock: AtomicBool<
+        SpinLockConstant<P::Constant>,
+        Option<SpinLockResource<T, P>>,
+        SpinLockAtomicPredicate<T, P>,
+    >,
     val: PCell<T>, //TODO: Waiting the new PCell that supports ?Sized
-    //val: UnsafeCell<T>,
-}
-
-closed spec fn wf(self) -> bool {
-    invariant on lock with (val) is (v:bool, g:Option<PointsTo<T>>) {
-        match g {
-            None => v == true,
-            Some(perm) => perm.id() == val.id() && !v
-        }
-    }
-}
+                   //val: UnsafeCell<T>,
 }
 
 verus! {
-impl<T> SpinLockInner<T>
+impl<T, P: SpinLockPredicate<T>> SpinLockInner<T, P>
 {
+    closed spec fn wf(self) -> bool {
+        &&& self.lock.well_formed()
+        &&& self.lock.constant().cell_id() == self.val.id()
+    }
+
     #[verifier::type_invariant]
     closed spec fn type_inv(self) -> bool{
         self.wf()
     }
 }
 
-impl<T, G> SpinLock<T, G> {
+impl<T, G> SpinLock<T, G, TrivialSpinLockPredicate> {
     /// Creates a new spin lock.
     ///
     /// # Verified Properties
@@ -128,10 +239,37 @@ impl<T, G> SpinLock<T, G> {
     /// - The function will not panic.
     /// - The created spin lock satisfies the invariant.
     pub const fn new(val: T) -> Self
+    {
+        Self::new_with_pred(val, Ghost(()), Tracked(()))
+    }
+}
+
+impl<T, G, P: SpinLockPredicate<T>> SpinLock<T, G, P> {
+    /// Creates a spin lock with a user-supplied invariant and its initial
+    /// tracked state.
+    pub const fn new_with_pred(
+        val: T,
+        Ghost(user_constant): Ghost<P::Constant>,
+        Tracked(state): Tracked<P::State>,
+    ) -> (res: Self)
+        requires
+            P::inv(user_constant, val, state),
+        ensures
+            res.constant() == user_constant,
     {
         let (val, Tracked(perm)) = PCell::new(val);
+        let ghost constant = SpinLockConstant { cell_id: val.id(), user_constant };
+        let tracked resource = SpinLockResource { perm, state };
         let lock_inner = SpinLockInner {
-            lock: AtomicBool::new(Ghost(val),false,Tracked(Some(perm))),
+            lock: AtomicBool::<
+                SpinLockConstant<P::Constant>,
+                Option<SpinLockResource<T, P>>,
+                SpinLockAtomicPredicate<T, P>,
+            >::new(
+                Ghost(constant),
+                false,
+                Tracked(Some(resource)),
+            ),
             //val: UnsafeCell::new(val),
             val: val,
         };
@@ -142,13 +280,18 @@ impl<T, G> SpinLock<T, G> {
     }
 }
 
-impl<T,G> SpinLock<T,G>
+impl<T, G, P: SpinLockPredicate<T>> SpinLock<T, G, P>
 {
     /// Returns the unique [`CellId`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/struct.CellId.html) of the internal `PCell<T>`.
     pub closed spec fn cell_id(self) -> cell::CellId {
         self.inner.val.id()
     }
 
+    /// The immutable user constant associated with the spin-lock predicate.
+    pub closed spec fn constant(self) -> P::Constant {
+        self.inner.lock.constant().user_constant()
+    }
+
     /// Public well-formedness predicate for external wrappers.
     pub closed spec fn wf(self) -> bool {
         self.type_inv()
@@ -177,7 +320,7 @@ impl<T: ?Sized> SpinLock<T, PreemptDisabled> {
 }*/
 
 #[verus_verify]
-impl<T /*: ?Sized */, G: SpinGuardian> SpinLock<T, G> {
+impl<T /*: ?Sized */, G: SpinGuardian, P: SpinLockPredicate<T>> SpinLock<T, G, P> {
     /// Acquires the spin lock.
     ///
     /// # Verified Properties
@@ -186,37 +329,47 @@ impl<T /*: ?Sized */, G: SpinGuardian> SpinLock<T, G> {
     /// ## Preconditions
     /// None. (The invariant of `SpinLock` always holds internally.)
     /// ## Postconditions
-    /// The returned `SpinLockGuard` satisfies its type invariant:
+    /// The returned `SpinLockGuard` satisfies its type invariant and the user-supplied predicate:
     /// - An exclusive permission to access the protected data is held by the guard.
     /// - The guard's permission matches the lock's internal cell ID.
+    /// - The protected value and tracked predicate state satisfy the predicate.
     /// ## Key Verification Step
     /// When the internal atomic compare-and-exchange operation in `acquire_lock` succeeds,
-    /// the ghost permission is simultaneously extracted from the lock.
+    /// the ghost permission and predicate state are simultaneously extracted from the lock.
     /// ```rust
     /// atomic_with_ghost!  {
     ///    self.inner.lock => compare_exchange(false, true);
     ///    returning res;
-    ///    ghost cell_perm => {
-    ///     // Extract the ghost permission when the lock is successfully acquired
+    ///    ghost lock_resource => {
+    ///     // Extract the resources when the lock is successfully acquired.
     ///     if res is Ok {
-    ///            perm = Some(cell_perm.tracked_take());
+    ///            resource = Some(lock_resource.tracked_take());
     ///        }
     ///    }
     ///}.is_ok()
     /// ```
-    pub fn lock(&self) -> SpinLockGuard<'_, T, G> {
+    #[verus_spec(ret =>
+        ensures
+            ret.constant() == self.constant(),
+            ret.predicate_inv(),
+    )]
+    pub fn lock(&self) -> SpinLockGuard<'_, T, G, P> {
         // Notice the guard must be created before acquiring the lock.
         proof!{ use_type_invariant(self);}
         proof_decl!{
-            let tracked perm: PointsTo<T>;
+            let tracked resource: SpinLockResource<T, P>;
         }
         let inner_guard = G::guard();
-        proof_with! {=> Tracked(perm)}
+        proof_with! {=> Tracked(resource)}
         self.acquire_lock();
+        proof_decl! {
+            let tracked SpinLockResource { perm, state } = resource;
+        }
         SpinLockGuard {
             lock: self,
             guard: inner_guard,
             tracked_perm: Tracked(perm),
+            tracked_state: Tracked(Some(state)),
         }
     }
 
@@ -231,16 +384,27 @@ impl<T /*: ?Sized */, G: SpinGuardian> SpinLock<T, G> {
     /// If `Some(guard)` is returned, it satisfies its type invariant:
     /// - An exclusive permission to access the protected data is held by the guard.
     /// - The guard's permission matches the lock's internal cell ID.
-    pub fn try_lock(&self) -> Option<SpinLockGuard<'_, T, G>> {
+    #[verus_spec(ret =>
+        ensures
+            ret is Some ==> {
+                &&& ret->0.constant() == self.constant()
+                &&& ret->0.predicate_inv()
+            },
+    )]
+    pub fn try_lock(&self) -> Option<SpinLockGuard<'_, T, G, P>> {
         let inner_guard = G::guard();
         proof_decl!{
-            let tracked mut perm: Option<PointsTo<T>> = None;
+            let tracked mut resource: Option<SpinLockResource<T, P>> = None;
         }
-        if #[verus_spec(with => Tracked(perm))] self.try_acquire_lock() {
+        if #[verus_spec(with => Tracked(resource))] self.try_acquire_lock() {
+            proof_decl! {
+                let tracked SpinLockResource { perm, state } = resource.tracked_unwrap();
+            }
             let lock_guard = SpinLockGuard {
                 lock: self,
                 guard: inner_guard,
-                tracked_perm: Tracked(perm.tracked_unwrap()),
+                tracked_perm: Tracked(perm),
+                tracked_state: Tracked(Some(state)),
             };
             return Some(lock_guard);
         }
@@ -259,36 +423,46 @@ impl<T /*: ?Sized */, G: SpinGuardian> SpinLock<T, G> {
     /// Acquires the spin lock, otherwise busy waiting
     #[verus_spec(ret =>
         with
-            -> perm: Tracked<PointsTo<T>>,
+            -> resource: Tracked<SpinLockResource<T, P>>,
         ensures
-            perm@.id() == self.inner.val.id(),
+            resource@.perm.id() == self.inner.val.id(),
+            P::inv(self.constant(), resource@.value(), resource@.predicate_state()),
             )]
     #[verifier::exec_allows_no_decreases_clause]
     fn acquire_lock(&self) {
         proof_decl!{
-            let tracked mut perm: Option<PointsTo<T>> = None;
+            let tracked mut resource: Option<SpinLockResource<T, P>> = None;
         }
         proof!{ use_type_invariant(self);}
         #[verus_spec(
             invariant self.type_inv(),
         )]
-        while !#[verus_spec(with => Tracked(perm))]self.try_acquire_lock() {
+        while !#[verus_spec(with => Tracked(resource))]self.try_acquire_lock() {
             core::hint::spin_loop();
         }
 
         proof_decl!{
-            let tracked mut perm = perm.tracked_unwrap();
+            let tracked resource = resource.tracked_unwrap();
         }
         // VERUS LIMITATION： Explicit return value to bind the ghost permission return value
-        #[verus_spec(with |= Tracked(perm))]
+        #[verus_spec(with |= Tracked(resource))]
         ()
     }
 
     #[verus_spec(ret =>
         with
-            -> perm: Tracked<Option<PointsTo<T>>>,
+            -> resource: Tracked<Option<SpinLockResource<T, P>>>,
         ensures
-            ret && perm@ is Some && perm@ -> Some_0.id() == self.inner.val.id() || !ret && perm@ is None,
+            ret ==> {
+                &&& resource@ is Some
+                &&& resource@->0.perm.id() == self.inner.val.id()
+                &&& P::inv(
+                    self.constant(),
+                    resource@->0.value(),
+                    resource@->0.predicate_state(),
+                )
+            },
+            !ret ==> resource@ is None,
             )]
     fn try_acquire_lock(&self) -> bool {
         /*self.inner
@@ -296,16 +470,16 @@ impl<T /*: ?Sized */, G: SpinGuardian> SpinLock<T, G> {
             .compare_exchange(false, true, Ordering::Acquire, Ordering::Relaxed)
             .is_ok()*/
         proof_decl!{
-            let tracked mut perm: Option<PointsTo<T>> = None;
+            let tracked mut resource: Option<SpinLockResource<T, P>> = None;
         }
         proof!{ use_type_invariant(self);}
-        proof_with!{ |= Tracked(perm)}
+        proof_with!{ |= Tracked(resource)}
         atomic_with_ghost!  {
             self.inner.lock => compare_exchange(false, true);
             returning res;
-            ghost cell_perm => {
+            ghost lock_resource => {
                 if res is Ok {
-                    perm = Some(cell_perm.tracked_take());
+                    resource = Some(lock_resource.tracked_take());
                 }
             }
         }.is_ok()
@@ -313,9 +487,10 @@ impl<T /*: ?Sized */, G: SpinGuardian> SpinLock<T, G> {
 
     #[verus_spec(
         with
-            Tracked(perm): Tracked<PointsTo<T>>,
+            Tracked(resource): Tracked<SpinLockResource<T, P>>,
         requires
-            perm.id() == self.inner.val.id(),
+            resource.perm.id() == self.inner.val.id(),
+            P::inv(self.constant(), resource.value(), resource.predicate_state()),
     )]
     fn release_lock(&self) {
         proof!{
@@ -324,8 +499,8 @@ impl<T /*: ?Sized */, G: SpinGuardian> SpinLock<T, G> {
         //self.inner.lock.store(false, Ordering::Release);
         atomic_with_ghost!{
             self.inner.lock => store(false);
-            ghost cell_perm => {
-                cell_perm = Some(perm);
+            ghost lock_resource => {
+                lock_resource = Some(resource);
             }
         }
     }
@@ -341,17 +516,18 @@ impl<T: ?Sized + fmt::Debug, G> fmt::Debug for SpinLock<T, G> {
 
 // SAFETY: Only a single lock holder is permitted to access the inner data of Spinlock.
 #[verifier::external]
-unsafe impl<T: Send, G> Send for SpinLock<T, G> {}
+unsafe impl<T: Send, G, P: SpinLockPredicate<T>> Send for SpinLock<T, G, P> {}
 #[verifier::external]
-unsafe impl<T: Send, G> Sync for SpinLock<T, G> {}
+unsafe impl<T: Send, G, P: SpinLockPredicate<T>> Sync for SpinLock<T, G, P> {}
 
 /// A guard that provides exclusive access to the data protected by a [`SpinLock`].
 ///
 /// # Verified Properties
 /// ## Verification Design
-/// The guard is extended with a ghost permission field `tracked_perm` that
-/// holds the ghost permission ([`PointsTo<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PointsTo.html))
-/// This permission grants exclusive ownership of the protected data and enables verified access to the `PCell<T>`.
+/// The guard is extended with tracked fields holding both the ghost permission
+/// ([`PointsTo<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PointsTo.html))
+/// and the user-supplied predicate state. The permission grants exclusive ownership of the
+/// protected data and enables verified access to the `PCell<T>`.
 ///
 ///
 /// ## Invariant
@@ -373,15 +549,22 @@ unsafe impl<T: Send, G> Sync for SpinLock<T, G> {}
 #[clippy::has_significant_drop]
 #[must_use]
 #[verus_verify]
-pub struct SpinLockGuard<'a, T /*: ?Sized*/, G: SpinGuardian> {
+pub struct SpinLockGuard<
+    'a,
+    T, /*: ?Sized*/
+    G: SpinGuardian,
+    P: SpinLockPredicate<T> = TrivialSpinLockPredicate,
+> {
     guard: G::Guard,
-    lock: &'a SpinLock<T, G>,
-    /// Ghost permission for verification
+    lock: &'a SpinLock<T, G, P>,
+    /// Ghost permission for the protected value.
     tracked_perm: Tracked<PointsTo<T>>,
+    /// User-supplied predicate state.
+    tracked_state: Tracked<Option<P::State>>,
 }
 
 verus! {
-impl<'a, T, G: SpinGuardian> SpinLockGuard<'a, T, G>
+impl<'a, T, G: SpinGuardian, P: SpinLockPredicate<T>> SpinLockGuard<'a, T, G, P>
 {
     #[verifier::type_invariant]
     spec fn type_inv(self) -> bool{
@@ -393,10 +576,76 @@ impl<'a, T, G: SpinGuardian> SpinLockGuard<'a, T, G>
         *self.tracked_perm@.value()
     }
 
+    /// The tracked state used by the user-supplied predicate.
+    pub closed spec fn predicate_state(self) -> P::State
+        recommends
+            self.has_predicate_state(),
+    {
+        self.tracked_state@->0
+    }
+
+    /// Whether the guard currently owns its predicate state.
+    pub closed spec fn has_predicate_state(self) -> bool {
+        self.tracked_state@ is Some
+    }
+
+    /// The immutable user constant associated with the guarded spin lock.
+    pub closed spec fn constant(self) -> P::Constant {
+        self.lock.constant()
+    }
+
+    /// Whether the user-supplied invariant currently holds.
+    pub open spec fn predicate_inv(self) -> bool {
+        &&& self.has_predicate_state()
+        &&& P::inv(self.constant(), self.value(), self.predicate_state())
+    }
+
     /// The value stored in the lock. It is an alias of `Self::value`.
     pub open spec fn view(self) -> T {
         self.value()
     }
+
+    /// Temporarily takes ownership of the user-supplied predicate state.
+    #[verus_spec(ret =>
+        with
+            -> state: Tracked<P::State>,
+        requires
+            old(self).has_predicate_state(),
+        ensures
+            state@ == old(self).predicate_state(),
+            !final(self).has_predicate_state(),
+            final(self).value() == old(self).value(),
+            final(self).constant() == old(self).constant(),
+    )]
+    pub fn take_predicate_state(&mut self) {
+        proof! {
+            use_type_invariant(&*self);
+        }
+        proof_decl! {
+            let tracked state = OptionAdditionalFns::tracked_take(&mut *self.tracked_state);
+        }
+        #[verus_spec(with |= Tracked(state))]
+        ()
+    }
+
+    /// Returns the user-supplied predicate state to the guard.
+    #[verus_spec(
+        with
+            Tracked(state): Tracked<P::State>,
+        requires
+            !old(self).has_predicate_state(),
+        ensures
+            final(self).has_predicate_state(),
+            final(self).predicate_state() == state,
+            final(self).value() == old(self).value(),
+            final(self).constant() == old(self).constant(),
+    )]
+    pub fn put_predicate_state(&mut self) {
+        proof! {
+            use_type_invariant(&*self);
+            *self.tracked_state = Some(state);
+        }
+    }
 }
 /*
 impl<T: ?Sized, G: SpinGuardian> AsAtomicModeGuard for SpinLockGuard<'_, T, G> {
@@ -407,7 +656,9 @@ impl<T: ?Sized, G: SpinGuardian> AsAtomicModeGuard for SpinLockGuard<'_, T, G> {
 
 // FIXME: fix when verus attribute syntax supports Tracked.
 #[verus_verify]
-impl<T: /*?Sized*/, G: SpinGuardian> Deref for SpinLockGuard<'_, T, G> {
+impl<T: /*?Sized*/, G: SpinGuardian, P: SpinLockPredicate<T>> Deref
+    for SpinLockGuard<'_, T, G, P>
+{
     type Target = T;
 
     #[verus_spec(returns self.view())]
@@ -427,11 +678,17 @@ impl<T: /*?Sized*/, G: SpinGuardian> Deref for SpinLockGuard<'_, T, G> {
 
 
 #[verus_verify]
-impl<T: /* ?Sized */, G: SpinGuardian> DerefMut for SpinLockGuard<'_, T, G> {
+impl<T: /* ?Sized */, G: SpinGuardian, P: SpinLockPredicate<T>> DerefMut
+    for SpinLockGuard<'_, T, G, P>
+{
     #[verus_spec(ret =>
         ensures
             final(self).view() == *final(ret),
             old(self).view() == *ret,
+            final(self).has_predicate_state() == old(self).has_predicate_state(),
+            old(self).has_predicate_state() ==> final(self).predicate_state()
+                == old(self).predicate_state(),
+            final(self).constant() == old(self).constant(),
     )]
     fn deref_mut(&mut self) -> &mut Self::Target
     {
@@ -452,12 +709,20 @@ impl<T: /* ?Sized */, G: SpinGuardian> DerefMut for SpinLockGuard<'_, T, G> {
 */
 
 #[verus_verify]
-impl<'a, T /*:?Sized */, G: SpinGuardian> SpinLockGuard<'a, T, G> {
+impl<'a, T /*:?Sized */, G: SpinGuardian, P: SpinLockPredicate<T>> SpinLockGuard<'a, T, G, P> {
     /// VERUS LIMITATION: We implement `drop` and call it manually because Verus's support for `Drop` is incomplete for now.
-    #[verus_spec]
+    #[verus_spec(
+        requires
+            self.predicate_inv(),
+    )]
     pub fn drop(self) {
         proof! {use_type_invariant(&self);}
-        proof_with!(self.tracked_perm);
+        proof_decl! {
+            let tracked perm = self.tracked_perm.get();
+            let tracked state = self.tracked_state.get().tracked_unwrap();
+            let tracked resource = SpinLockResource { perm, state };
+        }
+        proof_with!(Tracked(resource));
         self.lock.release_lock();
     }
 }
@@ -469,9 +734,9 @@ impl<'a, T /*:?Sized */, G: SpinGuardian> SpinLockGuard<'a, T, G> {
 }*/
 
 #[verus_verify]
-impl<T: ?Sized, G: SpinGuardian> !Send for SpinLockGuard<'_, T, G> {}
+impl<T: ?Sized, G: SpinGuardian, P: SpinLockPredicate<T>> !Send for SpinLockGuard<'_, T, G, P> {}
 
 #[verifier::external]
 // SAFETY: `SpinLockGuard` can be shared between tasks/threads in same CPU.
 // As `lock()` is only called when there are no race conditions caused by interrupts.
-unsafe impl<T: Sync, G: SpinGuardian> Sync for SpinLockGuard<'_, T, G> {}
+unsafe impl<T: Sync, G: SpinGuardian, P: SpinLockPredicate<T>> Sync for SpinLockGuard<'_, T, G, P> {}
diff --git a/ostd/src/sync/wait.rs b/ostd/src/sync/wait.rs
index fa5bec971..2800f304d 100644
--- a/ostd/src/sync/wait.rs
+++ b/ostd/src/sync/wait.rs
@@ -1,12 +1,16 @@
 // SPDX-License-Identifier: MPL-2.0
 use vstd::atomic_ghost::*;
 use vstd::prelude::*;
+use vstd::resource::{
+    Loc,
+    ghost_var::{GhostVar, GhostVarAuth},
+};
 
 use alloc::{collections::VecDeque, sync::Arc};
 use core::intrinsics::atomic_cxchg;
 use core::sync::atomic::{/*AtomicBool,*/ Ordering};
 
-use super::{LocalIrqDisabled, SpinLock};
+use super::{LocalIrqDisabled, SpinLock, SpinLockPredicate};
 use crate::task::{Task, scheduler};
 
 // # Explanation on the memory orders
@@ -39,6 +43,22 @@ use crate::task::{Task, scheduler};
 
 verus! {
 
+struct WakersPredicate;
+
+impl SpinLockPredicate<VecDeque<Arc<Waker>>> for WakersPredicate {
+    type Constant = Loc;
+
+    type State = GhostVar<int>;
+
+    /// While the spin lock is unlocked, its mirror records the exact queue
+    /// length. Lock acquisition transfers the mirror to the guard, allowing
+    /// the relation to be updated together with `num_wakers` before unlock.
+    closed spec fn inv(ghost_id: Loc, wakers: VecDeque<Arc<Waker>>, mirror: GhostVar<int>) -> bool {
+        &&& mirror.id() == ghost_id
+        &&& mirror@ == wakers@.len()
+    }
+}
+
 struct_with_invariants! {
 
 /// A wait queue.
@@ -49,13 +69,16 @@ struct_with_invariants! {
 /// wake up one or many waiting threads.
 pub struct WaitQueue {
     // A copy of `wakers.len()`, used for the lock-free fast path in `wake_one` and `wake_all`.
-    num_wakers: AtomicU32<_, (), _>,
-    wakers: SpinLock<VecDeque<Arc<Waker>>, LocalIrqDisabled>,
+    num_wakers: AtomicU32<_, GhostVarAuth<int>, _>,
+    wakers: SpinLock<VecDeque<Arc<Waker>>, LocalIrqDisabled, WakersPredicate>,
 }
 
 closed spec fn wf(self) -> bool {
-    invariant on num_wakers is (v: u32, g: ()) {
-        true
+    // The authoritative half agrees with the executable atomic counter. Its
+    // ID links it to the mirror protected by `wakers`.
+    invariant on num_wakers with (wakers) is (v: u32, g: GhostVarAuth<int>) {
+        &&& g.id() == wakers.constant()
+        &&& g@ == v as int
     }
 }
 }
@@ -70,10 +93,16 @@ impl WaitQueue {
 impl WaitQueue {
     /// Creates a new, empty wait queue.
     pub const fn new() -> Self {
-        WaitQueue {
-            num_wakers: AtomicU32::new(Ghost(()), 0, Tracked(())),
-            wakers: SpinLock::new(VecDeque::new()),
+        proof_decl! {
+            let tracked (count_auth, count_mirror) = GhostVarAuth::<int>::new(0int);
         }
+        let ghost ghost_id = count_auth.id();
+        let wakers = SpinLock::new_with_pred(
+            VecDeque::new(),
+            Ghost(ghost_id),
+            Tracked(count_mirror),
+        );
+        WaitQueue { num_wakers: AtomicU32::new(Ghost(wakers), 0, Tracked(count_auth)), wakers }
     }
 
     /// Waits until some condition is met.
@@ -131,15 +160,26 @@ impl WaitQueue {
         {
             let mut wakers = self.wakers.lock();
             let Some(waker) = wakers.pop_front() else {
+                wakers.drop();
                 return false;
             };
+            proof_decl! {
+                let tracked mut count_mirror: GhostVar<int>;
+            }
+            #[verus_spec(with => Tracked(count_mirror))]
+            wakers.take_predicate_state();
             atomic_with_ghost! {
                 self.num_wakers => fetch_sub(1);
                 update prev -> next;
-                ghost g => {
-                    assume(prev > 0);
+                ghost count_auth => {
+                    count_auth.agree(&count_mirror);
+                    assert(prev == count_mirror@);
+                    assert(prev > 0);
+                    count_auth.update(&mut count_mirror, next);
                 }
             };
+            #[verus_spec(with Tracked(count_mirror))]
+            wakers.put_predicate_state();
             // Avoid holding lock when calling `wake_up`
             //drop(wakers);
             wakers.drop();
@@ -169,15 +209,26 @@ impl WaitQueue {
         {
             let mut wakers = self.wakers.lock();
             let Some(waker) = wakers.pop_front() else {
+                wakers.drop();
                 break;
             };
+            proof_decl! {
+                let tracked mut count_mirror: GhostVar<int>;
+            }
+            #[verus_spec(with => Tracked(count_mirror))]
+            wakers.take_predicate_state();
             atomic_with_ghost! {
                 self.num_wakers => fetch_sub(1);
                 update prev -> next;
-                ghost g => {
-                    assume(prev > 1);
+                ghost count_auth => {
+                    count_auth.agree(&count_mirror);
+                    assert(prev == count_mirror@);
+                    assert(prev > 0);
+                    count_auth.update(&mut count_mirror, next);
                 }
             };
+            #[verus_spec(with Tracked(count_mirror))]
+            wakers.put_predicate_state();
             // Avoid holding lock when calling `wake_up`
             //drop(wakers);
             wakers.drop();
@@ -191,8 +242,10 @@ impl WaitQueue {
         num_woken
     }
 
-    #[verifier::external_body]
     fn is_empty(&self) -> bool {
+        proof! {
+            use_type_invariant(self);
+        }
         self.num_wakers.load() == 0
     }
 
@@ -204,13 +257,24 @@ impl WaitQueue {
         }
         let mut wakers = self.wakers.lock();
         wakers.push_back(waker);
+        proof_decl! {
+            let tracked mut count_mirror: GhostVar<int>;
+        }
+        #[verus_spec(with => Tracked(count_mirror))]
+        wakers.take_predicate_state();
         atomic_with_ghost! {
             self.num_wakers => fetch_add(1);
             update prev -> next;
-            ghost g => {
+            ghost count_auth => {
+                count_auth.agree(&count_mirror);
+                assert(prev == count_mirror@);
                 assume(prev < u32::MAX);
+                count_auth.update(&mut count_mirror, next);
             }
         };
+        #[verus_spec(with Tracked(count_mirror))]
+        wakers.put_predicate_state();
+        wakers.drop();
     }
 }