diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index b1b57d5..4cc6fc5 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -26,6 +26,15 @@
   	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps test.cpp))
 )
+(subdir new
+ (rule
+  (targets inc_new_cpp.v.stderr inc_new_cpp.v)
+  (alias test_ast)
+  (deps (:input inc_new.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to inc_new_cpp.v.stderr (run cpp2v -v %{input} -o inc_new_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc_new.cpp))
+)
 (subdir semaphore
  (rule
   (targets inc_hpp.v.stderr inc_hpp.v)
diff --git a/rocq-brick-libstdcpp/proof/new/hints.v b/rocq-brick-libstdcpp/proof/new/hints.v
new file mode 100644
index 0000000..4ebef15
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/new/hints.v
@@ -0,0 +1,280 @@
+Require Import bluerock.auto.cpp.proof.
+Require Export bluerock.brick.libstdcpp.new.spec.
+
+#[only(lazy_unfold(global))] derive alloc.tokenR.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic} {σ : genv}.
+
+  (** ** Hints for proving [alloc.token] from [new_token.R].
+
+     - <<_using_>> hints rely on [size_of _ ty = Some ...] to already be provable, while non
+       <<using>> hints introduce this fact and have higher hint cost.
+       This fact is otherwise lost because it is expressed within [alloc.token].
+     - <<_0>> lemmas special case for non-array allocations which are common and ensure that
+       the allocation overhead at the C++ level is 0. (Allocation overhead of the allocator-level is
+       separately captured in [allocatedR].)
+   *)
+  #[program]
+  Definition token_prove_using_C (p : ptr) q storage_p overhead ty sz
+    (_ : size_of _ ty = Some sz) :=
+    \cancelx
+    \consuming p |-> new_token.R q (new_token.mk ty storage_p overhead)
+    \proving p |-> alloc.tokenR ty q
+    \through storage_p .[ Tbyte ! -overhead ] |-> allocatedR q (overhead + sz)
+    \end.
+  Next Obligation.
+    rewrite alloc.tokenR.unlock. work.
+  Qed.
+
+  #[program]
+  Definition token_prove_C (p : ptr) q storage_p overhead ty :=
+    \cancelx
+    \consuming p |-> new_token.R q (new_token.mk ty storage_p overhead)
+    \proving p |-> alloc.tokenR ty q
+    \deduce{sz} [| size_of _ ty = Some sz |]
+    \through storage_p .[ Tbyte ! -overhead ] |-> allocatedR q (overhead + sz)
+    \end.
+  Next Obligation.
+    intros; iIntros "X".
+    iDestruct (observe [| exists sz, size_of _ _ = _ |] with "X") as "%".
+    destruct H; simpl in *.
+    rewrite alloc.tokenR.unlock. iDestruct "X" as "?"; work.
+  Qed.
+
+  (* special cases for the above two hints when the overhead is 0 *)
+  #[program]
+  Definition token_prove_using_0_C (p : ptr) q storage_p ty sz
+    (_ : size_of _ ty = Some sz) :=
+    \cancelx
+    \consuming p |-> new_token.R q (new_token.mk ty storage_p 0)
+    \proving p |-> alloc.tokenR ty q
+    \through storage_p |-> allocatedR q sz
+    \end.
+  Next Obligation.
+    rewrite alloc.tokenR.unlock. work.
+    normalize_ptrs. iStopProof; f_equiv. f_equiv. lia.
+  Qed.
+
+  #[program]
+  Definition token_prove_0_C (p : ptr) q storage_p ty :=
+    \cancelx
+    \consuming p |-> new_token.R q (new_token.mk ty storage_p 0)
+    \proving p |-> alloc.tokenR ty q
+    \deduce{sz} [| size_of _ ty = Some sz |]
+    \through storage_p |-> allocatedR q sz
+    \end.
+  Next Obligation.
+    intros; iIntros "X".
+    iDestruct (observe [| exists sz, size_of _ _ = _ |] with "X") as "%".
+    destruct H; simpl in *.
+    rewrite alloc.tokenR.unlock. iDestruct "X" as "?"; work.
+    normalize_ptrs. iStopProof; f_equiv; f_equiv; lia.
+  Qed.
+
+
+  (** ** Hints for proving [new_token.R] *)
+  #[program]
+  Definition token_use_non_array_C (p : ptr) ty q (_ : TCEq (is_array_type ty) false) :=
+    \cancelx
+    \consuming p |-> alloc.tokenR (σ:=σ) ty q
+    \proving{(storage_p : ptr) overhead} p |-> new_token.R q (new_token.mk ty storage_p overhead)
+    \deduce{(storage_p' : ptr) sz} [| size_of _ ty = Some sz |]
+    \deduce storage_p' |-> allocatedR q sz
+    \through [| storage_p = storage_p' |]
+    \through [| overhead = 0 |]%N
+    \end.
+  Next Obligation.
+    intros.
+    rewrite alloc.tokenR.unlock.
+    iIntros "X"; iDestruct "X" as (????) "[X ?]".
+    iDestruct (observe [| overhead = 0%N |] with "X") as "%".
+    subst. normalize_ptrs.
+    iExists storage_p.
+    iDestruct "X" as "?".
+    work.
+  Qed.
+
+  #[program]
+  Definition token_use_array_C (p : ptr) ty q :=
+    \cancelx
+    \consuming p |-> alloc.tokenR (σ:=σ) ty q
+    \proving{(storage_p : ptr) overhead} p |-> new_token.R q (new_token.mk ty storage_p overhead)
+    \deduce{(storage_p' : ptr) (overhead' : N) sz} [| size_of _ ty = Some sz |]
+    \deduce storage_p' .[ Tbyte ! -overhead' ] |-> allocatedR q (overhead' + sz)
+    \through [| storage_p = storage_p' |]
+    \through [| overhead = overhead' |]%N
+    \end.
+  Next Obligation.
+    rewrite alloc.tokenR.unlock. work.
+    iExists storage_p.
+    work.
+    iExists overhead. work.
+  Qed.
+
+  #[global] Instance alloc_token_new_token_learnable ty q q' a b c :
+    Learnable (alloc.tokenR ty q) (new_token.R q' (new_token.mk a b c)) [ty = a].
+  Proof. solve_learnable. Qed.
+  #[global] Instance allocatedR_learn : Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) allocatedR).
+  Proof. solve_learnable. Qed.
+
+  #[global] Instance token_learn : Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) alloc.tokenR).
+  Proof. solve_learnable. Qed.
+
+  (** <<delete nullptr>> hints
+      The needs for hints at that AST level is sub-optimal, but something that requires
+      a bit more infrastructure to automate. Specifically, [wp_delete_null] reduces to
+      a conjunction which requires splitting the proof. However, this split can be
+      avoided if <<operator delete(nullptr, ...)>> is effectively a no-op (as its
+      specification says that it should be). A better phrasing of this might be a class
+      like [TrivialOnNull function_name] which would allow us to generalize these proofs.
+   *)
+  #[program]
+  Definition wp_delete_null_operator_delete_size_C module cls Q
+    (Hdelete : delete_operator.delete_for module "operator delete(void*, unsigned long)" cls =[Vm]=> Some ("operator delete(void*, unsigned long)"%cpp_name, delete_operator.mk None true false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete_size
+    \using denoteModule module
+    \proving wp_delete_null "operator delete(void*, unsigned long)" cls Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    rewrite /delete_operator.type_for/=.
+    iApply invoke.use_cptrR; eauto; eauto.
+    simpl.
+    go.
+  Qed.
+
+  #[program]
+  Definition wp_delete_null_operator_delete_C module cls Q
+    (Hdelete : delete_operator.delete_for module "operator delete(void* )" cls =[Vm]=> Some ("operator delete(void* )"%cpp_name, delete_operator.mk None false false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete
+    \using denoteModule module
+    \proving wp_delete_null "operator delete(void* )" cls Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    rewrite /delete_operator.type_for/=.
+    iApply invoke.use_cptrR; eauto; eauto.
+    simpl.
+    go.
+  Qed.
+
+  #[program]
+  Definition wp_delete_null_operator_delete_array_size_C module cls Q
+    (Hdelete : delete_operator.delete_for module "operator delete[](void*, unsigned long)" (Tincomplete_array cls) =[Vm]=> Some ("operator delete[](void*, unsigned long)"%cpp_name, delete_operator.mk None true false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete_array_size
+    \using denoteModule module
+    \proving wp_delete_null "operator delete[](void*, unsigned long)" (Tincomplete_array cls) Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    iApply invoke.use_cptrR; eauto; eauto.
+    simpl. go.
+  Qed.
+
+  #[program]
+  Definition wp_delete_null_operator_delete_array_C module cls Q
+    (Hdelete : delete_operator.delete_for module "operator delete[](void* )" (Tincomplete_array cls) =[Vm]=> Some ("operator delete[](void* )"%cpp_name, delete_operator.mk None false false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete_array
+    \using denoteModule module
+    \proving wp_delete_null "operator delete[](void* )" (Tincomplete_array cls) Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    iApply invoke.use_cptrR; eauto; eauto.
+    go.
+  Qed.
+
+  #[program]
+  Definition wp_delete_null_operator_delete_fixed_array_C module cls array_size Q
+    (Hdelete : delete_operator.delete_for module "operator delete[](void*, unsigned long)" (Tarray cls array_size) =[Vm]=> Some ("operator delete[](void*, unsigned long)"%cpp_name, delete_operator.mk None true false))
+    {sz} (Hsizeof : sizeof._size_of module cls =[Vm]=> Some sz)
+    :=
+    \cancelx
+    \using operator_delete_array_size
+    \using denoteModule module
+    \proving wp_delete_null "operator delete[](void*, unsigned long)" (Tarray cls array_size) Q
+    \through Q
+    \end.
+  Next Obligation.
+    intros * Hdel * Hsize.
+    rewrite wp_delete_null.unlock.
+    iIntros "[#? #M] ?".
+    iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+    inversion Hdel.
+    erewrite delete_operator.delete_for_submodule;
+      [ | eassumption
+      | apply genv_compat_submodule; eauto ].
+    work. inversion Hsize as [Hx]; clear Hsize.
+    rewrite wp_invoke_delete.unlock; simpl.
+    work.
+    iApply invoke.use_cptrR; eauto; eauto.
+    go.
+  Qed.
+
+End with_cpp.
+
+#[global] Hint Resolve wp_delete_null_operator_delete_size_C wp_delete_null_operator_delete_C : db_bluerock_wp.
+#[global] Hint Resolve wp_delete_null_operator_delete_array_C wp_delete_null_operator_delete_array_size_C
+ wp_delete_null_operator_delete_fixed_array_C : db_bluerock_wp.
+
+#[global] Hint Resolve token_prove_C token_prove_0_C | 100 : br_opacity.
+#[global] Hint Resolve token_prove_using_C token_prove_using_0_C | 99 : br_opacity.
+#[global] Hint Resolve token_use_non_array_C | 99 : br_opacity.
+#[global] Hint Resolve token_use_array_C | 100 : br_opacity.
diff --git a/rocq-brick-libstdcpp/proof/new/inc_new.cpp b/rocq-brick-libstdcpp/proof/new/inc_new.cpp
new file mode 100644
index 0000000..89d9ed9
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/new/inc_new.cpp
@@ -0,0 +1 @@
+#include <new>
diff --git a/rocq-brick-libstdcpp/proof/new/pred.v b/rocq-brick-libstdcpp/proof/new/pred.v
new file mode 100644
index 0000000..f18ce8a
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/new/pred.v
@@ -0,0 +1,87 @@
+Require Import iris.proofmode.tactics.
+Require Import bluerock.auto.cpp.prelude.pred.
+Require Import bluerock.auto.cpp.elpi.derive.bi.
+Require Import bluerock.brick.libstdcpp.new.inc_new_cpp.
+#[local] Set Primitive Projections.
+
+cpp.enum "std::align_val_t" from source alias.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, source ⊧ σ}.
+
+  (** The ownership of the allocator data structures.
+
+   This would include ownership such as free lists and allocator data structures.
+   In C++, these are generally ambient, so this is exposed as a predicate
+   rather than a representation predicate.
+
+   NOTE/TODO: The current interface exposes but does **not** use `allocatorP`,
+   because doing so would effectively require
+   threading this ownership everywhere which is not very ergonomic; however,
+   formally, this makes the interface un-realizable.
+
+   More investigation is needed to understand how to encapsulate this ownership
+   (and other ownership like it). The most promising option to date is to use
+   thread-local invariants, but this still introduces some level of verbosity.
+   *)
+  Parameter allocatorP : forall {σ : genv}, Qp -> mpred.
+  #[only(fractional,fracvalid)] derive allocatorP.
+
+  (** The allocation meta-data **owned by the allocator**.
+
+      In a normal implementation of <<malloc>>, this is a few bytes before the
+      returned pointer that stores meta data, e.g. the size of the allocation.
+
+      NOTE: While C++ often stores the size of the array next to a dynamically
+      allocated array, the memory that backs this is **not** part of [allocatedR].
+      That memory is owned by the C++ abstract machine.
+   *)
+  Parameter allocatedR : forall {σ : genv}, Qp -> N -> Rep.
+  #[only(fractional,asfractional,fracvalid,timeless)] derive allocatedR.
+  #[global] Instance: Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) allocatedR).
+  Proof. solve_learnable. Qed.
+
+End with_cpp.
+
+NES.Begin alloc.
+
+  (** [token ty sz q] bundles the dynamic allocation tokens provided by
+      the C++ abstract machine with the [allocatedR] fact from the allocation library.
+   *)
+  br.lock
+  Definition tokenR `{Σ : cpp_logic} {σ : genv} (ty : type) (q : Qp) : Rep :=
+    Exists storage_p overhead sz,
+      [| size_of _ ty = Some sz |] **
+      new_token.R q {| new_token.alloc_ty := ty ; new_token.storage_ptr := storage_p ; new_token.overhead := overhead |} **
+      pureR (storage_p .[ "unsigned char" ! -overhead ] |-> allocatedR q (overhead + sz)).
+  #[only(fractional,asfractional,fracvalid,timeless)] derive new_token.R.
+  #[only(fracvalid,timeless)] derive tokenR.
+
+  #[local] Open Scope string_scope. (* for IPM *)
+  #[global] Instance tokenR_xxx `{Σ : cpp_logic} {σ : genv} ty
+    : Fractional (tokenR ty).
+  Proof.
+    rewrite tokenR.unlock.
+    repeat first [ apply _
+                 | apply fractional_exist; intros ].
+    { apply observe_2_sep_l.
+      apply observe_2_only_provable_impl.
+      congruence. }
+    { apply observe_2_exist; intros.
+      apply observe_2_sep_r, observe_2_sep_l.
+      iIntros "A B".
+      iDestruct (observe_2 [| _ = _ |] with "A B") as "%".
+      inversion H; eauto. }
+    { do 2 (apply observe_2_exist; intros).
+      apply observe_2_sep_r, observe_2_sep_l.
+      iIntros "A B".
+      iDestruct (observe_2 [| _ = _ |] with "A B") as "%".
+      inversion H; eauto. }
+  Qed.
+  (* We should be able to derive this, but <<derive>> gets stuck trying to prove the above instance
+  #[only(asfractional)] derive tokenR.
+   *)
+
+   #[global] Instance tokenR_asfractional `{Σ : cpp_logic} {σ : genv} (ty : type) (q : Qp) : AsFractional (tokenR ty q) (tokenR ty) q.
+  Proof. solve_as_frac. Qed.
+NES.End alloc.
diff --git a/rocq-brick-libstdcpp/proof/new/spec.v b/rocq-brick-libstdcpp/proof/new/spec.v
new file mode 100644
index 0000000..2e8f818
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/new/spec.v
@@ -0,0 +1,85 @@
+Require Import bluerock.auto.cpp.prelude.spec.
+Require Export bluerock.brick.libstdcpp.new.pred.
+Require Import bluerock.brick.libstdcpp.new.inc_new_cpp.
+
+#[local] Set Primitive Projections.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, source ⊧ σ}.
+
+  cpp.spec "operator new(std::size_t, const std::nothrow_t&)" as operator_new_nothrow with
+    (\arg{sz}        "sz"      (Vn sz)
+     \arg{nothrow_p} "nothrow" (Vref nothrow_p)
+     \post{p}[Vptr p]
+        if bool_decide (p = nullptr) then emp
+        else p |-> (blockR sz 1$m **
+                    alignedR STDCPP_DEFAULT_NEW_ALIGNMENT **
+                    allocatedR 1 sz)).
+
+  (* Consult <<spec_exc.v>> for a specification of <<operator new(size_t)>>, the
+     "default" <<new>>.
+   *)
+
+  cpp.spec "operator delete(void*)" as operator_delete with
+      (\arg{p} "p" (Vptr p)
+       \pre if bool_decide (p = nullptr) then emp
+            else ∃ sz, p |-> (allocatedR 1 sz ** blockR sz 1$m)
+       \post emp).
+
+(*  #[ignore_missing] *)
+  cpp.spec "operator delete(void*, std::size_t, enum std::align_val_t)" as operator_delete_size_align with
+      (\arg{p} "p" (Vptr p)
+       \arg{sz} "sz" (Vn sz)
+       \arg{al} "al" (Vn al)
+       \pre if bool_decide (p = nullptr) then emp
+            else ∃ sz, p |-> (allocatedR 1 sz ** blockR sz 1$m ** alignedR al)
+       \post emp).
+
+(*  #[ignore_missing] *)
+  cpp.spec "operator delete(void*, std::size_t)" as operator_delete_size with
+      (\arg{p} "p" (Vptr p)
+       \arg{sz} "sz" (Vn sz)
+       \pre if bool_decide (p = nullptr) then emp
+            else p |-> (allocatedR 1 sz ** blockR sz 1$m)
+       \post emp).
+
+  (** ** Array <<new>> and <<delete>> *)
+  cpp.spec "operator new[](std::size_t, const std::nothrow_t&)" as operator_new_array_nothrow with
+      (\arg{sz} "sz" (Vn sz)
+       \arg{nothrow_p} "" (Vptr nothrow_p)
+       \post{p}[Vptr p]
+          if bool_decide (p = nullptr) then emp
+          else p |-> (blockR sz 1$m **
+                      alignedR STDCPP_DEFAULT_NEW_ALIGNMENT **
+                      allocatedR 1 sz)).
+
+  cpp.spec "operator delete[](void*)" as operator_delete_array with
+      (\arg{p} "p" (Vptr p)
+       \pre if bool_decide (p = nullptr) then emp
+            else ∃ sz, p |-> (allocatedR 1 sz ** blockR sz 1$m)
+       \post emp).
+
+  cpp.spec "operator delete[](void*, std::size_t)" as operator_delete_array_size with
+      (\arg{p} "p" (Vptr p)
+       \arg{sz} "sz" (Vn sz)
+       \pre  if bool_decide (p = nullptr) then emp
+             else p |-> (allocatedR 1 sz ** blockR sz 1$m)
+       \post emp).
+
+End with_cpp.
+
+NES.Begin alloc.
+
+  (* TODO: fix this *)
+  Notation interface := (operator_new_nothrow ** operator_delete ** valid_ptr (_global "nothrow")).
+NES.End alloc.
+
+#[global] Hint Extern 1000 (SpecFor "operator new(unsigned long)"%cpp_name _) =>
+   (idtac "<<operator new(size_t)>>'s specification requires exceptions."
+          "See [bluerock.brick.libstdcpp.new.spec_exc] for more information about it.";
+    exact (SpecFor.mk _ emp)) : typeclass_instances.
+
+#[global] Hint Extern 1000 (SpecFor "operator new[](unsigned long)"%cpp_name _) =>
+  (idtac "<<operator new[](size_t)>>'s specification requires exceptions."
+     "See [bluerock.brick.libstdcpp.new.spec_exc] for more information about it.";
+   exact (SpecFor.mk _ emp)) : typeclass_instances.
diff --git a/rocq-brick-libstdcpp/proof/new/spec_exc.v b/rocq-brick-libstdcpp/proof/new/spec_exc.v
new file mode 100644
index 0000000..ae195f2
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/new/spec_exc.v
@@ -0,0 +1,48 @@
+Require Import bluerock.auto.cpp.specs.
+
+Require Import bluerock.brick.libstdcpp.new.inc_new_cpp.
+Require Export bluerock.brick.libstdcpp.new.spec.
+
+Import cpp_notation.
+
+(** This file provides a specification of the default <<operator new(size_t)>>
+    provided by the C++ standard library. This function communicates allocation
+    failures using exceptions which BRiCk does not currently support.
+
+    A common way to make this specification sound is to modify the
+    implementation of <<operator new>> to abort on allocation, e.g. by calling
+    <<exit(1);>>. With this revision, the following [new_spec] is sound.
+
+    If you require the use of exceptions in your development,
+    please up-vote this feature request:
+    <<https://github.com/skylabsai/BRiCk/issues/15>>.
+ *)
+
+
+#[local] Set Primitive Projections.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, module ⊧ σ}.
+
+  (** <<operator new(size_t)>> is not allowed to return <<nullptr>>, it
+      signals failure by raising an exception.
+   *)
+  cpp.spec "operator new(std::size_t)" as new_spec with
+      (\arg{sz} "sz"      (Vn sz)
+       \post{p}[Vptr p] p |-> (blockR sz 1$m **
+                               nonnullR **
+                               alignedR STDCPP_DEFAULT_NEW_ALIGNMENT **
+                               allocatedR 1 sz)).
+
+  (** <<operator new[](size_t)>> is not allowed to return <<nullptr>>, it
+      signals failure by raising an exception.
+   *)
+  cpp.spec "operator new[](std::size_t)" as operator_new_array with
+      (\arg{sz} "sz" (Vn sz)
+       \post{p}[Vptr p]
+           p |-> (blockR sz 1$m **
+                  nonnullR **
+                  alignedR STDCPP_DEFAULT_NEW_ALIGNMENT **
+                  allocatedR 1 sz)).
+
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh b/rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh
new file mode 100755
index 0000000..a228dca
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh
@@ -0,0 +1,138 @@
+#!/bin/bash
+#
+# Copyright (C) 2020-2025 BlueRock Security, 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.
+#
+
+usage() {
+	cat >&2 <<-EOF
+		usage: $(basename "$0") [ -t ] <filename>.<ext> <cpp2v-options> -- [ <clang-options> ]
+
+		This will output (to stdout) dune rules for building <filename>.<ext>,
+		passing <options> to cpp2v. Redirect output to dune.inc and
+		load via dune's include.
+
+		The output is filesystem-independent and <filename>.<ext> need not exist.
+		Placing the output in <base>/dune.inc will transform
+		<base>/<filename>.<ext> into <base>/<filename>_<ext>.v and
+		<base>/<filename>_<ext>_names.v and (with \`-t\`)
+		<base>/<filename>_<ext>_templates.v.
+	EOF
+	exit 1
+}
+
+outRule() {
+	local indent fullName name ext
+	indent="$1"
+	fullName="$2"
+	shift 2
+
+	# The extension starts at the last dot:
+	name="${fullName%.*}"
+	if [ "$name" = "$fullName" ]; then
+		echo -e "Error: filename '$fullName' has no extension\n" >&2
+		usage
+	fi
+	ext="${fullName##*.}"
+
+	local module="${name}_${ext}.v"
+	local targ="${module}"
+	local clang_options=""
+	local universe=""
+	if [ "$system" = 1 ]; then
+		universe=" (universe)"
+	fi
+	local cpp2v="cpp2v -v %{input} -o ${module}"
+
+	if [ "$gen_names" = 1 ]; then
+		local names="${name}_${ext}_names.v"
+		targ="${targ} ${names}"
+		cpp2v="${cpp2v} -names ${names}"
+	fi
+
+	if [ "$templates" = 1 ]; then
+		local templates="${name}_${ext}_templates.v"
+		cpp2v="${cpp2v} --templates=${templates}"
+		targ="$targ ${templates}"
+	fi
+
+	action="(run ${cpp2v} ${1+ $@} ${clang_options})"
+
+	sed "s/^/${indent}/" <<-EOF
+		(rule
+		 (targets ${module}.stderr ${targ})
+		 (alias test_ast)
+		 (deps (:input ${name}.${ext}) (glob_files_rec ${prefix}*.hpp)${universe})
+		 (action
+		 	 (with-stderr-to ${module}.stderr ${action})))
+		(alias (name srcs) (deps ${name}.${ext}))
+	EOF
+	# TODO: maybe drop @srcs alias, seems leftover from !2613
+}
+
+traverse() {
+	local indent path firstDir rest
+	indent="$1"
+	path="$2"
+	shift 2
+	firstDir="${path%%/*}"
+	rest="${path#*/}"
+	if [ "$firstDir" = "$path" ]; then
+		outRule "$indent" "$path" "$@"
+	elif [ "$firstDir" = "." ]; then
+		traverse "$indent" "$rest" "$@"
+	else
+		#echo DIR $firstDir
+		#echo REST $rest
+		echo "${indent}(subdir ${firstDir}"
+		(cd "${firstDir}"; traverse " $indent" "$rest" "$@")
+		echo "${indent})"
+	fi
+}
+
+gen_names=0
+templates=0
+system=0
+prefix="../"
+while :
+do
+	case "$1" in
+	-n)
+		gen_names=1
+		shift
+		;;
+	-t)
+		templates=1
+		shift
+		;;
+	-s)
+		system=1
+		shift
+		;;
+	-p)
+		shift
+		prefix="$1"
+		shift
+		;;
+	--)
+		shift
+		break
+		;;
+	-*)
+		usage
+		;;
+	*)
+		break
+		;;
+	esac
+done
+[ $# -ge 1 ] || usage
+
+path="$1"
+shift
+
+traverse "" "$path" "$@"
+
+# vim:set noet sw=8:
diff --git a/rocq-brick-libstdcpp/test/dune b/rocq-brick-libstdcpp/test/dune
new file mode 100644
index 0000000..ff158d5
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/dune
@@ -0,0 +1,15 @@
+; Copyright © 2022-2025 BlueRock Security, Inc.
+;
+; This file is CONFIDENTIAL AND PROPRIETARY to BlueRock. All rights reserved.
+;
+; Use of this file is only permitted subject to a separate written license agreement with BlueRock.
+
+(include_subdirs qualified)
+(coq.theory
+ (name bluerock.brick.libstdcpp.test) ; logical path of this library
+ (theories
+  Lens Lens.Elpi Equations Equations.Prop Equations.Type
+  Stdlib
+  bluerock iris stdpp elpi elpi_elpi ExtLib Ltac2
+  bluerock.brick.libstdcpp))
+(include dune.inc)
diff --git a/rocq-brick-libstdcpp/test/dune-gen.sh b/rocq-brick-libstdcpp/test/dune-gen.sh
new file mode 100755
index 0000000..271d8c0
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/dune-gen.sh
@@ -0,0 +1,34 @@
+#!/bin/sh
+#
+# Copyright (C) 2020-2025 BlueRock Security, 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.
+#
+
+target=dune.inc
+
+usage() {
+	cat >&2 <<-EOF
+		usage: $(basename "$0")
+
+		This will invoke ./cpp2v-dune-gen.sh for every C or C++ file under
+		the current directory, sending the dune rules to ${target}.
+	EOF
+        exit 1
+}
+
+[ $# = 0 ] || usage
+
+exec > ${target}
+
+echo "; DO NOT EDIT: Generated by \"$0${1+ $*}\""
+
+# Temporary: `cpp2v --templates` for only those tests in ./templates.
+
+# Blacklist some files for arch_indep
+find . -name '*.[ch]pp' |
+sort |
+while read i; do
+  ./cpp2v-dune-gen.sh -s -- $i -- -std=c++20 -stdlib=libstdc++
+done
diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc
new file mode 100644
index 0000000..52a0031
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/dune.inc
@@ -0,0 +1,10 @@
+; DO NOT EDIT: Generated by "./dune-gen.sh"
+(subdir new
+ (rule
+  (targets demo_cpp.v.stderr demo_cpp.v)
+  (alias test_ast)
+  (deps (:input demo.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to demo_cpp.v.stderr (run cpp2v -v %{input} -o demo_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps demo.cpp))
+)
diff --git a/rocq-brick-libstdcpp/test/new/demo.cpp b/rocq-brick-libstdcpp/test/new/demo.cpp
new file mode 100644
index 0000000..c697d7e
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/new/demo.cpp
@@ -0,0 +1,30 @@
+#include <new>
+
+int* test_new() {
+  return new int{0};
+}
+
+void test_delete(int* p) {
+  delete p;
+}
+
+void test_new_delete() {
+  auto p = new int;
+  delete p;
+}
+
+int* test_new_array() {
+  auto p = new int[2];
+  p[0] = 1;
+  p[1] = 2;
+  return p;
+}
+
+void test_delete_array(int* p) {
+  delete[] p;
+}
+
+void test_new_delete_array() {
+  auto p = new int[2];
+  delete[] p;
+}
diff --git a/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v b/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v
new file mode 100644
index 0000000..bcb5fb9
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v
@@ -0,0 +1,84 @@
+Require Import bluerock.auto.cpp.prelude.proof.
+Require Import bluerock.brick.libstdcpp.new.pred.
+
+Require Import bluerock.brick.libstdcpp.new.spec_exc.
+Require Import bluerock.brick.libstdcpp.new.hints.
+Require bluerock.brick.libstdcpp.test.new.demo_cpp.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic} {σ : genv}.
+
+  Import linearity.
+
+  cpp.spec "test_new()" from demo_cpp.source with
+    (\post{p}[Vptr p]
+       p |-> (intR 1$m 0 ** alloc.tokenR "int" 1)).
+
+  Lemma test_new_ok : verify[demo_cpp.source] "test_new()".
+  Proof. verify_spec; go. Qed.
+
+  cpp.spec "test_delete(int* )" from demo_cpp.source with
+    (\arg{p} "p" (Vptr p)
+     \pre{v} p |-> (intR 1$m v ** alloc.tokenR "int" 1)
+     \post emp).
+
+  Lemma test_delete_ok : verify[demo_cpp.source] "test_delete(int* )".
+  Proof.
+    verify_spec.
+    go; case_bool_decide; go.
+  Qed.
+
+  cpp.spec "test_new_delete()" from demo_cpp.source with
+    (\post emp).
+
+  Lemma test_new_delete_ok : verify[demo_cpp.source] "test_new_delete()".
+  Proof. verify_spec; go. Qed.
+
+  cpp.spec "test_new_array()" from demo_cpp.source with
+    (\post{p}[Vptr p]
+      p |-> (arrayLR "int" 0 2 (fun z => intR 1$m z) [1; 2]%Z **
+      alloc.tokenR "int[2]" 1)
+    ).
+
+  cpp.spec "test_delete_array(int* )" from demo_cpp.source with
+    (\arg{p} "p" (Vptr p)
+     \pre p |-> (arrayLR "int" 0 2 (fun z => intR 1$m z) [1; 2]%Z **
+                 alloc.tokenR "int[2]" 1)
+     \post emp
+    ).
+
+  cpp.spec "test_new_delete_array()" from demo_cpp.source with
+    (\post emp).
+
+  Lemma test_delete_array_ok : verify[demo_cpp.source] "test_delete_array(int* )".
+  Proof.
+    verify_spec; go.
+    case_bool_decide; try by go.
+    go.
+    case_bool_decide.
+    { go. rewrite H. go. exfalso; lia. }
+    { go. }
+  Qed.
+
+  (** The C++ standard recommends <<262144 <= SIZE_MAX>>.  *)
+  Axiom Cpp_SIZE_MAX : (262144 <= SIZE_MAX)%N.
+
+  Lemma test_new_array_ok : verify[demo_cpp.source] "test_new_array()".
+  Proof.
+    verify_spec.
+    go.
+    { exfalso.
+      generalize Cpp_SIZE_MAX. lia. }
+    { normalize_ptrs.
+      rewrite Z.add_opp_diag_r. normalize_ptrs. go. }
+  Qed.
+
+  Lemma test_new_delete_array_ok : verify[demo_cpp.source] "test_new_delete_array()".
+  Proof.
+    verify_spec; go.
+    normalize_ptrs.
+    rewrite Z.add_opp_diag_r. normalize_ptrs.
+    go.
+  Qed.
+
+End with_cpp.