diff --git a/bench/bench_bounded_stack.ml b/bench/bench_bounded_stack.ml
new file mode 100644
index 00000000..2dc2b495
--- /dev/null
+++ b/bench/bench_bounded_stack.ml
@@ -0,0 +1,74 @@
+open Multicore_bench
+module Stack = Saturn.Bounded_stack
+
+let run_one_domain ~budgetf ?(n_msgs = 50 * Util.iter_factor) () =
+  let t = Stack.create () in
+
+  let op push =
+    if push then Stack.try_push t 101 |> ignore else Stack.pop_opt t |> ignore
+  in
+
+  let init _ =
+    assert (Stack.is_empty t);
+    Util.generate_push_and_pop_sequence n_msgs
+  in
+  let work _ bits = Util.Bits.iter op bits in
+
+  Times.record ~budgetf ~n_domains:1 ~init ~work ()
+  |> Times.to_thruput_metrics ~n:n_msgs ~singular:"message" ~config:"one domain"
+
+let run_one ~budgetf ?(n_adders = 2) ?(n_takers = 2)
+    ?(n_msgs = 50 * Util.iter_factor) () =
+  let n_domains = n_adders + n_takers in
+
+  let t = Stack.create () in
+
+  let n_msgs_to_take = Atomic.make 0 |> Multicore_magic.copy_as_padded in
+  let n_msgs_to_add = Atomic.make 0 |> Multicore_magic.copy_as_padded in
+
+  let init _ =
+    assert (Stack.is_empty t);
+    Atomic.set n_msgs_to_take n_msgs;
+    Atomic.set n_msgs_to_add n_msgs
+  in
+  let work i () =
+    if i < n_adders then
+      let rec work () =
+        let n = Util.alloc n_msgs_to_add in
+        if 0 < n then begin
+          for i = 1 to n do
+            Stack.try_push t i |> ignore
+          done;
+          work ()
+        end
+      in
+      work ()
+    else
+      let rec work () =
+        let n = Util.alloc n_msgs_to_take in
+        if n <> 0 then begin
+          for _ = 1 to n do
+            while Option.is_none (Stack.pop_opt t) do
+              Domain.cpu_relax ()
+            done
+          done;
+          work ()
+        end
+      in
+      work ()
+  in
+
+  let config =
+    let format role n =
+      Printf.sprintf "%d %s%s" n role (if n = 1 then "" else "s")
+    in
+    Printf.sprintf "%s, %s" (format "adder" n_adders) (format "taker" n_takers)
+  in
+  Times.record ~budgetf ~n_domains ~init ~work ()
+  |> Times.to_thruput_metrics ~n:n_msgs ~singular:"message" ~config
+
+let run_suite ~budgetf =
+  run_one_domain ~budgetf ()
+  @ (Util.cross [ 1; 2 ] [ 1; 2 ]
+    |> List.concat_map @@ fun (n_adders, n_takers) ->
+       run_one ~budgetf ~n_adders ~n_takers ())
diff --git a/bench/main.ml b/bench/main.ml
index 24870c77..1c9fefb8 100644
--- a/bench/main.ml
+++ b/bench/main.ml
@@ -7,6 +7,7 @@ let benchmarks =
     ("Saturn Htbl", Bench_htbl.run_suite);
     ("Saturn Stack", Bench_stack.run_suite);
     ("Saturn Work_stealing_deque", Bench_ws_deque.run_suite);
+    ("Saturn Bounded_Stack", Bench_bounded_stack.run_suite);
   ]
 
 let () = Multicore_bench.Cmd.run ~benchmarks ()
diff --git a/dune-project b/dune-project
index 2eceb755..9fe76bba 100644
--- a/dune-project
+++ b/dune-project
@@ -9,7 +9,6 @@
 (documentation "https://ocaml-multicore.github.io/saturn/")
 (using mdx 0.4)
 
