diff --git a/rocq-brick-libstdcpp/proof/mutex/inc.hpp b/rocq-brick-libstdcpp/proof/mutex/inc.hpp
index ccb7a7c..0bdd0c2 100644
--- a/rocq-brick-libstdcpp/proof/mutex/inc.hpp
+++ b/rocq-brick-libstdcpp/proof/mutex/inc.hpp
@@ -1,3 +1,10 @@
 #include <mutex>
 
 template class std::lock_guard<std::mutex>;
+template class std::unique_lock<std::mutex>;
+template class std::scoped_lock<std::mutex, std::mutex>;
+
+inline void foo() {
+  std::mutex m1, m2;
+  std::scoped_lock lock(m1, m2);
+}
diff --git a/rocq-brick-libstdcpp/proof/mutex/scoped_lock_spec.v b/rocq-brick-libstdcpp/proof/mutex/scoped_lock_spec.v
new file mode 100644
index 0000000..6be2e73
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/scoped_lock_spec.v
@@ -0,0 +1,149 @@
+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.
+
+Module scoped_lock.
+  Section with_cpp.
+    Context `{Σ : cpp_logic}.
+
+    (* Parameter gname : Set. *)
+    Parameter R : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
+      cQp.t -> list (ptr * gname * Qp * mpred) -> Rep.
+
+    #[only(type_ptr="std::scoped_lock<std::mutex, std::mutex>")] derive R.
+
+    Section with_threads.
+      Context {σ : genv}.
+      Context `{HAS_THREADS : !HasStdThreads Σ}.
+
+      cpp.spec
+      "std::scoped_lock<...<std::mutex, std::mutex>>::scoped_lock(std::mutex&, std::mutex&)"
+      (* "std::scoped_lock<std::mutex, std::mutex>::scoped_lock(std::mutex&, std::mutex&)" *)
+      as ctor_spec from source with (
+        \this this
+        \arg{mp1} "" (Vptr mp1)
+        \pre{g1 q1 P1} mp1 |-> mutex.R g1 q1$m P1
+        \pre mutex.token g1 q1
+        \arg{mp2} "" (Vptr mp2)
+        \pre{g2 q2 P2} mp2 |-> mutex.R g2 q2$m P2
+        \pre mutex.token g2 q2
+        \persist{thr} current_thread thr
+        \post
+          this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)] **
+          P1 ** mutex.locked g1 thr q1 **
+          P2 ** mutex.locked g2 thr q2
+      ).
+
+      cpp.spec "std::scoped_lock<...<std::mutex, std::mutex>>::~scoped_lock()"
+        as dtor_spec from source with (
+        \this this
+        \persist{thr} current_thread thr
+        \pre{
+          mp1 mp2
+          g1 q1 P1
+          g2 q2 P2
+        }
+          this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)]
+        \pre |> P1
+        \pre |> P2
+        \pre mutex.locked g1 thr q1
+        \pre mutex.locked g2 thr q2
+        \post
+          mp1 |-> mutex.R g1 q1$m P1 ** mutex.token g1 q1 **
+          mp2 |-> mutex.R g2 q2$m P2 ** mutex.token g2 q2
+      ).
+
+      cpp.spec "foo()" as foo_spec from source with
+      (
+        \persist{thr} current_thread thr
+        \post emp
+      ).
+
+      (* #[only(cfracsplittable)] derive R. *)
+      #[only(cfractional,ascfractional,cfracvalid)] derive R.
+
+      Lemma foo_ok : verify[source] foo_spec.
+      Proof.
+        verify_spec; go.
+        iExists emp; go.
+        iExists emp; go.
+        Fail solve [ego].
+        ework.
+        ego.
+
+        (**
+        (** Weird failure! *)
+        ego.
+  match args_for <$> as_function (normalize_type ?ty0) with
+  | Some _ =>
+  eval evaluation_order.nd (map (wp_operand ?tu ?ρ) ?es0)
+  (λ (vs : list val) (free : FreeTemps),
+  builtins.wp_builtin ?f0 ?ty0 vs
+  (λ v : val,
+  match v with
+  | Vptr obj_ptr =>
+  if bool_decide (obj_ptr = nullptr)
+  then wp_delete_null ?default_delete ?destroyed_type (?Q Vvoid free)
+  else
+  new_delete.wp_delete_dispatch.body ?default_delete ?destroyed_type obj_ptr
+  (?Q Vvoid free)
+  | _ => False
+  end))
+  | None => errors.Errors.ERROR.body "builtin does not have function type"%bs
+  end ∗
+  match args_for <$> as_function (normalize_type ?ty) with
+  | Some _ =>
+  eval evaluation_order.nd (map (wp_operand ?tu0 ?ρ0) ?es)
+  (λ (vs : list val) (free : FreeTemps),
+  builtins.wp_builtin ?f ?ty vs
+  (λ v : val,
+  match v with
+  | Vptr obj_ptr =>
+  if bool_decide (obj_ptr = nullptr)
+  then wp_delete_null ?default_delete0 ?destroyed_type0 (?Q0 Vvoid free)
+  else
+  new_delete.wp_delete_dispatch.body ?default_delete0 ?destroyed_type0 obj_ptr
+  (?Q0 Vvoid free)
+  | _ => False
+  end))
+  | None => errors.Errors.ERROR.body "builtin does not have function type"%bs
+  end ∗
+  lock_addr
+  |-> R 1$m
+  [(?p, ?g, ?q,
+  ::wpOperand
+  ?ρ
+  (Edelete false ?default_delete
+  (Ecall (Ecast (Cbuiltin2fun (Tptr [...])) (Eglobal (Nglobal [...]) ?ty0)) ?es0)
+  ?destroyed_type));
+  (?p0, ?g0, ?q0,
+  ::wpOperand
+  ?ρ0
+  (Edelete false ?default_delete0
+  (Ecall (Ecast (Cbuiltin2fun (Tptr [...])) (Eglobal (Nglobal [...]) ?ty)) ?es)
+  ?destroyed_type0))] ∗ mutex.locked ?g thr ?q ∗ mutex.locked ?g0 thr ?q0 ∗
+  (?p
+  |-> mutex.R ?g ?q$m
+  (::wpOperand
+  ?ρ
+  (Edelete false ?default_delete
+  (Ecall (Ecast (Cbuiltin2fun ([...])) (Eglobal ([...]) ?ty0)) ?es0)
+  ?destroyed_type)) ∗ mutex.token ?g ?q ∗
+  ?p0
+  |-> mutex.R ?g0 ?q0$m
+  (::wpOperand
+  ?ρ0
+  (Edelete false ?default_delete0
+  (Ecall (Ecast (Cbuiltin2fun ([...])) (Eglobal ([...]) ?ty)) ?es)
+  ?destroyed_type0)) ∗ mutex.token ?g0 ?q0 -∗
+  interp source ((1 >*> FreeTemps.delete "std::mutex" m2_addr) >*>
+  FreeTemps.delete "std::mutex" m1_addr)
+  (∀ p : ptr, p |-> primR "void" 1$m Vvoid -∗ ▷ _PostPred_ p))
+        *)
+      Qed.
+    End with_threads.
+  End with_cpp.
+
+End scoped_lock.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
new file mode 100644
index 0000000..5f42cc3
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
@@ -0,0 +1,76 @@
+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.
+
+Module scoped_lock.
+  Section with_cpp.
+    Context `{Σ : cpp_logic}.
+
+    (* Parameter gname : Set. *)
+    Parameter R : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
+      cQp.t -> list (ptr * gname * Qp * mpred) -> Rep.
+
+    #[only(type_ptr="std::scoped_lock<std::mutex, std::mutex>")] derive R.
+    #[only(cfractional,ascfractional,cfracvalid)] derive R.
+
+    Section with_threads.
+      Context {σ : genv}.
+      Context `{HAS_THREADS : !HasStdThreads Σ}.
+
+      #[global] Instance: LearnEqF1 R := ltac:(solve_learnable).
+
+      cpp.spec
+      "std::scoped_lock<...<std::mutex, std::mutex>>::scoped_lock(std::mutex&, std::mutex&)"
+      (* "std::scoped_lock<std::mutex, std::mutex>::scoped_lock(std::mutex&, std::mutex&)" *)
+      as ctor_spec from source with (
+        \this this
+        \arg{mp1} "" (Vptr mp1)
+        \pre{g1 q1 P1} mp1 |-> mutex.R g1 q1$m P1
+        \pre mutex.token g1 q1
+        \arg{mp2} "" (Vptr mp2)
+        \pre{g2 q2 P2} mp2 |-> mutex.R g2 q2$m P2
+        \pre mutex.token g2 q2
+        \persist{thr} current_thread thr
+        \post
+          this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)] **
+          P1 ** mutex.locked g1 thr q1 **
+          P2 ** mutex.locked g2 thr q2
+      ).
+
+      cpp.spec "std::scoped_lock<...<std::mutex, std::mutex>>::~scoped_lock()"
+        as dtor_spec from source with (
+        \this this
+        \persist{thr} current_thread thr
+        \pre{
+          mp1 mp2
+          g1 q1 P1
+          g2 q2 P2
+        }
+          this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)]
+        \pre |> P1
+        \pre |> P2
+        \pre mutex.locked g1 thr q1
+        \pre mutex.locked g2 thr q2
+        \post
+          mp1 |-> mutex.R g1 q1$m P1 ** mutex.token g1 q1 **
+          mp2 |-> mutex.R g2 q2$m P2 ** mutex.token g2 q2
+      ).
+
+      cpp.spec "foo()" as foo_spec from source with
+      (
+        \persist{thr} current_thread thr
+        \post emp
+      ).
+
+      Lemma foo_ok : verify[source] foo_spec.
+      Proof.
+        verify_spec; go.
+        iExists emp; go.
+        iExists emp; go.
+      Qed.
+    End with_threads.
+  End with_cpp.
+
+End scoped_lock.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
new file mode 100644
index 0000000..7c86a6f
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@@ -0,0 +1,216 @@
+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.
+
+Module unique_lock.
+Section with_cpp.
+  Context `{Σ : cpp_logic}.
+
+    (* Parameter gname : Set. *)
+    (* 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 {HAS_THREADS : HasStdThreads Σ} {σ : genv},
+      cQp.t -> option (bool * (ptr * gname * Qp * mpred)) -> Rep.
+
+    Definition owned (om : option (bool * (ptr * gname * Qp * mpred))) : bool :=
+      match om with
+      | Some (own, _) => own
+      | None => false
+      end.
+
+    Definition mutex (om : option (bool * (ptr * gname * Qp * mpred))) : ptr :=
+      match om with
+      | Some (_, (mp, g, q, P)) => mp
+      | None => nullptr
+      end.
+
+    (* #[only(type_ptr="std::unique_lock<std::mutex>")] derive R. *)
+
+    Section with_threads.
+      Context {σ : genv}.
+      Context `{HAS_THREADS : !HasStdThreads Σ}.
+
+      (* TODO maybe a class / interface Lockable that exposes do_lock, do_unlock
+         and the rep predicate R, formalizing the C++ lockable concept
+         <https://en.cppreference.com/w/cpp/named_req/Lockable.html>.
+
+         Instantiate with mutex, recursive_mutex, maybe in different styles (AC
+         and invariant styles).
+      *)
+
+      (*
+      TODO: could we write something like this?
+      Definition do_unlock_spec_body (thr : thread_idT) (lk : ptr * gname * Qp * mpred) (Q : mpred) : WpSpec_cpp :=
+        match lk with
+        | (mp, g, q, P) =>
+        \pre mutex.locked g thr q
+        \pre ▷P
+        \post mutex.token g q
+        end.
+        *)
+
+      Definition do_unlock (thr : thread_idT) (lk : ptr * gname * Qp * mpred) (Q : mpred) : mpred :=
+        match lk with
+        | (mp, g, q, P) =>
+          mutex.locked g thr q ** ▷P ** ▷(mutex.token g q -* Q)
+        end.
+
+      Definition do_lock (thr : thread_idT) (lk : ptr * gname * Qp * mpred) (Q : mpred) : mpred :=
+        match lk with
+        | (mp, g, q, P) =>
+          mutex.token g q ** ▷(mutex.locked g thr q ** ▷P -* Q)
+        end.
+
+      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{g q P} mp |-> mutex.R g q$m P
+        \persist{thr} current_thread thr
+        \pre{K} do_lock thr (mp, g, q, P) K
+        \post
+          this |-> R 1$m (Some (true, (mp, g, q, P))) **
+          K
+      ).
+
+      cpp.spec "std::unique_lock<std::mutex>::unique_lock(std::mutex&)" as mutex_ctor_spec from source with (
+        \this this
+        \arg{mp} "" (Vptr mp)
+        \pre{g q P} mp |-> mutex.R g q$m P
+        \pre mutex.token g q
+        \persist{thr} current_thread thr
+        \post
+          this |-> R 1$m (Some (true, (mp, g, q, P))) **
+          P ** mutex.locked g thr q
+      ).
+
+      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{g q P} mp |-> mutex.R g q$m P
+        \arg{def_p} "" (Vptr def_p)
+        \post this |-> R 1$m (Some (false, (mp, g, q, P)))
+      ).
+
+      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
+      ).
+
+      (* unlock the associated mutex, if any  *)
+      Definition ensure_unlock (thr : thread_idT) (om : option (bool * (ptr * gname * Qp * mpred))) (Q : mpred) : mpred :=
+        match om with
+        | Some (true, mm) => do_unlock thr mm Q
+        | Some (false, (mp, g, q, P)) =>
+          ▷ (mp |-> mutex.R g q$m P -* Q)
+        | _ => (* TODO should this be [bi_later Q]? *) Q
+        end.
+
+      (* 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
+        \persist{thr} current_thread thr
+        \pre{om} this |-> R 1$m om
+        \pre{K}
+          ensure_unlock thr om K
+        \post K
+        ).
+
+      cpp.spec "std::unique_lock<std::mutex>::~unique_lock()" as dtor_spec from source with (
+        \this this
+        \persist{thr} current_thread thr
+        \pre{om} this |-> R 1$m om
+        \pre
+          match om with
+          | Some (true, (mp, g, q, P)) => mutex.locked g thr q ** ▷P
+          | _ => emp
+          end
+        \post
+          match om with
+          | Some (true, (mp, g, q, P)) => mp |-> mutex.R g q$m P ** mutex.token g q
+          | Some (false, (mp, g, q, P)) => mp |-> mutex.R g q$m P
+          | 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
+        \persist{thr} current_thread thr
+        \pre{K}
+          ensure_unlock thr 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
+          match om1 with
+          | Some (true, (mp, g, q, P)) => mutex.locked g thr q ** ▷P
+          | _ => emp
+          end
+        \post
+          this |-> R 1$m om2 **
+          other |-> R 1$m None **
+          match om1 with
+          | Some (true, (mp, g, q, P)) => mp |-> mutex.R g q$m P ** mutex.token g q
+          | Some (false, (mp, g, q, P)) => mp |-> mutex.R g q$m P
+          | 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
+      ).
+
+      (* 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{mp g q P} this |-> R 1$m (Some (false, (mp, g, q, P)))
+        \pre mutex.token g q
+        \persist{thr} current_thread thr
+        \post
+          this |-> R 1$m (Some (true, (mp, g, q, P))) **
+          P ** mutex.locked g thr q).
+    End with_threads.
+End with_cpp.
+End unique_lock.