diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index 52ff904b..dbb871ac 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -167,6 +167,18 @@
   	 (with-stderr-to inc_new_cpp.v.stderr (run cpp2v -v %{input} -o inc_new_cpp.v --no-elaborate --templates=inc_new_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_new.cpp))
 )
+(subdir pthread
+ (rule
+  (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)
+  (alias test_ast)
+  (deps
+   (:input inc.hpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc.hpp))
+)
 (subdir semaphore
  (rule
   (targets inc_hpp.v.stderr inc_hpp.v inc_hpp_templates.v)
diff --git a/rocq-brick-libstdcpp/proof/pthread/hints.v b/rocq-brick-libstdcpp/proof/pthread/hints.v
new file mode 100644
index 00000000..a50d7a56
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/hints.v
@@ -0,0 +1,70 @@
+(*
+ * Copyright (c) 2025 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.brick.libstdcpp.pthread.pred.
+Require Import skylabs.brick.libstdcpp.pthread.spec.
+Require Import skylabs.auto.cpp.prelude.spec.
+
+Section with_cpp.
+  Import pthread.
+  Import auto.telescopes auto.telescopes.TeleNotations.
+
+  Context `{Σ : cpp_logic, σ : genv}.
+  Context `{!HasStdThreads Σ}.
+
+  Class ThreadFunction (nm : globname) (P : mpred)
+      (argT : tele)
+      (Pre : ptr -> argT -> mpred)
+      (Post : ptr -> argT -> thread_idT -> mpred) :=
+    thread_function : P |-- _global nm |-> unmaterialized_specR starter_kind (starter_spec _ Pre Post).
+  #[global] Hint Mode ThreadFunction + + - - - : typeclass_instances.
+
+  #[program]
+  Definition fptr_spec_C P nm argT' Pre' Post' :=
+    \cancelx
+    \using P
+    \guard ThreadFunction nm P argT' Pre' Post'
+    \bound argT Pre Post
+    \proving _global nm |-> starter_specR argT Pre Post
+    \let P0 := fun t => ptr → tele_arg t → mpred
+    \let P1 := fun t => ptr → tele_arg t → thread_idT → mpred
+    (* \let P2 := fun t0 t1 => ptr -> tele_arg t0 → tele_arg t1 → mpred *)
+    (* \let x := existT (P := fun t => ptr → tele_arg t → ptr → mpred) argT  *)
+    (* \through [|  = existT argT' Pre' |] *)
+    \through [| existT (P := P0) argT Pre = existT argT' Pre' |]
+    \through [| existT (P := P1) argT Post = existT argT' Post' |]
+    \end.
+  Admit Obligations.
+
+  #[program]
+  Definition exists_tele_app_B {PROP : bi} {t : tele} (P : t -pt> PROP) :=
+    \cancelx
+    \bound_existential x
+    \proving tele_app P x
+    \through (∃p.. a, {instantiate x := a} ∗ tele_app P a)%I
+    \end.
+  Admit Obligations.
+
+  #[program]
+  Definition exists_tele_app_boxed_F {PROP : bi} {t : tele} (P : t -pt> PROP) x `{!IsAnyVariable x} :=
+    \fwd
+    \using □ tele_app P x
+    \deduce (∃p.. a, [| x = a |] ∗ tele_app P a)%I
+    \end.
+  Admit Obligations.
+  #[program]
+  Definition exists_tele_app_F {PROP : bi} {t : tele} (P : t -pt> PROP) x `{!IsAnyVariable x} :=
+    \fwd
+    \using tele_app P x
+    \deduce (∃p.. a, [| x = a |] ∗ tele_app P a)%I
+    \end.
+  Admit Obligations.
+
+End with_cpp.
+
+#[global] Hint Resolve fptr_spec_C : br_hints.
+#[global] Hint Resolve exists_tele_app_B : br_hints.
+#[global] Hint Resolve exists_tele_app_F | 1 : br_hints.
+#[global] Hint Resolve exists_tele_app_boxed_F | 0 : br_hints.
diff --git a/rocq-brick-libstdcpp/proof/pthread/inc.hpp b/rocq-brick-libstdcpp/proof/pthread/inc.hpp
new file mode 100644
index 00000000..46ddc5be
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/inc.hpp
@@ -0,0 +1,7 @@
+/*
+ * Copyright (c) 2025 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ */
+
+#include <pthread.h>
diff --git a/rocq-brick-libstdcpp/proof/pthread/pred.v b/rocq-brick-libstdcpp/proof/pthread/pred.v
new file mode 100644
index 00000000..109bc066
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/pred.v
@@ -0,0 +1,70 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Export skylabs.brick.libstdcpp.runtime.pred.
+Require Export skylabs.brick.libstdcpp.runtime.objective.
+
+Require Import skylabs.auto.cpp.prelude.spec.
+(* TODO: add this to a prelude *)
+Require Import skylabs.cpp.slice.
+
+Require Import skylabs.brick.libstdcpp.pthread.inc_hpp.
+
+Import wrap.
+
+Module pthread.
+
+  Record gname := { _ghost : iprop.gname }.
+
+  (** [handle γ spawner tid P Pc] is a token returned when thread creation succeeds. [P] and [Pc]
+      are respectively the postcondition of the thread and its cancelation postcondition. [handle]
+      can be given to <<pthread_join>> to retrieve ownership of left by a thread's termination. It
+      can also be given to <<pthread_cancel>> to retrieve resources from the aborted thread.
+
+      [handle] also specifies the thread id of the spawning thread so that the precondition of [pthread_join]
+      can rule out two threads trying to mutually join with each other.  *)
+  Parameter handle : forall `{Σ : cpp_logic,!HasStdThreads Σ}
+                       (γ : gname) (spawner tid : thread_idT)
+                       (Post : mpred), mpred.
+
+  mlock
+  Definition R `{Σ : cpp_logic, σ : genv} (q : cQp.t) (id : thread_idT) :=
+    ulongR q (unwrapN id).
+  #[only(cfractional,cfracvalid,ascfractional,type_ptr,lazy_unfold)] derive R.
+
+  (* TODO: fix [lazy_unfold] derivation. [q] and [q'] need to be distinct variables. *)
+  #[global] Instance R_defined_using' `{Σ : cpp_logic, σ : genv} (q q' : cQp.t) (id : thread_idT) (arg : val) :
+    lazy_unfold.AutoUnlocking.DefinedUsing
+      (pthread.R q id)
+      (primR "unsigned long" q' arg) := {}.
+
+  Section with_cpp.
+    Import rep.RepFor.
+    Import RepScheme.
+
+    Context `{Σ : cpp_logic,σ : genv,!HasStdThreads Σ}.
+
+    #[global] Instance R_learnable :
+        Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) R) := ltac:(solve_learnable).
+
+
+    Definition learn_eq_dep {T U V} : Learning V → Learning (forall x : T, U x → V) :=
+      fun '{|unLearning := k|} =>
+        {|unLearning := fun L R ls => forall a a' b b', k (L a b) (R a' b') ((existT a b = existT a' b') :: ls) |}.
+
+    #[global] Instance handle_learnable_1 :
+      Cbn (Learn (learn_eq ==> learn_eq ==> req_eq ==> learn_eq ==> learn_hints.fin)
+             pthread.handle) := ltac:(solve_learnable).
+
+    #[global] Instance handle_learnable_2 :
+      Cbn (Learn (req_eq ==> learn_eq ==> learn_eq ==> learn_eq ==> learn_hints.fin)
+             pthread.handle) := ltac:(solve_learnable).
+
+    #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
+      rep.RepFor.C "pthread_t" [ArgType.CFrac; ArgType.Model _]
+        R := {}.
+
+  End with_cpp.
+End pthread.
diff --git a/rocq-brick-libstdcpp/proof/pthread/spec.v b/rocq-brick-libstdcpp/proof/pthread/spec.v
new file mode 100644
index 00000000..f6d9df88
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/pthread/spec.v
@@ -0,0 +1,104 @@
+(*
+ * Copyright (c) 2025 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.brick.libstdcpp.pthread.pred.
+Require Import skylabs.brick.libstdcpp.pthread.inc_hpp.
+
+Require Export skylabs.bi.tls_modalities.
+
+Require Import skylabs.auto.cpp.prelude.spec.
+
+Module pthread.
+  Export pthread.
+  Import auto.telescopes auto.telescopes.TeleNotations.
+
+  (** [pthread] specs
+
+      This module specifies thread creation and joining. Unsupported are the following features of
+      pthread:
+      - detaching threads;
+      - canceling threads;
+      - joining a thread by threads other than their creator.
+
+      This prevents possible deadlocks when joining threads or race conditions when two threads both
+      try to cancel the same thread.
+   *)
+
+  Definition starter_kind : okind :=
+    tFunction (cc:=CC_C) "void*" ["void*"%cpp_type].
+
+  Definition starter_spec `{Σ : cpp_logic, σ : genv} `{!HasStdThreads Σ}
+      (argT : tele)
+      (Pre : ptr -> argT -> mpred)
+      (Post : ptr -> argT -> thread_idT -> mpred) : WpSpec_cpp_val :=
+    \arg{argp} "arg" (Vptr argp)
+    \prepost{tid} current_thread tid
+    \pre{arg} Pre argp arg
+    \post[Vptr nullptr] Post argp arg tid.
+
+  mlock
+  Definition starter_specR `{Σ : cpp_logic, σ : genv} `{!HasStdThreads Σ}
+      (argT : tele)
+      (Pre : ptr -> argT -> mpred)
+      (Post : ptr -> argT -> thread_idT -> mpred) : Rep :=
+    unmaterialized_specR starter_kind
+      (starter_spec argT Pre Post)  .
+
+Section with_cpp.
+
+  Context `{Σ : cpp_logic, σ : genv}.
+  Context `{!HasStdThreads Σ}.
+
+  cpp.spec "pthread_t::pthread_t()"
+    from source
+    as ctor_spec
+    with ( \this this
+           \post ∃ tid, this |-> pthread.R 1$m tid ).
+
+  cpp.spec "pthread_t::~pthread_t()"
+    from source
+    as dtor_spec
+    inline.
+
+  cpp.spec "pthread_create"
+     as create_spec
+     from source
+     with ( \arg{idp}        "tid"   (Vptr idp)
+            \pre{id0}         idp |-> oprimR "unsigned long" 1$m id0
+            \arg             "attr"  (Vptr nullptr)
+            \arg{starterp}   "start" (Vptr starterp)
+            \with argT Pre Post
+            \pre              starterp |-> starter_specR argT Pre Post
+            \arg{argp}       "arg"   (Vptr argp)
+            \pre{arg : argT}  Pre argp arg
+            \with this_thread
+            \prepost          current_thread this_thread
+            \require LocalWith procTI (Pre argp arg)
+            \require forall tid, LocalWith procTI (Post argp arg tid)
+            \post{err}[Vint err]
+               if bool_decide (err = 0) then
+                 ∃ γt tid,
+                   pthread.handle γt this_thread tid (Post argp arg tid) ∗
+                   idp |-> pthread.R 1$m tid
+               else
+                 Pre argp arg ∗
+                 idp |-> oprimR "unsigned long" 1$m id0 ).
+
+  cpp.spec "pthread_join"
+     as join_spec
+     from source
+     with ( \arg{tid}      "tid"   (Vthread tid)
+            \arg           "ret"   (Vptr nullptr)
+            \prepost{this_thread} current_thread this_thread
+            \pre{γ P}      pthread.handle γ this_thread tid P
+            \post[Vint 0] (* the precondition rules out the errors that [pthread_join] can report:
+                              - deadlocks
+                              - thread is not joinable (our specs don't allow us to create such threads yet)
+                              - thread id does not designate an existing thread
+                              - thread is being joined by other thread *)
+                 P ).
+
+End with_cpp.
+End pthread.
diff --git a/rocq-brick-libstdcpp/proof/runtime/objective.v b/rocq-brick-libstdcpp/proof/runtime/objective.v
new file mode 100644
index 00000000..3d176bea
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/runtime/objective.v
@@ -0,0 +1,123 @@
+
+Require Import skylabs.lang.cpp.logic.
+
+Require Import skylabs.bi.tls_modalities.
+Require Import skylabs.bi.tls_modalities_rep.
+Require Import skylabs.bi.weakly_objective.
+Require Import skylabs.cpp.slice.
+Require Import skylabs.auto.cpp.local_with.
+
+Require Export skylabs.brick.libstdcpp.runtime.pred.
+
+Require Import skylabs.iris.extra.proofmode.proofmode.
+
+Module Type PROC_OBJECTIVE_AXIOM_TYPE.
+Section proc_objective_axiom.
+  Context `{Σ : !cpp_logic ti Σ0, σ : genv, !HasStdThreads Σ}.
+
+  #[global] Declare Instance tptsto_pd_local_weakly_obj p ty q a :
+      LocalWith procTI (tptsto ty q p a).
+  #[global] Declare Instance padding_pd_local_weakly_obj q cls :
+      LocalWithR procTI (structR cls q).
+  #[global] Declare Instance mdc_path_pd_local_weakly_obj n path q p :
+      LocalWith procTI (mdc_path n path q p).
+  #[global] Declare Instance type_ptr_pd_local_weakly_obj p ty :
+      LocalWith procTI (type_ptr ty p).
+  #[global] Declare Instance valid_ptr_pd_local_weakly_obj p ty :
+      LocalWith procTI (_valid_ptr ty p).
+  #[global] Declare Instance anyR_pd_local_weakly_obj ty q :
+      LocalWithR procTI (anyR ty q).
+  #[global] Declare Instance has_type_pd_weakly_obj v ty :
+      LocalWith procTI (has_type v ty).
+End proc_objective_axiom.
+End PROC_OBJECTIVE_AXIOM_TYPE.
+
+Declare Module Export PROC_OBJECTIVE_AXIOM : PROC_OBJECTIVE_AXIOM_TYPE.
+
+Section derived_local_withR.
+  Context `{Σ : !cpp_logic ti Σ0, σ : genv, !HasStdThreads Σ}.
+  Implicit Types p : ptr.
+
+  #[global] Instance validR_pd_local_obj :
+    LocalWithR procTI validR.
+  Proof.
+    rewrite LocalWithR_iff_LocalWith_at => p.
+    rewrite _at_validR; apply _.
+  Qed.
+
+  #[global] Instance tptstoR_pd_local_obj ty q v :
+    LocalWithR procTI (tptstoR ty q v).
+  Proof.
+    rewrite LocalWithR_iff_LocalWith_at => p.
+    rewrite _at_tptstoR; apply _.
+  Qed.
+
+  #[global] Instance tptsto_fuzzyR_pd_local_obj ty q v :
+    LocalWithR procTI (tptsto_fuzzyR ty q v).
+  Proof.
+    rewrite LocalWithR_iff_LocalWith_at => p.
+    rewrite _at_tptsto_fuzzyR; apply _.
+  Qed.
+
+  #[global] Instance primR_pd_local_obj ty q v :
+    LocalWithR procTI (primR ty q v).
+  Proof.
+    rewrite LocalWithR_iff_LocalWith_at => p.
+    rewrite _at_primR; apply _.
+  Qed.
+
+  #[global] Instance uninitR_pd_local_obj ty q :
+    LocalWithR procTI (uninitR ty q).
+  Proof. rewrite uninitR.unlock; apply _. Qed.
+
+  #[global] Instance type_ptrR_pd_local_obj ty :
+    LocalWithR procTI (type_ptrR ty).
+  Proof. rewrite type_ptrR_eq /type_ptrR_def. apply _. Qed.
+
+  #[global] Instance derivationR_pd_local_obj n path q :
+    LocalWithR procTI (derivationR n path q).
+  Proof. rewrite derivationR.unlock. apply _. Qed.
+
+  (** TODO: allow references to list in assumptions:
+      << (∀ i x, xs !! i = Some x -> LocalWithR procTI (Rs x)) >>
+   *)
+  Lemma arrayR_pd_local_obj_lookup
+    {X} ty (Rs : X → Rep) (xs : list X) :
+    (∀ x, LocalWithR procTI (Rs x)) →
+    LocalWithR procTI (arrayR ty Rs xs).
+  Proof.
+    intros HRs.
+    rewrite arrayR_eq /arrayR_def arrR_eq /arrR_def.
+    repeat first [ apply sep_local_withR | apply _ ].
+    rewrite big_opL_fmap.
+    apply _.
+  Qed.
+
+  (** TODO: allow references to list in assumptions:
+      << (∀ i x, xs !! i = Some x -> LocalWithR procTI (Rs x)) >>
+   *)
+  Lemma array_sliceR_pd_local_obj_lookup m n
+    {X} ty (Rs : X → Rep) (xs : list X) :
+    (∀ x, LocalWithR procTI (Rs x)) →
+    LocalWithR procTI (array_sliceR ty m n Rs xs).
+  Proof.
+    intros HR.
+    rewrite array_sliceR.unlock.
+    apply sep_local_withR; first apply _.
+    apply LocalWithR_offsetR, arrayR_pd_local_obj_lookup => x.
+    apply _.
+  Qed.
+
+  #[global] Instance arrayR_pd_local_obj
+    {X} ty (Rs : X → Rep) (xs : list X)
+    `{∀ (x : X), LocalWithR procTI (Rs x)} :
+    LocalWithR procTI (arrayR ty Rs xs).
+  Proof. by apply arrayR_pd_local_obj_lookup, _. Qed.
+
+  #[global] Instance array_sliceR_pd_local_obj
+    {X} ty (Rs : X → Rep) (xs : list X) m n
+    `{∀ (x : X), LocalWithR procTI (Rs x)} :
+    LocalWithR procTI (array_sliceR ty m n Rs xs).
+  Proof. by apply array_sliceR_pd_local_obj_lookup, _. Qed.
+
+End derived_local_withR.
diff --git a/rocq-brick-libstdcpp/proof/runtime/pred.v b/rocq-brick-libstdcpp/proof/runtime/pred.v
index ca8c1c76..6fac343e 100644
--- a/rocq-brick-libstdcpp/proof/runtime/pred.v
+++ b/rocq-brick-libstdcpp/proof/runtime/pred.v
@@ -9,26 +9,35 @@ Require Import skylabs.auto.cpp.prelude.proof.
 Require Import skylabs.auto.core.hints.cancelx_notation.
 Require Import skylabs.iris.extra.proofmode.proofmode.
 
-Parameter thread_idT : Type.
-#[global] Declare Instance thread_idT_inh : Inhabited thread_idT.
-#[global] Declare Instance thread_idT_eq_dec : EqDecision thread_idT.
-#[global] Declare Instance thread_idT_countable : Countable thread_idT.
+Import wrap.
 
-Canonical Structure thread_idTO := leibnizO thread_idT.
+Variant ProcIdT := .
+Definition proc_idT := WrapN ProcIdT.
+Variant ThreadIdT := .
+Definition thread_idT := WrapN ThreadIdT.
+
+Canonical Structure proc_idTO := leibnizO proc_idT.
+Canonical Structure proc_idT_bi_index : biIndex := BiIndex proc_idT _ eq _.
 
+Canonical Structure thread_idTO := leibnizO thread_idT.
 Canonical Structure thread_idT_bi_index : biIndex := BiIndex thread_idT _ eq _.
 
 Parameter HasStdThreads : forall `{Σ : cpp_logic}, Type.
 #[global] Arguments HasStdThreads {_ _} Σ.
 Existing Class HasStdThreads.
 
-(** The projection of the thread from the thread information.
+(** The projection of respectively the process id and thread id from the
+    thread information.
 
   NOTE: This is effectively a field of `HasStdThreads`, but since that
   is registered as an Axiom, we use another Parameter for this.
   *)
+Parameter procTI : forall `{HasStdThreads}, thread_info -ml> proc_idT_bi_index.
 Parameter threadTI : forall `{HasStdThreads}, thread_info -ml> thread_idT_bi_index.
 
+Definition Vthread (tid : thread_idT) := Vn (unwrapN tid).
+#[global] Instance Vthread_type_compat : TypeCompat "unsigned long" Vthread := {}.
+
 (** [current_thread thr] means that the current thread is [thr].
 
     For more information on monalities, consult tls_modalities.
diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc
index 37b1b7bf..5ec8f414 100644
--- a/rocq-brick-libstdcpp/test/dune.inc
+++ b/rocq-brick-libstdcpp/test/dune.inc
@@ -311,6 +311,18 @@
   	 (with-stderr-to demo_cpp.v.stderr (run cpp2v -v %{input} -o demo_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps demo.cpp))
 )
+(subdir pthread
+ (rule
+  (targets test_cpp.v.stderr test_cpp.v)
+  (alias test_ast)
+  (deps
+   (:input test.cpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps test.cpp))
+)
 (subdir shared_mutex
  (rule
   (targets test_cpp.v.stderr test_cpp.v)
diff --git a/rocq-brick-libstdcpp/test/pthread/test.cpp b/rocq-brick-libstdcpp/test/pthread/test.cpp
new file mode 100644
index 00000000..3aebf9de
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/pthread/test.cpp
@@ -0,0 +1,52 @@
+
+#include <pthread.h>
+#include <cassert>
+
+void* thread_fn(void* data) {
+    int* counter = static_cast<int*>(data);
+    ++*counter;
+    return nullptr;
+}
+
+void multithreaded_broken () {
+    int counter = 0;
+    int err;
+    pthread_t child;
+
+    if (pthread_create(&child, nullptr, thread_fn, &counter) != 0)
+        return;
+    counter++; // problem here
+    pthread_join(child, nullptr);
+}
+
+void* cancelable_thread(void* data) {
+    int* counter = static_cast<int*>(data);
+    ++*counter;
+    pthread_testcancel();
+    ++*counter;
+    pthread_testcancel();
+    ++*counter;
+    return nullptr;
+}
+
+void multithreaded_ok () {
+    int counter1 = 0;
+    int counter2 = 0;
+    int err;
+    pthread_t child1, child2;
+
+    if (pthread_create(&child1, nullptr, thread_fn, &counter1) != 0)
+        return;
+    if (pthread_create(&child2, nullptr, cancelable_thread, &counter2) != 0) {
+        // Here, it is important that the precondition of `pthread_join` excludes dead-lock because
+        // otherwise, we could not retrieve the ownership of the local variable `counter1` when a
+        // deadlock is detected. The absence of deadlock is assured by requiring the thread that
+        // spawned a thread to also be the one to join it.
+        pthread_join(child1, nullptr);
+        return;
+    }
+    pthread_join(child2, nullptr);
+    pthread_join(child1, nullptr);
+    assert (counter1 == 1);
+    assert (counter2 == 3);
+}
diff --git a/rocq-brick-libstdcpp/test/pthread/test.v b/rocq-brick-libstdcpp/test/pthread/test.v
new file mode 100644
index 00000000..b3dfc068
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/pthread/test.v
@@ -0,0 +1,97 @@
+(*
+ * Copyright (c) 2025 SkyLabs AI, Inc.
+ * This software is distributed under the terms of the BedRock Open-Source License.
+ * See the LICENSE-BedRock file in the repository root for details.
+ *)
+Require Import skylabs.brick.libstdcpp.mutex.requirements.
+
+Require Import skylabs.brick.libstdcpp.pthread.pred.
+Require Import skylabs.brick.libstdcpp.pthread.spec.
+Require Import skylabs.brick.libstdcpp.pthread.hints.
+Require Import skylabs.brick.libstdcpp.cassert.spec.
+
+Require Import skylabs.brick.libstdcpp.test.pthread.test_cpp.
+
+Require Import skylabs.auto.cpp.prelude.proof.
+
+Section with_cpp.
+  Import auto.telescopes auto.telescopes.TeleNotations.
+
+  Context `{Σ : cpp_logic, σ : genv}.
+  Context {HAS_THREADS : HasStdThreads Σ}.
+  Context `{!test_cpp.source ⊧ σ}.
+
+  cpp.spec "thread_fn(void*)" as thread_fn_spec with
+      ( \arg{argp} "arg" (Vptr argp)
+        \pre{x}  argp |-> intR 1$m x
+        \post*   argp |-> intR 1$m (x + 1)
+        \require valid<"int"> (x + 1)
+        \post[Vptr nullptr] emp ).
+
+  cpp.spec "cancelable_thread(void*)" as cancelable_thread_spec with
+      ( \arg{argp} "arg" (Vptr argp)
+        \pre{x}       argp |-> intR 1$m x
+        \post*        argp |-> intR 1$m (x + 3)
+        \require      valid<"int"> (x + 3)  (* TODO: validP / valid should be interchageable *)
+        \post[Vptr nullptr] emp ).
+
+    cpp.spec "multithreaded_broken()" as multithreaded_broken_spec with
+      ( \post emp ).
+
+    cpp.spec "multithreaded_ok()" as multithreaded_ok_spec with
+      ( \post emp ).
+
+End with_cpp.
+
+Section with_cpp.
+  Import auto.telescopes auto.telescopes.TeleNotations.
+
+  Context `{Σ : cpp_logic, σ : genv}.
+  Context {HAS_THREADS : HasStdThreads Σ}.
+  Context `{Hmodule : !test_cpp.source ⊧ σ}.
+  Set Default Proof Using "Hmodule".
+
+  #[local] Arguments tele_app _ _ & _.
+  #[local] Hint Opaque tele_app : sl_opacity.
+
+  #[global] Instance thread_fn_is_thread :
+    ThreadFunction "thread_fn(void*)" thread_fn_spec
+      [tele (_ : Z)]
+      (fun p => tele_app (fun x => p |-> intR 1$m x ∗ [| valid<"int"> (x + 1) |]))%I
+      (fun p => tele_app (fun x _tid => p |-> intR 1$m (x + 1)))%I.
+  Proof. eapply specify_mono; work. Qed.
+
+  #[global] Instance cancelable_thread_fn_is_thread :
+    ThreadFunction "cancelable_thread(void* )" cancelable_thread_spec
+      [tele (_ : Z)]
+      (fun p => tele_app $ fun x => p |-> intR 1$m x ∗ [| valid<"int"> (x + 3) |] )%I
+      (fun p => tele_app $ fun x _retp => p |-> intR 1$m (x + 3))%I.
+  Proof. eapply specify_mono; work. Qed.
+
+  Lemma thread_fn_ok : verify[source] thread_fn_spec.
+  Proof.
+    verify_spec. go.
+  Qed.
+
+  Lemma multithreaded_broken_ok : verify[source] multithreaded_broken_spec.
+  Proof.
+    verify_spec. go.
+    wp_if.
+    { go. }
+    go.
+    (* fails here because thread owns local variable [counter] *)
+  Fail Qed.
+  Abort.
+
+  Lemma multithreaded_ok_ok : verify[source] multithreaded_ok_spec.
+  Proof.
+    verify_spec. go.
+      (* fork thread 1 *)
+    wp_if; go; [].
+      (* fork thread 2 *)
+    wp_if.
+    { go. }
+    go.
+  Qed.
+
+End with_cpp.