-
 (package
  (name saturn)
  (synopsis "Collection of concurent-safe data structures for Multicore OCaml")
diff --git a/src/bounded_stack.ml b/src/bounded_stack.ml
new file mode 100644
index 00000000..0e0f5e26
--- /dev/null
+++ b/src/bounded_stack.ml
@@ -0,0 +1,117 @@
+type 'a t = { head : (int * 'a list) Atomic.t; capacity : int }
+
+(* *)
+let create ?(capacity = Int.max_int) () =
+  let head = Atomic.make_contended (0, []) in
+  { head; capacity = max capacity 1 }
+
+let length t = fst (Atomic.get t.head)
+let is_full t = t.capacity = length t
+let is_empty t = Atomic.get t.head = (0, [])
+
+exception Empty
+exception Full
+
+let of_list ?(capacity = Int.max_int) list =
+  if capacity < List.length list then raise Full
+  else
+    let head = Atomic.make_contended (List.length list, List.rev list) in
+    { head; capacity } |> Multicore_magic.copy_as_padded
+
+let of_seq ?(capacity = Int.max_int) seq =
+  if capacity < Seq.length seq then raise Full
+  else
+    let list = List.of_seq seq in
+    let head = Atomic.make_contended (List.length list, List.rev list) in
+    { head; capacity } |> Multicore_magic.copy_as_padded
+
+(* *)
+
+type ('a, _) poly1 = Option : ('a, 'a option) poly1 | Value : ('a, 'a) poly1
+
+let peek_as : type a r. a t -> (a, r) poly1 -> r =
+ fun t poly ->
+  match Atomic.get t.head with
+  | _, [] -> begin match poly with Option -> None | Value -> raise Empty end
+  | _, value :: _ -> ( match poly with Option -> Some value | Value -> value)
+
+let peek_exn t = peek_as t Value
+let peek_opt t = peek_as t Option
+
+type ('a, _) poly2 =
+  | Option : ('a, 'a option) poly2
+  | Value : ('a, 'a) poly2
+  | Unit : ('a, unit) poly2
+
+(* *)
+let rec pop_as : type a r. a t -> Backoff.t -> (a, r) poly2 -> r =
+ fun t backoff poly ->
+  match Atomic.get t.head with
+  | _, [] -> begin
+      match poly with
+      | Option -> None
+      | Value -> raise Empty
+      | Unit -> raise Empty
+    end
+  | (len, hd :: tl) as old_head ->
+      if Atomic.compare_and_set t.head old_head (len - 1, tl) then
+        match poly with Option -> Some hd | Value -> hd | Unit -> ()
+      else pop_as t (Backoff.once backoff) poly
+
+let pop_exn t = pop_as t Backoff.default Value
+let pop_opt t = pop_as t Backoff.default Option
+let drop_exn t = pop_as t Backoff.default Unit
+
+let rec pop_all t backoff =
+  match Atomic.get t.head with
+  | _, [] -> []
+  | (_, values) as old_head ->
+      if Atomic.compare_and_set t.head old_head (0, []) then values
+      else pop_all t (Backoff.once backoff)
+
+let pop_all t = pop_all t Backoff.default
+
+let to_seq t =
+  match Atomic.get t.head with
+  | _, [] -> Seq.empty
+  | _, values -> List.to_seq values
+(* *)
+
+type _ mono = Unit : unit mono | Bool : bool mono
+
+let rec push_as : type r. 'a t -> Backoff.t -> 'a -> r mono -> r =
+ fun t backoff value mono ->
+  let ((len, values) as before) = Atomic.get t.head in
+  if len >= t.capacity then match mono with Bool -> false | Unit -> raise Full
+  else
+    let after = (len + 1, value :: values) in
+
+    if Atomic.compare_and_set t.head before after then
+      match mono with Bool -> true | Unit -> ()
+    else push_as t (Backoff.once backoff) value mono
+
+let push_exn t value = push_as t Backoff.default value Unit
+let try_push t value = push_as t Backoff.default value Bool
+
+let rec push_all_as : type r. 'a t -> Backoff.t -> 'a list -> r mono -> r =
+ fun t backoff values mono ->
+  let len = List.length values in
+  if len = 0 then match mono with Unit -> () | Bool -> true
+  else if len > t.capacity then
+    match mono with Unit -> raise Full | Bool -> false
+  else
+    let ((curr_len, prev_values) as before) = Atomic.get t.head in
+    if curr_len + len > t.capacity then
+      match mono with Bool -> false | Unit -> raise Full
+    else
+      let after =
+        (curr_len + len, List.rev_append (List.rev values) prev_values)
+      in
+      if Atomic.compare_and_set t.head before after then
+        match mono with Bool -> true | Unit -> ()
+      else push_all_as t (Backoff.once backoff) values mono
+
+let try_push_all t values = push_all_as t Backoff.default (List.rev values) Bool
+let push_all_exn t values = push_all_as t Backoff.default (List.rev values) Unit
+let add_seq_exn t seq = push_all_as t Backoff.default (List.of_seq seq) Unit
+let try_add_seq t seq = push_all_as t Backoff.default (List.of_seq seq) Bool
diff --git a/src/bounded_stack.mli b/src/bounded_stack.mli
new file mode 100644
index 00000000..5b79d3db
--- /dev/null
+++ b/src/bounded_stack.mli
@@ -0,0 +1,198 @@
+(** Lock-free bounded stack. 
+
+  This module implements a lock-free bounded stack based on Treiber's stack 
+  algorithm. Adding a capacity to this algorithm adds a general overhead to the
+   operations, and thus, it is recommended to use the unbounded stack 
+   {!Saturn.Stack} if neither the capacity nor the {!length} function 
+    is needed.
+*)
+
+(** {1 API} *)
+
+type 'a t
+(** Represents a lock-free bounded stack holding elements of type ['a]. *)
+
+val create : ?capacity:int -> unit -> 'a t
+(** [create ~capacity ()] creates a new empty bounded stack with a maximum 
+capacity of [capacity]. The default [capacity] value is [Int.max_int].
+*)
+
+val of_list : ?capacity:int -> 'a list -> 'a t
+(** [of_list list] creates a new Treiber stack from a list.
+
+  @raises Full if the [list] is longer than the capacity of the stack.
+*)
+
+val length : 'a t -> int
+(** [length stack] returns the number of elements currently in the [stack]. *)
+
+val is_empty : 'a t -> bool
+(** [is_empty stack] returns [true] if the [stack] is empty, otherwise [false]. *)
+
+val is_full : 'a t -> bool
+(** [is_full stack] returns [true] if the [stack] has reached capacity, 
+  otherwise [false]. *)
+
+(** {2 Consumer functions} *)
+
+exception Empty
+(** Raised when {!pop_exn}, {!peek_exn}, or {!drop_exn} is applied to an empty
+ stack. *)
+
+val peek_exn : 'a t -> 'a
+(** [peek_exn stack] returns the top element of the [stack] without removing it.
+    
+  @raises Empty if the [stack] is empty. *)
+
+val peek_opt : 'a t -> 'a option
+(** [peek_opt stack] returns [Some] of the top element of the [stack] without
+    removing it, or [None] if the [stack] is empty. *)
+
+val pop_exn : 'a t -> 'a
+(** [pop_exn stack] removes and returns the top element of the [stack].
+ 
+  @raises Empty if the [stack] is empty. *)
+
+val pop_opt : 'a t -> 'a option
+(** [pop_opt stack] removes and returns [Some] of the top element of the [stack],
+    or [None] if the [stack] is empty. *)
+
+val drop_exn : 'a t -> unit
+(** [drop_exn stack] removes the top element of the [stack]. 
+
+  @raises Empty if the [stack] is empty. *)
+
+val pop_all : 'a t -> 'a list
+(** [pop_all stack] removes and returns all elements of the [stack] in LIFO 
+order. 
+
+  {[
+    # open Saturn.Bounded_stack
+    # let t : int t = create ()
+    val t : int t = <abstr>
+    # try_push t 1
+    - : bool = true
+    # try_push t 2
+    - : bool = true
+    # try_push t 3
+    - : bool = true
+    # pop_all t
+    - : int list = [3; 2; 1]
+  ]}
+*)
+
+(** {2 Producer functions} *)
+
+exception Full
+(** Raised when {!push_exn} or {!push_all_exn} is applied to a full stack. *)
+
+val push_exn : 'a t -> 'a -> unit
+(** [push_exn stack element] adds [element] to the top of the [stack].
+    
+  @raises Full if the [stack] is full. *)
+
+val try_push : 'a t -> 'a -> bool
+(** [try_push stack element] tries to add [element] to the top of the [stack].
+    Returns [true] if the element was successfully added, or [false] if the
+    stack is full. *)
+
+val push_all_exn : 'a t -> 'a list -> unit
+(** [push_all_exn stack elements] adds all [elements] to the top of the [stack].
+    
+  @raises Full if the [stack] is full. *)
+
+val try_push_all : 'a t -> 'a list -> bool
+(** [try_push_all stack elements] tries to add all [elements] to the top of the 
+    [stack]. Returns [true] if the elements were successfully added, or [false] if 
+    the stack is full. 
+    
+  {[
+    # let t : int t = create ()
+    val t : int t = <abstr>
+    # try_push_all t [1; 2; 3; 4]
+    - : bool = true
+    # pop_opt t
+    - : int option = Some 4
+    # pop_opt t 
+    - : int option = Some 3
+    # pop_all t
+    - : int list = [2; 1]
+  ]}
+    *)
+
+(** {2 With Sequences }*)
+val to_seq : 'a t -> 'a Seq.t
+(** [to_seq stack] takes a snapshot of [stack] and returns its value from top to 
+bottom.
+
+  🐌 This is a linear time operation. *)
+
+val of_seq : ?capacity:int -> 'a Seq.t -> 'a t
+(** [of_seq seq] creates a stack from a [seq]. It must be finite. 
+
+  @raises Full if the [list] is longer than the capacity of the stack.
+*)
+
+val add_seq_exn : 'a t -> 'a Seq.t -> unit
+(** [add_seq_exn stack seq] adds all elements of [seq] to the top of the 
+[stack]. [seq] must be finite. 
+
+@raises Full if the [seq] is too long to fit in the stack. *)
+
+val try_add_seq : 'a t -> 'a Seq.t -> bool
+(** [try_add_seq stack seq] tries to add all elements of [seq] to the top of the
+[stack]. Returns [true] if the elements were successfully added, or [false] if 
+the [seq] is too long to fit in the stack.  *)
+
+(** {1 Examples}
+    An example top-level session:
+    {[
+      # open Saturn.Bounded_stack
+      # let t : int t = create ()
+      val t : int t = <abstr>
+      # try_push t 42
+      - : bool = true
+      # push_exn t 1
+      - : unit = ()
+      # pop_exn t
+      - : int = 1
+      # peek_opt t
+      - : int option = Some 42
+      # pop_opt t
+      - : int option = Some 42
+      # pop_opt t
+      - : int option = None
+      # pop_exn t
+      Exception: Saturn__Bounded_stack.Empty.]}
+
+    A multicore example: 
+    {@ocaml non-deterministic[
+      # open Saturn.Bounded_stack
+      # let t :int t = create ()
+      val t : int t = <abstr>
+      # let barrier =  Atomic.make 2
+      val barrier : int Atomic.t = <abstr>
+      # let pusher () = 
+        Atomic.decr barrier;
+        while Atomic.get barrier != 0 do Domain.cpu_relax () done;
+
+        try_push_all t [1;2;3] |> ignore;
+        push_exn t 42;
+        push_exn t 12
+      val pusher : unit -> unit = <fun>
+      # let popper () = 
+        Atomic.decr barrier;
+        while Atomic.get barrier != 0 do Domain.cpu_relax () done;
+        List.init 6 (fun i -> Domain.cpu_relax (); pop_opt t)
+      val popper : unit -> int option list = <fun>
+      # let domain_pusher = Domain.spawn pusher
+      val domain_pusher : unit Domain.t = <abstr>
+      # let domain_popper = Domain.spawn popper
+      val domain_popper : int option list Domain.t = <abstr>
+      # Domain.join domain_pusher
+      - : unit = ()
+      # Domain.join domain_popper
+      - : int option list = [Some 42; Some 3; Some 2; Some 1; None; Some 12]
+      ]}
+ 
+    *)
diff --git a/src/dune b/src/dune
index 739869ca..edec87ee 100644
--- a/src/dune
+++ b/src/dune
@@ -23,6 +23,12 @@ let () =
  (action
   (copy domain.ocaml4.ml domain.ml)))
 
+(rule
+ (enabled_if
+  (< %{ocaml_version} 4.14.0))
+ (action
+  (copy seq.ocaml4.13.ml seq.ml)))
+
 (rule
  (enabled_if
   (< %{ocaml_version} 5.2.0))
@@ -36,5 +42,5 @@ let () =
    (<> %{os_type} Win32)
    (>= %{ocaml_version} 5.0.0)))
  (libraries saturn)
- (files treiber_stack.mli))
+ (files treiber_stack.mli bounded_stack.mli))
 |}
