diff --git a/rocq-brick-libstdcpp/proof/mutex/requirements.v b/rocq-brick-libstdcpp/proof/mutex/requirements.v
new file mode 100644
index 0000000..4e0427a
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/requirements.v
@@ -0,0 +1,64 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+
+(** This file captures the following "named requirements":
+    - [BasicLockable](https://cppreference.com/cpp/named_req/BasicLockable)
+    - [Lockable](https://cppreference.com/cpp/named_req/Lockable)
+
+    It proposes a pattern for capturing these using Rocq typeclasses such
+    that clients can use these to depend on
+ *)
+
+Section with_cpp.
+  Context `{Σ : cpp_logic} {σ : genv}.
+
+  (* NOTE: This is *not* meant to be a statement about the way that
+     things should be packaged (bundled or unbundled), just a demonstration
+     of the way that specifications can be written in a higher-order way.
+   *)
+
+  (** This captures [BasicLockable](https://cppreference.com/cpp/named_req/BasicLockable) *)
+  Class BasicLockable (ty : type) {T : Type} (R : cQp.t -> T -> Rep) : Type :=
+  { do_lock : ptr -> T -> mpred -> mpred
+    (* the WP for <ty::lock()> *)
+  ; do_unlock : ptr -> T -> mpred -> mpred
+    (* the WP for <ty::unlock()> *)
+  }.
+  (** TODO: consider adding a Hint Mode*)
+  (*
+  #[global] Hint Mode BasicLockable ! - ! : typeclass_instances.
+  #[global] Arguments do_lock ty {T} R {BL} _ _ _ : rename.
+  #[global] Arguments do_unlock ty {T} R {BL} _ _ _ : rename.
+  *)
+
+  Section with_BasicLockable.
+    Context (ty : type) {T: Type} (R : cQp.t -> T -> Rep) {BL : BasicLockable ty R}.
+
+    Definition lock_basic_lockable : ptr -> WpSpec mpred val val :=
+      (\this this
+       \prepost{q m} this |-> R q m
+       \pre{K} do_lock this m K
+       \post K).
+
+    Definition unlock_basic_lockable : ptr -> WpSpec mpred val val :=
+      (\this this
+       \prepost{q m} this |-> R q m
+       \pre{K} do_unlock this m K
+       \post K).
+  End with_BasicLockable.
+
+  (** This captures [Lockable](https://cppreference.com/cpp/named_req/Lockable) *)
+  Class Lockable (ty : type) {T : Type} (R : cQp.t -> T -> Rep) {BASIC_LOCKABLE : BasicLockable ty R} : Type :=
+  { do_try_lock : ptr -> T -> (bool -> mpred) -> mpred }.
+  (* TODO: Hint Mode here too. *)
+
+  Section with_Lockable.
+    Context (ty : type) {T : Type} (R : cQp.t -> T -> Rep) `{LOCKABLE : Lockable (T:=T) ty R}.
+
+    Definition try_lock_lockable : ptr -> WpSpec mpred val val :=
+      (\this this
+       \prepost{q m} this |-> R q m
+       \pre{K} do_try_lock this m K
+       \post{r}[Vbool r] K r).
+  End with_Lockable.
+
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v
index 4264c53..c5e4344 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec.v
@@ -1,5 +1,8 @@
-Require Export skylabs.brick.libstdcpp.mutex.spec.mutex.
+(* Export all specifications.
+Keep them listed in alphabetical order. *)
+Require Export skylabs.brick.libstdcpp.mutex.spec.defer_lock_t.
 Require Export skylabs.brick.libstdcpp.mutex.spec.lock_guard.
+Require Export skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Export skylabs.brick.libstdcpp.mutex.spec.recursive_mutex.
 Require Export skylabs.brick.libstdcpp.mutex.spec.scoped_lock.
 Require Export skylabs.brick.libstdcpp.mutex.spec.unique_lock.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/defer_lock_t.v b/rocq-brick-libstdcpp/proof/mutex/spec/defer_lock_t.v
new file mode 100644
index 0000000..e9bbd60
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/defer_lock_t.v
@@ -0,0 +1,23 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+
+Module defer_lock_t.
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Parameter R : forall {σ : genv}, cQp.t -> Rep.
+  #[only(cfracsplittable, type_ptr="std::defer_lock_t")] derive R.
+
+  cpp.spec "std::defer_lock_t::defer_lock_t(const std::defer_lock_t&)" as defer_lock_copy_ctor_spec from source with (
+    \this this
+    \arg{other} "other" (Vptr other)
+    \prepost{q} other |-> R q
+    \post this |-> R 1$m
+  ).
+  cpp.spec "std::defer_lock_t::~defer_lock_t()" as defer_lock_dtor_spec from source with (
+    \this this
+    \pre this |-> R 1$m
+    \post emp
+  ).
+End with_cpp.
+End defer_lock_t.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
index a687349..7600867 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
@@ -7,9 +7,11 @@ Require Import skylabs.bi.weakly_objective.
 Require Import skylabs.auto.cpp.weakly_local_with.
 
 Require Import skylabs.auto.cpp.spec.
+Require Import skylabs.auto.cpp.proof.
 Require Export skylabs.brick.libstdcpp.runtime.pred.
 
 Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+Require Import skylabs.brick.libstdcpp.mutex.requirements.
 
 Import linearity.
 
@@ -59,6 +61,24 @@ Section with_cpp.
   Context `{MOD : source ⊧ σ}.
   Context {HAS_THREADS : HasStdThreads Σ}.
 
+  Definition do_unlock (thr : thread_idT) (lk : gname * Qp * mpred) (Q : mpred) : mpred :=
+      match lk with
+      | (g, q, P) =>
+        locked g thr q ** ▷P **
+        (* TODO readd *)
+        (* ▷ *)
+        (token g q -* Q)
+      end.
+
+  Definition do_lock (thr : thread_idT) (lk : gname * Qp * mpred) (K: mpred) : mpred :=
+      match lk with
+      | (g, q, P) =>
+        token g q **
+        (* TODO readd *)
+        (* ▷ *)
+        (locked g thr q ** ▷P -* K)
+      end.
+
   cpp.spec "std::mutex::mutex()" as ctor_spec with
       (\this this
       \pre{P} ▷P
@@ -75,6 +95,14 @@ Section with_cpp.
       \pre token g q
       \post P ** locked g thr q).
 
+  cpp.spec "std::mutex::lock()" as lock_spec_alt with
+      (\this this
+      \prepost{q P g} this |-> R g q$m P (* part of both pre and post *)
+      \persist{thr} current_thread thr
+      \pre{K} do_lock thr (g, q, P) K
+      \post K
+      ).
+
   cpp.spec "std::mutex::try_lock()" as try_lock_spec with
       (\this this
       \prepost{q P g} this |-> R g q P (* part of both pre and post *)
@@ -90,11 +118,44 @@ Section with_cpp.
       \pre ▷P
       \post token g q).
 
+  cpp.spec "std::mutex::unlock()" as unlock_spec_alt with
+      (\this this
+      \prepost{q P g} this |-> R g q$m P (* part of both pre and post *)
+      \persist{thr} current_thread thr
+      \pre{K} do_unlock thr (g, q, P) K
+      \post K).
+
   cpp.spec "std::mutex::~mutex()" as dtor_spec with
       (\this this
       \pre{g P} this |-> R g 1$m P ** token g 1
       \post P).
 
+  Lemma lock_spec_entails_lock_spec_alt : lock_spec |-- lock_spec_alt.
+  Proof.
+    apply specify_mono.
+    rewrite /do_lock.
+    go. iExists q$m%cQp. go.
+  Qed.
+
+  Lemma unlock_spec_entails_unlock_spec_alt : unlock_spec |-- unlock_spec_alt.
+  Proof.
+    apply specify_mono.
+    rewrite /do_unlock.
+    go. iExists q$m%cQp. go.
+  Qed.
+
+  (* candidate? *)
+  Definition T : Type := gname * mpred.
+
+  #[global,program] Instance mutex_basic_lockable : BasicLockable (T := thread_idT * gname * Qp * mpred) "std::mutex" (λ q '(thr, γ, q', P), R γ q$m P) :=
+  { do_lock := fun this '(thr, γ, q', P) K => do_lock thr (γ, q', P) K
+  ; do_unlock := fun this '(thr, γ, q', P) K => do_unlock thr (γ, q', P) K }.
+
+  (*
+  #[global,program] Instance mutex_basic_lockable : BasicLockable (T := gname * Qp * mpred) "std::mutex" (λ q '(thr, γ, q', P), R γ q$m P) :=
+  { do_lock := fun this '(γ, q', P) K => do_lock thr (γ, q', P) K
+  ; do_unlock := fun this '(γ, q', P) K => do_unlock thr (γ, q', P) K }.
+  *)
 End with_cpp.
 End mutex.
 
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
index 47f86e1..ae2ce6c 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@@ -4,27 +4,6 @@ Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
 Require Export skylabs.brick.libstdcpp.runtime.pred.
 Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
 
-Module defer_lock_t.
-Section with_cpp.
-  Context `{Σ : cpp_logic, σ : genv}.
-
-  Parameter R : forall {σ : genv}, cQp.t -> Rep.
-  #[only(cfracsplittable, type_ptr="std::defer_lock_t")] derive R.
-
-  cpp.spec "std::defer_lock_t::defer_lock_t(const std::defer_lock_t&)" as defer_lock_copy_ctor_spec from source with (
-    \this this
-    \arg{other} "other" (Vptr other)
-    \prepost{q} other |-> R q
-    \post this |-> R 1$m
-  ).
-  cpp.spec "std::defer_lock_t::~defer_lock_t()" as defer_lock_dtor_spec from source with (
-    \this this
-    \pre this |-> R 1$m
-    \post emp
-  ).
-End with_cpp.
-End defer_lock_t.
-
 Module unique_lock.
 Section with_cpp.
   Context `{Σ : cpp_logic}.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
new file mode 100644
index 0000000..c168700
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
@@ -0,0 +1,222 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+
+Require Export skylabs.brick.libstdcpp.runtime.pred.
+Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
+Require Import skylabs.brick.libstdcpp.mutex.requirements.
+
+
+Module unique_lock.
+Section with_cpp.
+  Context `{Σ : cpp_logic}.
+
+  Record M {T : Type} : Type :=
+  { is_held : bool
+  ; mutex_ptr : ptr
+  ; mutex_q : Qp
+  ; mutex_m : T }.
+  #[global] Arguments M _ : clear implicits.
+  #[only(lens)] derive M.
+
+  (* a unique_lock may have an associated mutex, if so it holds
+      (Some (b * mutex_state)) where b indicates whether the unique_lock
+      has acquired the associated mutex. *)
+  Parameter R : forall {σ : genv} ty {T} mutexR `{!BasicLockable ty (T:=T) mutexR},
+    cQp.t -> option (M T) -> Rep.
+
+  Definition owned {T} (om : option (M T)) : bool :=
+    match om with
+    | Some m => m.(is_held)
+    | None => false
+    end.
+
+  Definition mutex {T} (om : option (M T)) : ptr :=
+    match om with
+    | Some m => m.(mutex_ptr)
+    | None => nullptr
+    end.
+
+  #[global] Declare Instance R_cfrac {σ : genv} `{!BasicLockable ty (T:=T) mutexR} :
+    CFractional1 mutexR ->
+    CFractional1 (R ty mutexR).
+
+  #[global] Instance R_as_cfrac {σ : genv} `{!BasicLockable ty (T:=T) mutexR} :
+    CFractional1 mutexR ->
+    AsCFractional1 (R ty mutexR).
+  Proof. solve_as_cfrac. Qed.
+
+  (* #[global] Declare Instance R_timeless {σ : genv} `{!BasicLockable ty (T:=T) mutexR} : *)
+  (*   Timeless2 mutexR -> *)
+  (*   Timeless2 (R ty mutexR). *)
+
+  #[global] Declare Instance R_cfrac_valid {σ : genv} `{!BasicLockable ty (T:=T) mutexR} :
+    CFracValid1 (R ty mutexR).
+
+  #[global] Declare Instance R_type_ptr {σ : genv} `{!BasicLockable ty (T:=T) mutexR} q om :
+    Typed ("std::unique_lock" .<< Atype ty >>) (R ty mutexR q om).
+
+  Section with_threads.
+    Context {σ : genv}.
+
+    Context `{HAS_THREADS : !HasStdThreads Σ}.
+    Context ty {mutexT} mutexR `{!BasicLockable ty (T:=mutexT) mutexR}.
+
+    #[global] Instance: LearnEqF1 (R ty mutexR) := ltac:(solve_learnable).
+    #[local] Notation R := (R ty (T:=mutexT) mutexR).
+
+    (* TODO: all the following specs should be generalized over the lock type, except for [lock_spec] and [unlock_spec]. *)
+
+    cpp.spec "std::unique_lock<std::mutex>::unique_lock()"
+      as default_ctor_spec from source with (
+      \this this
+      \post this |-> R 1$m None
+    ).
+
+    cpp.spec "std::unique_lock<std::mutex>::unique_lock(std::mutex&)" as mutex_ctor_spec_alt from source with (
+      \this this
+      \arg{mp} "" (Vptr mp)
+      \pre{q m} mp |-> mutexR q$m m
+      \pre{K} do_lock mp m K
+      \post
+        this |-> R 1$m (Some {| is_held := true ; mutex_ptr := mp ; mutex_q := q ; mutex_m := m |}) **
+        K
+    ).
+
+    cpp.spec "std::unique_lock<std::mutex>::unique_lock(std::mutex&, std::defer_lock_t)" as mutex_defer_ctor_spec from source with (
+      \this this
+      \arg{mp} "" (Vptr mp)
+      \pre{q m} mp |-> mutexR q$m m
+      \arg{def_p} "" (Vptr def_p)
+      \post this |-> R 1$m (Some {| is_held := false ; mutex_ptr := mp ; mutex_q := q ; mutex_m := m |})
+    ).
+
+    cpp.spec "std::unique_lock<std::mutex>::unique_lock(std::unique_lock<std::mutex> &&)" as move_ctor_spec from source with (
+      \this this
+      \arg{other} "" (Vptr other)
+      \pre{om} other |-> R 1$m om
+      \post
+        this |-> R 1$m om **
+        other |-> R 1$m None
+    ).
+
+    (** Ensures the associated mutex is unlocked and released. *)
+    Definition ensure_unlock (om : option (M mutexT)) (Q : mpred) : mpred :=
+      match om with
+      | Some {| is_held := is_held ; mutex_ptr := mp ; mutex_q := q ; mutex_m := m |} =>
+        if is_held then
+          letI* := do_unlock mp m in
+          mp |-> mutexR q$m m -* Q
+        else
+          ▷ (mp |-> mutexR q$m m -* Q)
+      | _ =>
+      (* TODO should this be [bi_later Q]? *)
+        Q
+      end%I.
+
+    (* spec for dtor written with do_unlock.
+    Should be equivalent to dtor_spec. *)
+    cpp.spec "std::unique_lock<std::mutex>::~unique_lock()" as dtor_spec_alt from source with (
+      \this this
+      \pre{om} this |-> R 1$m om
+      \pre{K} ensure_unlock om K
+      \post K
+      ).
+
+    cpp.spec "std::unique_lock<std::mutex>::~unique_lock()" as dtor_spec from source with (
+      \this this
+      \pre{om} this |-> R 1$m om
+      \pre{K}
+        match om with
+        | Some m =>
+            if m.(is_held) then do_unlock m.(mutex_ptr) m.(mutex_m) K
+            else K
+        | _ => K
+        end
+      \post K **
+        match om with
+        | Some m => m.(mutex_ptr) |-> mutexR m.(mutex_q)$m m.(mutex_m)
+        | None => emp
+        end
+      ).
+
+    (* unlock the associated mutex, if any, and set input as the associated mutex.
+    Should be equivalent to move_assign_spec. *)
+    cpp.spec "std::unique_lock<std::mutex>::operator=(std::unique_lock<std::mutex> &&)" as move_assign_spec_alt from source with (
+      \this this
+      \arg{other} "" (Vptr other)
+      \pre{om1} this |-> R 1$m om1
+      \pre{om2} other |-> R 1$m om2
+      \pre{K} ensure_unlock om1 K
+      \post
+        this |-> R 1$m om2 **
+        other |-> R 1$m None **
+        K
+      ).
+
+    cpp.spec "std::unique_lock<std::mutex>::operator=(std::unique_lock<std::mutex> &&)" as move_assign_spec from source with (
+      \this this
+      \arg{other} "" (Vptr other)
+      \pre{om1} this |-> R 1$m om1
+      \pre{om2} other |-> R 1$m om2
+      \persist{thr} current_thread thr
+      \pre{K}
+        match om1 with
+        | Some m =>
+            if m.(is_held) then do_unlock m.(mutex_ptr) m.(mutex_m) K
+            else K
+        | _ => K
+        end
+      \post
+        this |-> R 1$m om2 **
+        other |-> R 1$m None **
+        K **
+        match om1 with
+        | Some m => m.(mutex_ptr) |-> mutexR m.(mutex_q)$m m.(mutex_m)
+        | None => emp
+        end
+      ).
+
+    Notation owns_lock_spec_body := (
+      \this this
+      \prepost{om q} this |-> R q om
+      \post [Vbool (owned om)] emp) (only parsing).
+
+    cpp.spec "std::unique_lock<std::mutex>::owns_lock() const" as owns_lock_spec
+      from source with (owns_lock_spec_body).
+
+    cpp.spec "std::unique_lock<std::mutex>::operator bool() const" as operator_bool_spec
+      from source with (owns_lock_spec_body).
+
+    cpp.spec "std::unique_lock<std::mutex>::mutex() const" as mutex_spec from source with (
+      \this this
+      \prepost{om q} this |-> R q om
+      \post[Vptr (mutex om)] emp
+    ).
+
+    (* TODO: these specs seem mutex-specific. unlock_spec doesn't seem good for recursive mutexes. *)
+
+    (* these preconditions statically rule out cases that throw exceptions, such as:
+    - If there is no associated mutex, std::system_error with an error code of std::errc::operation_not_permitted.
+    - If the mutex is already locked by this unique_lock (in other words, owns_lock() is true), std::system_error with an error code of std::errc::resource_deadlock_would_occur. *)
+    cpp.spec "std::unique_lock<std::mutex>::lock()" as lock_spec from source with (
+      \this this
+      \pre{mm} this |-> R 1$m (Some mm)
+      \require ~~ mm.(is_held)
+      \pre{K} do_lock mm.(mutex_ptr) mm.(mutex_m) K
+      \post
+        this |-> R 1$m (Some (mm &: _is_held .= true)%lens) **
+        K).
+
+    cpp.spec "std::unique_lock<std::mutex>::unlock()" as unlock_spec from source with (
+      \this this
+      \pre{mm} this |-> R 1$m (Some mm)
+      \require mm.(is_held)
+      \pre{K} do_unlock mm.(mutex_ptr) mm.(mutex_m) K
+      \post
+        this |-> R 1$m (Some (mm &: _is_held .= false)%lens) **
+        K
+    ).
+
+  End with_threads.
+End with_cpp.
+End unique_lock.