diff --git a/rocq-brick-libstdcpp/proof/atomic/inc_int.cpp b/rocq-brick-libstdcpp/proof/atomic/inc_int.cpp
new file mode 100644
index 00000000..fd52b45e
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/atomic/inc_int.cpp
@@ -0,0 +1,2 @@
+#include <atomic>
+template<> class std::atomic<int>;
diff --git a/rocq-brick-libstdcpp/proof/atomic/pred.v b/rocq-brick-libstdcpp/proof/atomic/pred.v
new file mode 100644
index 00000000..52e2a14a
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/atomic/pred.v
@@ -0,0 +1,57 @@
+(**
+ * Copyright (C) 2025 SkyLabs AI, Inc.
+ * All rights reserved.
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
+ *)
+Require Import skylabs.auto.cpp.spec.
+Require Import skylabs.cpp.spec.concepts.
+Require skylabs.brick.libstdcpp.atomic.inc_int_cpp.
+
+Require Import skylabs.cpp.spec.concepts.
+
+(** * Interface to Atomic<T> *)
+(**
+These specifications assume that all memory order parameters (template,
+function arguments) are _SEQ_CST. In the C++ code, redefine the other
+memory order macros to __ATOMIC_SEQ_CST.
+*)
+
+cpp.enum "std::memory_order" from (inc_int_cpp.source) variant.
+#[global] Abbreviation Tmemory_order := {%cpp_type[inc_int_cpp.source] "std::memory_order"} (only parsing).
+
+NES.Begin std.atomic.
+Module Type ATOMIC_PREDS.
+
+  (** Type [t] indexing our spec models the type name T in Atomic<T>. *)
+
+  (** The base class used by libstdc++ integral specializations (excluding bool).
+  Pointer, bool, and primary-template atomics have different layouts and are
+  not covered by these partial specs. *)
+  #[global] Abbreviation base_name ty :=
+    (Ninst "std::__atomic_base" [Atype ty]).
+  (** The type <<std::atomic<T>>> *)
+  #[global] Abbreviation class_name ty := (Ninst "std::atomic" [Atype ty]).
+  #[global] Abbreviation T ty := (Tnamed (class_name ty)).
+
+  (** Abstract predicates *)
+
+  (** Fraction [q] ownership of atomically accessible value [v]. *)
+  Parameter R : ∀ `{Σ : cpp_logic} {σ : genv} (ty : type) `{PV : @PrimVal ty A} (q : cQp.t) (x : A), Rep.
+
+  Section R_props.
+    Context `{Σ : cpp_logic} {σ : genv} `{PV : @PrimVal ty A}.
+    Abbreviation R := (R ty (PV:=PV)).
+
+    #[global] Declare Instance R_frac : CFractional1 R.
+    #[global] Declare Instance R_timeless : Timeless2 R.
+    #[global] Declare Instance R_frac_valid : CFracValid1 R.
+    #[global] Declare Instance R_agree : Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) R).
+    #[global] Declare Instance R_type : Typed2 (class_name ty) R.
+  End R_props.
+
+End ATOMIC_PREDS.
+
+Declare Module atomic : ATOMIC_PREDS.
+
+NES.End std.atomic.
diff --git a/rocq-brick-libstdcpp/proof/atomic/spec.v b/rocq-brick-libstdcpp/proof/atomic/spec.v
new file mode 100644
index 00000000..8d496c3e
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/atomic/spec.v
@@ -0,0 +1,381 @@
+(**
+ * Copyright (C) 2025 SkyLabs AI, Inc.
+ * All rights reserved.
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
+ *)
+Require Import skylabs.auto.cpp.spec.
+Require Import skylabs.cpp.spec.concepts.
+Require Import skylabs.brick.libstdcpp.atomic.inc_int_cpp.
+
+Require Import skylabs.cpp.spec.concepts.
+Require Export skylabs.brick.libstdcpp.atomic.pred.
+
+NES.Begin std.atomic.
+Module atomic_specs (Import atomic : ATOMIC_PREDS).
+
+  #[global] Hint Opaque R : sl_opacity.
+
+  Section spec.
+    Context `{Σ : cpp_logic} {σ : genv}.
+    Context (ty : type).
+    Context `{!PrimVal ty A,!DefaultValue ty A}.
+    Abbreviation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
+    Abbreviation b := (base_name ty) (only parsing).
+    Abbreviation R := (R ty).
+    Abbreviation bR q v := (_derived b s |-> R q%cQp v) (only parsing).
+
+    Definition default_ctor : mpred :=
+      specify.template.ctor s [] $
+        \this this
+        \post this |-> R 1$m (default_val ty).
+    #[global] Hint Opaque default_ctor : sl_opacity.
+    #[global] Arguments default_ctor : simpl never.
+    Definition SpecFor_default_ctor := RegisterSpec default_ctor.
+    #[global] Existing Instance SpecFor_default_ctor.
+
+    Definition ctor : mpred :=
+      specify.template.ctor s [ty] $
+        \this this
+        \arg{n} "v" (Vinj ty n)
+        \post this |-> R 1$m n.
+    #[global] Hint Opaque ctor : sl_opacity.
+    #[global] Arguments ctor : simpl never.
+    Definition SpecFor_ctor := RegisterSpec ctor.
+    #[global] Existing Instance SpecFor_ctor.
+
+    Definition dtor : mpred :=
+      specify.template.dtor s $
+        \this this
+        \pre{n} this |-> R 1$m n
+        \post emp.
+    #[global] Hint Opaque dtor : sl_opacity.
+    #[global] Arguments dtor : simpl never.
+    Definition SpecFor_dtor := RegisterSpec dtor.
+    #[global] Existing Instance SpecFor_dtor.
+
+    (** *** <<load>> & <<store>> *)
+    Definition do_load (this : ptr) (K : A -> mpred) : mpred :=
+      AR1 << ∃∃ n q, this |-> bR q n >> @ top, empty << K n >>.
+    #[global] Hint Opaque do_load : typeclass_instances sl_opacity.
+
+    Definition load : mpred :=
+      specify.template.method b "load" function_qualifiers.N ty [Tmemory_order] $
+        \this this
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{K} do_load this K
+        \post{n}[Vinj ty n] K n.
+    #[global] Hint Opaque load : sl_opacity.
+    #[global] Arguments load : simpl never.
+    Definition SpecFor_load := RegisterSpec load.
+    #[global] Existing Instance SpecFor_load.
+
+    Definition load_const : mpred :=
+      specify.template.method b "load" function_qualifiers.Nc ty [Tmemory_order] $
+        \this this
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{K} do_load this K
+        \post{n}[Vinj ty n] K n.
+    #[global] Hint Opaque load_const : sl_opacity.
+    #[global] Arguments load_const : simpl never.
+    Definition SpecFor_load_const := RegisterSpec load_const.
+    #[global] Existing Instance SpecFor_load_const.
+
+    Definition do_store (this : ptr) (n : A) (K : mpred) : mpred :=
+      AC1 << ∀ m, this |-> bR 1$m m >> @ top, empty
+          << this |-> bR 1$m n, COMM K >>.
+    #[global] Hint Opaque do_store : typeclass_instances sl_opacity.
+
+    Definition store : mpred :=
+      specify.template.method b "store" function_qualifiers.N Tvoid [ty; Tmemory_order] $
+        \this this
+        \arg{n} "v" (Vinj ty n)
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{K} do_store this n K
+        \post K.
+    #[global] Hint Opaque store : sl_opacity.
+    #[global] Arguments store : simpl never.
+    Definition SpecFor_store := RegisterSpec store.
+    #[global] Existing Instance SpecFor_store.
+
+    (** *** <<operator=>> *)
+    Definition assign : mpred :=
+      specify.template.op b OOEqual function_qualifiers.N ty [ty] $
+        \this this
+        \arg{n} "v" (Vinj ty n)
+        \pre{K} do_store this n K
+        \post[Vinj ty n] K.
+    #[global] Hint Opaque assign : sl_opacity.
+    #[global] Arguments assign : simpl never.
+    Definition SpecFor_assign := RegisterSpec assign.
+    #[global] Existing Instance SpecFor_assign.
+
+    (** *** <<operator ty>> *)
+    Definition cast : mpred :=
+      specify.template.conv b ty function_qualifiers.Nc $
+        \this this
+        \pre{K} do_load this K
+        \post{n}[Vinj ty n] K n.
+    #[global] Hint Opaque cast : sl_opacity.
+    #[global] Arguments cast : simpl never.
+    Definition SpecFor_cast := RegisterSpec cast.
+    #[global] Existing Instance SpecFor_cast.
+
+    (** *** <<exchange>> *)
+    Definition do_exchange (this : ptr) (n : A) (K : A -> mpred) : mpred :=
+      AU1 << ∀ m, this |-> bR 1$m m >> @ top, empty
+          <<      this |-> bR 1$m n, COMM K m >>.
+    #[global] Hint Opaque do_exchange : typeclass_instances sl_opacity.
+
+    Definition exchange : mpred :=
+      specify.template.method b "exchange" function_qualifiers.N ty
+          [ty; Tmemory_order] $
+        \this this
+        \arg{desired} "desired" (Vinj ty desired)
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{K} do_exchange this desired K
+        \post{m}[Vinj ty m] K m.
+    #[global] Hint Opaque exchange : sl_opacity.
+    #[global] Arguments exchange : simpl never.
+    Definition SpecFor_exchange := RegisterSpec exchange.
+    #[global] Existing Instance SpecFor_exchange.
+
+    (** *** <<compare_exchange_weak>> & <<compare_exchange_strong>> *)
+    Definition do_compare_exchange (weak : bool) (this expected_p : ptr) (expected desired : A)
+        (K : bool -> mpred) : mpred :=
+      AU1 << ∀ cur, this |-> bR 1$m cur >> @ top, empty
+        << ∃ success m',
+          [| if weak then (* lifting the test on [weak] is probably a bit easier to work with *)
+               (success = true /\ cur = expected /\ m' = desired) \/
+               (success = false /\ m' = cur)
+             else
+               (success = true /\ cur = expected /\ m' = desired) \/
+               (success = false /\ cur <> expected /\ m' = cur)
+          |] **
+          this |-> bR 1$m m',
+        COMM
+          expected_p |-> primR ty 1$m (Vinj ty cur) -*
+          K success
+        >>.
+    #[global] Hint Opaque do_compare_exchange : typeclass_instances sl_opacity.
+
+    (** NOTE: the difference between the following two specs is not immediately obvious. *)
+    Definition compare_exchange_strong : mpred :=
+      specify.template.method b "compare_exchange_strong" function_qualifiers.N "bool"
+          [Tref ty; ty; Tmemory_order; Tmemory_order] $
+        \this this
+        \arg{expected_p} "o" (Vref expected_p)
+        \arg{desired} "n" (Vinj ty desired)
+        \arg "mo_success" (memory_order.to_val memory_order.seq_cst)
+        \arg "mo_failure" (memory_order.to_val memory_order.seq_cst)
+        \pre{expected} expected_p |-> primR ty 1$m (Vinj ty expected)
+        \pre{K} do_compare_exchange false this expected_p expected desired K
+        \post{b}[Vbool b] K b.
+    #[global] Hint Opaque compare_exchange_strong : sl_opacity.
+    #[global] Arguments compare_exchange_strong : simpl never.
+    Definition SpecFor_compare_exchange_strong := RegisterSpec compare_exchange_strong.
+    #[global] Existing Instance SpecFor_compare_exchange_strong.
+
+    Definition compare_exchange_strong_1 : mpred :=
+      specify.template.method b "compare_exchange_strong" function_qualifiers.N "bool"
+        [Tref ty; ty; Tmemory_order] $
+        \this this
+        \arg{expected_p} "o" (Vref expected_p)
+        \arg{desired} "n" (Vinj ty desired)
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{expected} expected_p |-> primR ty 1$m (Vinj ty expected)
+        \pre{K} do_compare_exchange false this expected_p expected desired K
+        \post{b}[Vbool b] K b.
+    #[global] Hint Opaque compare_exchange_strong_1 : sl_opacity.
+    #[global] Arguments compare_exchange_strong_1 : simpl never.
+    Definition SpecFor_compare_exchange_strong_1 := RegisterSpec compare_exchange_strong_1.
+    #[global] Existing Instance SpecFor_compare_exchange_strong_1.
+
+    Definition compare_exchange_weak : mpred :=
+      specify.template.method b "compare_exchange_weak" function_qualifiers.N "bool"
+        [Tref ty; ty; Tmemory_order; Tmemory_order] $
+        \this this
+        \arg{expected_p} "o" (Vref expected_p)
+        \arg{desired} "n" (Vinj ty desired)
+        \arg "mo_success" (memory_order.to_val memory_order.seq_cst)
+        \arg "mo_failure" (memory_order.to_val memory_order.seq_cst)
+        \pre{expected} expected_p |-> primR ty 1$m (Vinj ty expected)
+        \pre{K} do_compare_exchange true this expected_p expected desired K
+        \post{b}[Vbool b] K b.
+    #[global] Hint Opaque compare_exchange_weak : sl_opacity.
+    #[global] Arguments compare_exchange_weak : simpl never.
+    Definition SpecFor_compare_exchange_weak := RegisterSpec compare_exchange_weak.
+    #[global] Existing Instance SpecFor_compare_exchange_weak.
+
+    Definition compare_exchange_weak_1 : mpred :=
+      specify.template.method b "compare_exchange_weak" function_qualifiers.N "bool"
+        [Tref ty; ty; Tmemory_order] $
+        \this this
+        \arg{expected_p} "o" (Vref expected_p)
+        \arg{desired} "n" (Vinj ty desired)
+        \arg "mo" (memory_order.to_val memory_order.seq_cst)
+        \pre{expected} expected_p |-> primR ty 1$m (Vinj ty expected)
+        \pre{K} do_compare_exchange true this expected_p expected desired K
+        \post{b}[Vbool b] K b.
+    #[global] Hint Opaque compare_exchange_weak_1 : sl_opacity.
+    #[global] Arguments compare_exchange_weak_1 : simpl never.
+    Definition SpecFor_compare_exchange_weak_1 := RegisterSpec compare_exchange_weak_1.
+    #[global] Existing Instance SpecFor_compare_exchange_weak_1.
+
+  End spec.
+
+  Section bundled_spec.
+    Context `{Σ : cpp_logic} {σ : genv}.
+    Context (ty : type).
+    Context `{!PrimVal ty A,!DefaultValue ty A}.
+
+    Definition specs :=
+      ctor ty **
+      default_ctor ty **
+      dtor ty **
+      load ty **
+      load_const ty **
+      store ty    **
+      assign ty   **
+      cast ty     **
+      exchange ty **
+      compare_exchange_strong ty **
+      compare_exchange_strong_1 ty **
+      compare_exchange_weak ty **
+      compare_exchange_weak_1 ty.
+  End bundled_spec.
+
+  Class UnOp (ty : type) (A : Type) (op_name : OverloadableOperator) :=
+  { atomic_un_op : A -> A
+  }.
+  #[global] Hint Mode UnOp ! - ! : typeclass_instances.
+
+  Class BinOp (ty1 ty2 : type) (A B : Type) (op_name : OverloadableOperator) (fun_name : ident) :=
+  { atomic_bin_op : A -> B -> A
+  }.
+  #[global] Hint Mode BinOp ! - ! - ! - : typeclass_instances.
+  #[global] Hint Mode BinOp ! - ! - - ! : typeclass_instances.
+
+  Section with_ty.
+    Context `{Σ : cpp_logic} {σ : genv}.
+    Context (ty : type).
+    Context `{PrimVal ty A}.
+
+    #[local] Abbreviation s := (class_name ty) (only parsing).	(** [Atomic<T>] *)
+    #[local] Abbreviation b := (base_name ty) (only parsing).
+    #[local] Abbreviation bR q v := (_derived b s |-> R ty q v) (only parsing).
+
+    (** Apply operation [op] to the atomic cell pointed by [this],
+    and return the old contents to continuation [K]. *)
+    Definition do_op (op : A -> A) (this : ptr) (K : A -> mpred) : mpred :=
+      AC1 << ∀ m, this |-> bR 1$m m >> @ top, empty
+          << this |-> bR 1$m (op m), COMM K m >>.
+    #[global] Hint Opaque do_op : typeclass_instances sl_opacity.
+
+    Section with_unop.
+      Context `{UO : !UnOp ty A op_name}.
+
+      (** Triple for unary operators that return the new value *)
+      Definition unop_fetch : mpred :=
+        specify.template.op b op_name function_qualifiers.N ty [] $
+          \this this
+          \pre{K} do_op (atomic_un_op (UnOp := UO)) this K
+          \post{m}[Vinj ty (atomic_un_op (UnOp := UO) m)] K m.
+
+      #[global] Hint Opaque unop_fetch : sl_opacity.
+      #[global] Arguments unop_fetch : simpl never.
+      Definition SpecFor_unop_fetch := RegisterSpec unop_fetch.
+      #[global] Existing Instance SpecFor_unop_fetch.
+
+      (** Triple for unary operators that return the old value *)
+      Definition fetch_unop : mpred :=
+        specify.template.op b op_name function_qualifiers.N ty [Tint] $
+          \this this
+          \arg{dummy} "dummy" (Vint dummy)
+          \pre{K} do_op (atomic_un_op (UnOp := UO)) this K
+          \post{m}[Vinj ty m] K m.
+
+      #[global] Hint Opaque fetch_unop : sl_opacity.
+      #[global] Arguments fetch_unop : simpl never.
+      Definition SpecFor_fetch_unop := RegisterSpec fetch_unop.
+      #[global] Existing Instance SpecFor_fetch_unop.
+    End with_unop.
+
+    Section with_binop.
+      Context `{BO : !BinOp ty tyM A B op_name fun_name}.
+      Context `{!PrimVal tyM B}.
+
+      (** Triple for binary operators that return the new value *)
+      Definition binop_fetch : mpred :=
+        specify.template.op b op_name function_qualifiers.N ty [tyM] $
+          \this this
+          \arg{n : B} "v" (Vinj tyM n)
+          \pre{K} do_op (flip (atomic_bin_op (BinOp := BO)) n) this K
+          \post{m}[Vinj ty (atomic_bin_op (BinOp := BO) m n)] K m.
+      #[global] Hint Opaque binop_fetch : sl_opacity.
+      #[global] Arguments binop_fetch : simpl never.
+      Definition SpecFor_binop_fetch := RegisterSpec binop_fetch.
+      #[global] Existing Instance SpecFor_binop_fetch.
+
+      (** Triple for methods that return the old value *)
+      Definition fetch_binop : mpred :=
+        specify.template.method b fun_name function_qualifiers.N ty [tyM; Tmemory_order] $
+          \this this
+          \arg{n : B} "v" (Vinj tyM n)
+          \arg "mo" (memory_order.to_val memory_order.seq_cst)
+          \pre{K} do_op (flip (atomic_bin_op (BinOp := BO)) n) this K
+          \post{m}[Vinj ty m] K m.
+      #[global] Hint Opaque fetch_binop : sl_opacity.
+      #[global] Arguments fetch_binop : simpl never.
+      Definition SpecFor_fetch_binop := RegisterSpec fetch_binop.
+      #[global] Existing Instance SpecFor_fetch_binop.
+    End with_binop.
+  End with_ty.
+
+  (* Overflow on atomic integers is _defined_ behavior; reuse [atomic_eval] as
+  functional model. *)
+  #[global] Instance num_plusplus {sz sgn} :
+    UnOp (Tnum sz sgn) Z OOPlusPlus :=
+  {| atomic_un_op := Reduce atomic_eval sz sgn Z.add 1 |}.
+
+  #[global] Instance num_minusminus {sz sgn} :
+    UnOp (Tnum sz sgn) Z OOMinusMinus :=
+  {| atomic_un_op := Reduce atomic_eval sz sgn Z.add (-1) |}.
+
+  #[global] Instance num_add {sz sgn} :
+    BinOp (Tnum sz sgn) (Tnum sz sgn) Z Z OOPlusEqual "fetch_add" :=
+  {| atomic_bin_op := Reduce atomic_eval sz sgn Z.add |}.
+  (* TODO character types? *)
+
+  (** TODO fix overflow handling. *)
+  #[global] Instance num_sub {sz sgn} :
+    BinOp (Tnum sz sgn) (Tnum sz sgn) Z Z OOMinusEqual "fetch_sub" :=
+  {| atomic_bin_op := Reduce atomic_eval sz sgn Z.sub |}.
+
+  #[global] Instance num_bor {sz sgn} :
+    BinOp (Tnum sz sgn) (Tnum sz sgn) Z Z OOPipeEqual "fetch_or" :=
+  {| atomic_bin_op := Reduce atomic_eval sz sgn Z.lor |}.
+
+  #[global] Instance num_band {sz sgn} :
+    BinOp (Tnum sz sgn) (Tnum sz sgn) Z Z OOAmpEqual "fetch_and" :=
+  {| atomic_bin_op := Reduce atomic_eval sz sgn Z.land |}.
+
+  #[global] Instance num_bxor {sz sgn} :
+    BinOp (Tnum sz sgn) (Tnum sz sgn) Z Z OOCaretEqual "fetch_xor" :=
+  {| atomic_bin_op := Reduce atomic_eval sz sgn Z.lxor |}.
+
+  (* TODO character types? *)
+
+
+  #[global] Instance ptr_add {σ : genv} {ty} :
+    BinOp (Tptr ty) Tptrdiff_t ptr Z OOPlusEqual "fetch_add" :=
+  {| atomic_bin_op (p : ptr) b := p .[ ty ! b ] |}.
+
+  #[global] Instance ptr_sub {σ : genv} {ty} :
+    BinOp (Tptr ty) Tptrdiff_t ptr Z OOMinusEqual "fetch_sub" :=
+  {| atomic_bin_op (p : ptr) b := p .[ ty ! -b ] |}.
+
+End atomic_specs.
+
+Include (atomic_specs atomic).
+NES.End std.atomic.
diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index 52ff904b..b173654d 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -23,6 +23,18 @@
   	 (with-stderr-to inc_array_cpp.v.stderr (run cpp2v -v %{input} -o inc_array_cpp.v --no-elaborate --templates=inc_array_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_array.cpp))
 )
+(subdir atomic
+ (rule
+  (targets inc_int_cpp.v.stderr inc_int_cpp.v inc_int_cpp_templates.v)
+  (alias test_ast)
+  (deps
+   (:input inc_int.cpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to inc_int_cpp.v.stderr (run cpp2v -v %{input} -o inc_int_cpp.v --no-elaborate --templates=inc_int_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc_int.cpp))
+)
 (subdir cassert
  (rule
   (targets inc_cassert_cpp.v.stderr inc_cassert_cpp.v inc_cassert_cpp_templates.v)
diff --git a/rocq-brick-libstdcpp/test/atomic/test.cpp b/rocq-brick-libstdcpp/test/atomic/test.cpp
new file mode 100644
index 00000000..3e40173b
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/atomic/test.cpp
@@ -0,0 +1,91 @@
+/**
+ * Copyright (C) 2025 BlueRock Security, Inc.
+ * All rights reserved.
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
+ */
+#include <atomic>
+#include <cassert>
+
+using namespace std;
+
+void
+test(bool b, const char* msg = nullptr) {
+    assert(b);
+}
+
+void
+TestDefaultConstructor() {
+    std::atomic<int> atomicInt;
+    test(atomicInt.load() == 0);
+}
+
+void
+TestParameterizedConstructor() {
+    int initialValue = 10;
+    std::atomic<int> atomicInt(initialValue);
+    test(atomicInt.load() == initialValue);
+}
+
+void
+TestLoad() {
+    std::atomic<int> atomicInt(42);
+    test(42 == atomicInt.load());
+    test(42 == atomicInt);
+}
+
+void
+TestStore() {
+    std::atomic<int> atomicInt;
+    atomicInt.store(25);
+    test(atomicInt.load() == 25);
+    test((atomicInt = 31) == 31);
+    test(atomicInt.load() == 31);
+}
+
+void
+TestCAS() {
+    std::atomic<int> atomicInt{57};
+    int var = 13;
+    atomicInt.compare_exchange_strong(var, 25);
+    test(var == 57);
+    test(atomicInt.load() == 57);
+    var = 57;
+    atomicInt.compare_exchange_strong(var, 25);
+    test(var == 57);
+    test(atomicInt.load() == 25);
+    test(25 == atomicInt.exchange(13));
+    test(atomicInt.load() == 13);
+}
+
+void
+TestArith() {
+    std::atomic<int> atomicInt{57};
+    assert(60 == (atomicInt += 3));
+    assert(60 == atomicInt.load());
+}
+
+void
+TestFetchAdd() {
+    std::atomic<int> atomicInt{10};
+    assert(10 == atomicInt.fetch_add(1));
+    assert(11 == atomicInt.load());
+    assert(11 == atomicInt.fetch_add(1));
+    assert(12 == atomicInt);
+    assert(12 == atomicInt++);
+    assert(13 == atomicInt);
+    assert(14 == ++atomicInt);
+    assert(19 == (atomicInt += 5));
+}
+
+int
+main() {
+    TestDefaultConstructor();
+    TestParameterizedConstructor();
+    TestLoad();
+    TestStore();
+    TestCAS();
+    TestArith();
+    TestFetchAdd();
+    return 0;
+}
diff --git a/rocq-brick-libstdcpp/test/atomic/test_cpp_proof.v b/rocq-brick-libstdcpp/test/atomic/test_cpp_proof.v
new file mode 100644
index 00000000..ab720078
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/atomic/test_cpp_proof.v
@@ -0,0 +1,216 @@
+(**
+ * Copyright (C) 2025 SkyLabs AI, Inc.
+ * All rights reserved.
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
+ *)
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.brick.libstdcpp.cassert.spec.
+Require Import skylabs.brick.libstdcpp.atomic.spec.
+Require Import skylabs.brick.libstdcpp.test.atomic.test_cpp.
+
+NES.Open std.atomic.
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Abbreviation GLOBALS q := (_global "std::memory_order_seq_cst" |-> primR "enum std::memory_order" q 5).
+
+  Section specs.
+    Context `{MOD : test_cpp.source ⊧ σ}.
+
+    cpp.spec "test(bool, const char*)" as test_spec with
+      (\arg "b" (Vbool true)
+       \arg{p} "" (Vptr p)
+       \post emp).
+
+    cpp.spec "TestDefaultConstructor()" as test_default_ctor with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestParameterizedConstructor()" as test_parameterized_ctor with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestLoad()" as test_load with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestStore()" as test_store with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestCAS()" as test_cas with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestArith()" as test_arith with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "TestFetchAdd()" as test_fetch_add with
+        (\prepost{q} GLOBALS q
+         \post emp).
+
+    cpp.spec "main()" as main with
+        (\prepost{q} GLOBALS q
+         \post[Vint 0] emp).
+
+    Definition specs :=
+      test_default_ctor **
+      test_parameterized_ctor **
+      test_load **
+      test_store **
+      test_cas **
+      test_arith **
+      test_fetch_add.
+    #[global] Hint Opaque specs : sl_opacity.
+
+  End specs.
+
+  #[local] Hint Resolve fractional.UNSAFE_read_prim_cancel : sl_opacity.
+
+  Abbreviation BASE p := (p ,, _base "std::atomic<int>" "std::__atomic_base<int>").
+
+  #[program]
+  Definition do_load_C (p : ptr) :=
+    \cancelx
+    \using denoteModule test_cpp.source
+    \consuming{q (n : Z)} p |-> atomic.R "int" q n
+    \proving{(K : Z -> mpred) (_ : IsExistential K)} do_load Tint (BASE p) K
+    \instantiate K := (fun x : Z => p |-> atomic.R "int" q n ** [| x = n |])
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (?? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /do_load.
+    iAcIntro. rewrite /commit_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work. iExists q. work.
+    iMod "Y". iModIntro.
+    work.
+  Qed.
+  #[program]
+  Definition do_store_C (p : ptr) :=
+    \cancelx
+    \using denoteModule test_cpp.source
+    \consuming{(n : Z)} p |-> atomic.R "int" 1$m n
+    \proving{K (_ : IsExistential K) v} do_store Tint (BASE p) v K
+    \instantiate K := (p |-> atomic.R "int" 1$m v)
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (??? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /do_load.
+    iAcIntro. rewrite /commit_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work.
+    iMod "Y". iModIntro.
+    work.
+  Qed.
+  (* TODO: this is not the most general hint *)
+  #[program]
+  Definition do_compare_exchange_C (p p' : ptr) old new :=
+    \cancelx
+    \using (denoteModule test_cpp.source : mpred)
+    \consuming{n} p |-> atomic.R "int" 1$m (n : Z)
+    \proving{K (_ : IsExistential K)}
+      do_compare_exchange "int" false (BASE p) p' old new K
+    \instantiate K := (fun res =>
+                         if bool_decide (n = old) then
+                           p |-> atomic.R "int" 1$m new **
+                           p' |-> primR "int" 1$m old ** [| res = true |]
+                         else
+                           p |-> atomic.R "int" 1$m n **
+                           p' |-> primR "int" 1$m n ** [| res = false |])
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (?? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /do_compare_exchange.
+    iAuIntro1. rewrite /atomic1_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work.
+    { iMod "Y". iModIntro. work. }
+    { iMod "Y"; iModIntro. work.
+      case_bool_decide.
+      { subst. lazymatch goal with H : _ \/ _ |- _ => destruct H end. intuition. work.
+        exfalso; tauto. }
+      { lazymatch goal with H : _ \/ _ |- _ => destruct H end; try by exfalso; tauto.
+        intuition; subst. work. } }
+  Qed.
+  #[program]
+  Definition do_exchange_C (p : ptr) new :=
+    \cancelx
+    \using denoteModule test_cpp.source
+    \consuming{n} p |-> atomic.R "int" 1$m n
+    \proving{K (_ : IsExistential K)}
+      do_exchange "int" (BASE p) new K
+    \instantiate K := (fun res => [| res = n |] **
+                         p |-> atomic.R "int" 1$m new)
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (?? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /do_compare_exchange.
+    iAuIntro1. rewrite /atomic1_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work.
+    { iMod "Y". iModIntro. work. }
+    { iMod "Y"; iModIntro. work. }
+  Qed.
+
+  #[program]
+  Definition do_op_C (p : ptr) (op : Z -> Z) :=
+    \cancelx
+    \using denoteModule test_cpp.source
+    \consuming{n} p |-> atomic.R "int" 1$m n
+    \proving{K (_ : IsExistential K)}
+      do_op "int" op (BASE p) K
+    \instantiate K := (fun res => [| res = n |] **
+                               p |-> atomic.R "int" 1$m (op n))
+    \end@{mpredI}.
+  Next Obligation.
+    intros. iIntros "[#M ?]" (?? ->).
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    rewrite /do_op.
+    iAcIntro. rewrite /commit_acc.
+    iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+    work.
+    iMod "Y"; iModIntro; work.
+  Qed.
+
+  Hint Resolve do_compare_exchange_C do_exchange_C : sl_opacity.
+  Hint Resolve do_load_C do_store_C : sl_opacity.
+  Hint Resolve do_op_C : sl_opacity.
+
+  Abbreviation OK spec :=
+    (verify?[test_cpp.source] spec) (only parsing).
+
+  Lemma fetch_add_ok : OK test_fetch_add.
+  Proof. verify_spec. go. Qed.
+
+  Lemma arith_ok : OK test_arith.
+  Proof. verify_spec. go. Qed.
+
+  Lemma cas_ok : OK test_cas.
+  Proof. verify_spec. go. Qed.
+
+  Lemma default_ctor_ok : OK test_default_ctor.
+  Proof. verify_spec; go. Qed.
+
+  Lemma param_ctor_ok : OK test_parameterized_ctor.
+  Proof. verify_spec; go. Qed.
+
+  Lemma load_ok : OK test_load.
+  Proof. verify_spec; go. Qed.
+
+  Lemma store_ok : OK test_store.
+  Proof. verify_spec; go. Qed.
+
+  Lemma main_ok : OK main.
+  Proof.
+    rewrite /specs.
+    verify_spec. go.
+  Qed.
+
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc
index c24b00d1..2b10ff55 100644
--- a/rocq-brick-libstdcpp/test/dune.inc
+++ b/rocq-brick-libstdcpp/test/dune.inc
@@ -11,6 +11,18 @@
   	 (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 atomic
+ (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 cctype
  (rule
   (targets test_cpp.v.stderr test_cpp.v)