diff --git a/src/saturn.ml b/src/saturn.ml
index eff05f9d..7da90e4d 100644
--- a/src/saturn.ml
+++ b/src/saturn.ml
@@ -29,6 +29,7 @@ Copyright (c) 2017, Nicolas ASSOUAD <nicolas.assouad@ens.fr>
 module Queue = Michael_scott_queue
 module Queue_unsafe = Michael_scott_queue_unsafe
 module Stack = Treiber_stack
+module Bounded_stack = Bounded_stack
 module Work_stealing_deque = Ws_deque
 module Single_prod_single_cons_queue = Spsc_queue
 module Single_prod_single_cons_queue_unsafe = Spsc_queue_unsafe
diff --git a/src/saturn.mli b/src/saturn.mli
index eac1789b..52f9f821 100644
--- a/src/saturn.mli
+++ b/src/saturn.mli
@@ -33,6 +33,7 @@ Copyright (c) 2017, Nicolas ASSOUAD <nicolas.assouad@ens.fr>
 module Queue = Michael_scott_queue
 module Queue_unsafe = Michael_scott_queue_unsafe
 module Stack = Treiber_stack
+module Bounded_stack = Bounded_stack
 module Work_stealing_deque = Ws_deque
 module Single_prod_single_cons_queue = Spsc_queue
 module Single_prod_single_cons_queue_unsafe = Spsc_queue_unsafe
diff --git a/src/seq.ocaml4.13.ml b/src/seq.ocaml4.13.ml
new file mode 100644
index 00000000..1d29d539
--- /dev/null
+++ b/src/seq.ocaml4.13.ml
@@ -0,0 +1,6 @@
+include Stdlib.Seq
+
+let rec length_aux accu xs =
+  match xs () with Nil -> accu | Cons (_, xs) -> length_aux (accu + 1) xs
+
+let[@inline] length xs = length_aux 0 xs
diff --git a/test/bounded_stack/bounded_stack_dscheck.ml b/test/bounded_stack/bounded_stack_dscheck.ml
new file mode 100644
index 00000000..06c7dfb4
--- /dev/null
+++ b/test/bounded_stack/bounded_stack_dscheck.ml
@@ -0,0 +1,317 @@
+module Stack = Bounded_stack
+
+let drain stack = Stack.pop_all stack |> List.length
+
+let push_pop () =
+  Atomic.trace (fun () ->
+      let stack = Stack.create () in
+      let items_total = 4 in
+
+      (* producer *)
+      Atomic.spawn (fun () ->
+          for i = 1 to items_total do
+            Stack.try_push stack i |> ignore
+          done);
+
+      (* consumer *)
+      let popped = ref [] in
+      Atomic.spawn (fun () ->
+          for _ = 1 to items_total do
+            match Stack.pop_opt stack with
+            | None -> ()
+            | Some v -> popped := v :: !popped
+          done);
+
+      (* checks*)
+      Atomic.final (fun () ->
+          Atomic.check (fun () ->
+              let remaining = Stack.pop_all stack in
+              let pushed = List.init items_total (fun x -> x + 1) in
+              List.sort Int.compare (!popped @ remaining) = pushed)))
+
+let push_drop () =
+  Atomic.trace (fun () ->
+      let stack = Stack.create () in
+      let items_total = 4 in
+
+      (* producer *)
+      Atomic.spawn (fun () ->
+          for i = 1 to items_total do
+            Stack.try_push stack i |> ignore
+          done);
+
+      (* consumer *)
+      let dropped = ref 0 in
+      Atomic.spawn (fun () ->
+          for _ = 1 to items_total do
+            match Stack.drop_exn stack with
+            | () -> dropped := !dropped + 1
+            | exception Stack.Empty -> ()
+          done);
+
+      (* checks*)
+      Atomic.final (fun () ->
+          Atomic.check (fun () ->
+              let remaining = drain stack in
+              !dropped + remaining = items_total)))
+
+let push_pop_with_capacity () =
+  Atomic.trace (fun () ->
+      let stack = Stack.create ~capacity:2 () in
+      let items_total = 4 in
+
+      (* producer *)
+      let pushed = Array.make items_total false in
+      Atomic.spawn (fun () ->
+          Array.iteri (fun i _ -> pushed.(i) <- Stack.try_push stack i) pushed);
+
+      (* consumer *)
+      let popped = Array.make items_total None in
+      Atomic.spawn (fun () ->
+          Array.iteri (fun i _ -> popped.(i) <- Stack.pop_opt stack) popped);
+      (* checks*)
+      Atomic.final (fun () ->
+          let popped = Array.to_list popped |> List.filter_map Fun.id in
+          let remaining = Stack.pop_all stack in
+          Atomic.check (fun () ->
+              let xor a b = (a && not b) || ((not a) && b) in
+              try
+                Array.iteri
+                  (fun i elt ->
+                    if elt then begin
+                      if not @@ xor (List.mem i remaining) (List.mem i popped)
+                      then raise Exit
+                    end
+                    else if List.mem i remaining || List.mem i popped then
+                      raise Exit)
+                  pushed;
+                true
+              with _ -> false)))
+
+let push_push () =
+  Atomic.trace (fun () ->
+      let stack = Stack.create () in
+      let items_total = 6 in
+
+      (* two producers *)
+      for i = 0 to 1 do
+        Atomic.spawn (fun () ->
+            for j = 1 to items_total / 2 do
+              (* even nums belong to thr 1, odd nums to thr 2 *)
+              Stack.try_push stack (i + (j * 2)) |> ignore
+            done)
+      done;
+
+      (* checks*)
+      Atomic.final (fun () ->
+          let items = Stack.pop_all stack in
+
+          (* got the same number of items out as in *)
+          Atomic.check (fun () -> items_total = List.length items);
+
+          (* they are in lifo order *)
+          let odd, even = List.partition (fun v -> v mod 2 == 0) items in
+
+          Atomic.check (fun () -> List.sort Int.compare odd = List.rev odd);
+          Atomic.check (fun () -> List.sort Int.compare even = List.rev even)))
+
+let push_push_with_capacity () =
+  Atomic.trace (fun () ->
+      let capacity = 3 in
+      let stack = Stack.create ~capacity () in
+      let items_total = 6 in
+
+      (* two producers *)
+      for i = 0 to 1 do
+        Atomic.spawn (fun () ->
+            for j = 1 to items_total / 2 do
+              (* even nums belong to thr 1, odd nums to thr 2 *)
+              Stack.try_push stack (i + (j * 2)) |> ignore
+            done)
+      done;
+
+      (* checks*)
+      Atomic.final (fun () ->
+          let items = Stack.pop_all stack in
+
+          (* got the same number of items out as in *)
+          Atomic.check (fun () -> capacity = List.length items)))
+
+let pop_pop () =
+  Atomic.trace (fun () ->
+      let stack = Stack.create () in
+      let items_total = 4 in
+
+      for i = 1 to items_total do
+        Stack.try_push stack i |> ignore
+      done;
+
+      (* two consumers *)
+      let lists = [ ref []; ref [] ] in
+      List.iter
+        (fun list ->
+          Atomic.spawn (fun () ->
+              for _ = 1 to items_total / 2 do
+                (* even nums belong to thr 1, odd nums to thr 2 *)
+                list := Option.get (Stack.pop_opt stack) :: !list
+              done)
+          |> ignore)
+        lists;
+
+      (* checks*)
+      Atomic.final (fun () ->
+          let l1 = !(List.nth lists 0) in
+          let l2 = !(List.nth lists 1) in
+
+          (* got the same number of items out as in *)
+          Atomic.check (fun () -> items_total = List.length l1 + List.length l2);
+
+          (* they are in lifo order *)
+          Atomic.check (fun () -> List.sort Int.compare l1 = l1);
+          Atomic.check (fun () -> List.sort Int.compare l2 = l2)))
+
+let pop_push_all () =
+  Atomic.trace (fun () ->
+      let stack = Stack.create () in
+      let n_items = 4 in
+      let items = List.init n_items (fun x -> x + 1) in
+
+      Atomic.spawn (fun () -> Stack.try_push_all stack items |> ignore);
+
+      let popped = ref [] in
+      Atomic.spawn (fun () ->
+          for _ = 1 to n_items do
+            popped := Stack.pop_opt stack :: !popped
+          done);
+
+      Atomic.final (fun () ->
+          let popped =
+            List.filter Option.is_some !popped |> List.map Option.get
+          in
+          (* got the same number of items out as in *)
+          Atomic.check (fun () ->
+              popped
+              = List.filteri
+                  (fun i _ -> i >= n_items - List.length popped)
+                  items)))
+
+let two_domains () =
+  Atomic.trace (fun () ->
+      let stack = Stack.create () in
+      let n1, n2 = (1, 2) in
+
+      (* two producers *)
+      let lists =
+        [
+          (List.init n1 (fun i -> i), ref []);
+          (List.init n2 (fun i -> i + n1), ref []);
+        ]
+      in
+      List.iter
+        (fun (lpush, lpop) ->
+          Atomic.spawn (fun () ->
+              List.iter
+                (fun elt ->
+                  (* even nums belong to thr 1, odd nums to thr 2 *)
+                  Stack.try_push stack elt |> ignore;
+                  lpop := Option.get (Stack.pop_opt stack) :: !lpop)
+                lpush)
+          |> ignore)
+        lists;
+
+      (* checks*)
+      Atomic.final (fun () ->
+          let lpop1 = !(List.nth lists 0 |> snd) in
+          let lpop2 = !(List.nth lists 1 |> snd) in
+
+          (* got the same number of items out as in *)
+          Atomic.check (fun () -> List.length lpop1 = 1);
+          Atomic.check (fun () -> List.length lpop2 = 2);
+
+          (* no element are missing *)
+          Atomic.check (fun () ->
+              List.sort Int.compare (lpop1 @ lpop2)
+              = List.init (n1 + n2) (fun i -> i))))
+
+let two_domains_more_pop () =
+  Atomic.trace (fun () ->
+      let stack = Stack.create () in
+      let n1, n2 = (2, 1) in
+
+      (* two producers *)
+      let lists =
+        [
+          (List.init n1 (fun i -> i), ref []);
+          (List.init n2 (fun i -> i + n1), ref []);
+        ]
+      in
+      List.iter
+        (fun (lpush, lpop) ->
+          Atomic.spawn (fun () ->
+              List.iter
+                (fun elt ->
+                  Stack.try_push stack elt |> ignore;
+                  lpop := Stack.pop_opt stack :: !lpop;
+                  lpop := Stack.pop_opt stack :: !lpop)
+                lpush)
+          |> ignore)
+        lists;
+
+      (* checks*)
+      Atomic.final (fun () ->
+          let lpop1 =
+            !(List.nth lists 0 |> snd)
+            |> List.filter Option.is_some |> List.map Option.get
+          in
+          let lpop2 =
+            !(List.nth lists 1 |> snd)
+            |> List.filter Option.is_some |> List.map Option.get
+          in
+
+          (* got the same number of items out as in *)
+          Atomic.check (fun () ->
+              n1 + n2 = List.length lpop1 + List.length lpop2);
+
+          (* no element are missing *)
+          Atomic.check (fun () ->
+              List.sort Int.compare (lpop1 @ lpop2)
+              = List.init (n1 + n2) (fun i -> i))))
+
+let pop_all () =
+  Atomic.trace (fun () ->
+      let stack = Stack.create () in
+      let n_items = 6 in
+      Atomic.spawn (fun () ->
+          for i = 0 to n_items - 1 do
+            Stack.try_push stack i |> ignore
+          done);
+
+      let popped = ref [] in
+      Atomic.spawn (fun () -> popped := Stack.pop_all stack);
+
+      Atomic.final (fun () ->
+          let remaining = Stack.pop_all stack in
+
+          (* got the same number of items out as in *)
+          Atomic.check (fun () ->
+              remaining @ !popped = List.rev @@ List.init n_items Fun.id)))
+
+let () =
+  let open Alcotest in
+  run "Stack_dscheck"
+    [
+      ( "basic",
+        [
+          test_case "1-producer-1-consumer" `Slow push_pop;
+          test_case "1-producer-1-consumer-capacity" `Slow
+            push_pop_with_capacity;
+          test_case "1-push-1-drop" `Slow push_drop;
+          test_case "2-producers" `Slow push_push;
+          test_case "2-producers-capacity" `Slow push_push_with_capacity;
+          test_case "2-consumers" `Slow pop_pop;
+          test_case "2-domains" `Slow two_domains;
+          test_case "2-domains-more-pops" `Slow two_domains_more_pop;
+          test_case "2-domains-pops_all" `Slow pop_all;
+          test_case "1-pop-1-push-all" `Slow pop_push_all;
+        ] );
+    ]
diff --git a/test/bounded_stack/dune b/test/bounded_stack/dune
new file mode 100644
index 00000000..6e291ec1
--- /dev/null
+++ b/test/bounded_stack/dune
@@ -0,0 +1,23 @@
+(rule
+ (action
+  (copy ../../src/bounded_stack.ml bounded_stack.ml))
+ (package saturn))
+
+(test
+ (package saturn)
+ (name bounded_stack_dscheck)
+ (libraries atomic dscheck alcotest backoff multicore-magic)
+ (build_if
+  (and
+   (>= %{ocaml_version} 5)
+   (not
+    (and
+     (= %{arch_sixtyfour} false)
+     (= %{architecture} arm)))))
+ (modules bounded_stack bounded_stack_dscheck))
+
+(test
+ (package saturn)
+ (name stm_bounded_stack)
+ (modules stm_bounded_stack)
+ (libraries saturn qcheck-core qcheck-stm.stm stm_run))
diff --git a/test/bounded_stack/stm_bounded_stack.ml b/test/bounded_stack/stm_bounded_stack.ml
new file mode 100644
index 00000000..221ea8f4
--- /dev/null
+++ b/test/bounded_stack/stm_bounded_stack.ml
@@ -0,0 +1,108 @@
+(** Sequential and Parallel model-based tests of bounded_queue *)
+
+open QCheck
+open STM
+module Stack = Saturn.Bounded_stack
+
+module Spec = struct
+  type cmd =
+    | Try_push of int
+    (* push_exn uses the same function as try_push *)
+    | Try_push_all of int list
+    (* push_all_exn and add_seq_exn and try_add_seq uses the same function as
+       try_push_all*)
+    | Pop_opt
+    (* peek_exn and drop_exn use the same function as pop_exn*)
+    | Pop_all
+    | Peek_opt
+    (* peek_exn uses the same function as peek_exn *)
+    | To_seq
+    | Is_empty
+    | Is_full
+    | Length
+
+  let string_of_int_list l =
+    "[" ^ String.concat "; " (List.map string_of_int l) ^ "]"
+
+  let show_cmd c =
+    match c with
+    | Try_push i -> "Try_push " ^ string_of_int i
+    | Try_push_all l -> "Try_push_all " ^ string_of_int_list l
+    (* | Push_all_exn l -> "Push_all_exn " ^ string_of_int_list l *)
+    | Pop_opt -> "Pop_opt"
+    | Pop_all -> "Pop_all"
+    | Peek_opt -> "Peek_opt"
+    | To_seq -> "To_seq"
+    | Is_empty -> "Is_empty"
+    | Is_full -> "Is_full"
+    | Length -> "Length"
+
+  type state = int list
+  type sut = int Stack.t
+
+  let arb_cmd _s =
+    let int_gen = Gen.nat in
+    QCheck.make ~print:show_cmd
+      (Gen.oneof
+         [
+           Gen.map (fun i -> Try_push i) int_gen;
+           Gen.map (fun l -> Try_push_all l) (Gen.list int_gen);
+           Gen.return Pop_opt;
+           Gen.return Pop_all;
+           Gen.return Peek_opt;
+           Gen.return To_seq;
+           Gen.return Is_empty;
+           Gen.return Is_full;
+           Gen.return Length;
+         ])
+
+  let init_state = []
+  let capacity = 16
+  let init_sut () = Stack.create ~capacity ()
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with
+    | Try_push i -> if List.length s >= capacity then s else i :: s
+    | Try_push_all l ->
+        if List.length s + List.length l > capacity then s else List.rev l @ s
+    (* | Push_all_exn l ->
+        if List.length s + List.length l > capacity then s else List.rev l @ s *)
+    | Pop_opt -> ( match s with [] -> s | _ :: s' -> s')
+    | Pop_all -> []
+    | Peek_opt -> s
+    | To_seq -> s
+    | Is_empty -> s
+    | Is_full -> s
+    | Length -> s
+
+  let precond _ _ = true
+
+  let run c d =
+    match c with
+    | Try_push i -> Res (bool, Stack.try_push d i)
+    | Try_push_all l -> Res (bool, Stack.try_push_all d l)
+    | Pop_opt -> Res (option int, Stack.pop_opt d)
+    | Pop_all -> Res (list int, Stack.pop_all d)
+    | Peek_opt -> Res (option int, Stack.peek_opt d)
+    | To_seq -> Res (seq int, Stack.to_seq d)
+    | Is_empty -> Res (bool, Stack.is_empty d)
+    | Is_full -> Res (bool, Stack.is_full d)
+    | Length -> Res (int, Stack.length d)
+
+  let postcond c (s : state) res =
+    match (c, res) with
+    | Try_push _, Res ((Bool, _), res) -> List.length s < capacity = res
+    | Try_push_all l, Res ((Bool, _), res) ->
+        List.length s + List.length l <= capacity = res
+    | (Pop_opt | Peek_opt), Res ((Option Int, _), res) -> (
+        match s with [] -> res = None | j :: _ -> res = Some j)
+    | Pop_all, Res ((List Int, _), res) -> res = s
+    | To_seq, Res ((Seq Int, _), res) -> List.of_seq res = s
+    | Is_empty, Res ((Bool, _), res) -> res = (s = [])
+    | Is_full, Res ((Bool, _), res) -> res = (List.length s = capacity)
+    | Length, Res ((Int, _), res) -> res = List.length s
+    | _, _ -> false
+end
+
+let () = Stm_run.run ~name:"Saturn.Bounded_stack" (module Spec) |> exit
diff --git a/test/skiplist/stm_skiplist.ml b/test/skiplist/stm_skiplist.ml
index 0ada005b..1cfeba4a 100644
--- a/test/skiplist/stm_skiplist.ml
+++ b/test/skiplist/stm_skiplist.ml
@@ -64,4 +64,4 @@ module Spec = struct
     | _, _ -> false
 end
 
-let () = Stm_run.run ~name:"Lockfree.Skiplist" (module Spec) |> exit
+let () = Stm_run.run ~name:"Saturn.Skiplist" (module Spec) |> exit