diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index f9f7456..05a7859 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -20,6 +20,9 @@ jobs:
 
     runs-on: ${{ matrix.os }}
 
+    env:
+      QCHECK_MSG_INTERVAL: '60'
+
     steps:
       - name: Checkout code
         uses: actions/checkout@v2
@@ -45,4 +48,4 @@ jobs:
 
       - run: opam exec -- make all
 
-      - run: opam exec -- make run_test
\ No newline at end of file
+      - run: opam exec -- make run_test
diff --git a/domainslib.opam b/domainslib.opam
index 99b1fd0..9e5c86f 100644
--- a/domainslib.opam
+++ b/domainslib.opam
@@ -13,6 +13,9 @@ depends: [
   "dune" {>= "3.0"}
   "lockfree" { >= "0.2.0"}
   "mirage-clock-unix" {with-test}
+  "qcheck-core" {with-test & >= "0.20"}
+  "qcheck-multicoretests-util" {with-test & >= "0.1"}
+  "qcheck-stm" {with-test & >= "0.1"}
 ]
 depopts: []
 build: [
diff --git a/test/chan_stm_tests.ml b/test/chan_stm_tests.ml
new file mode 100644
index 0000000..4c8b45d
--- /dev/null
+++ b/test/chan_stm_tests.ml
@@ -0,0 +1,86 @@
+open QCheck
+open Domainslib
+open STM
+
+(** This contains sequential and parallel model-based tests of [Domainslib.Chan] *)
+
+module ChConf =
+struct
+  type state = int list
+  type sut = int Domainslib.Chan.t
+  type cmd =
+    | Send of int
+    | Send_poll of int
+    | Recv
+    | Recv_poll
+
+  let show_cmd c = match c with
+    | Send i -> "Send" ^ (string_of_int i)
+    | Send_poll i -> "Send_poll" ^ (string_of_int i)
+    | Recv -> "Recv"
+    | Recv_poll -> "Recv_poll"
+
+  let capacity = 8
+
+  let arb_cmd s =
+    let int_gen = Gen.nat in
+    QCheck.make ~print:show_cmd
+      (if s=[]
+       then
+         Gen.oneof
+           [Gen.map (fun i -> Send i) int_gen;
+	    Gen.map (fun i -> Send_poll i) int_gen;
+	    Gen.return Recv_poll] (* don't generate blocking Recv cmds on an empty channel *)
+       else
+       if List.length s >= capacity
+       then
+         Gen.oneof
+           [Gen.map (fun i -> Send_poll i) int_gen;
+            Gen.return Recv;
+	    Gen.return Recv_poll] (* don't generate blocking Send cmds on a full channel *)
+       else
+         Gen.oneof
+           [Gen.map (fun i -> Send i) int_gen;
+	    Gen.map (fun i -> Send_poll i) int_gen;
+            Gen.return Recv;
+	    Gen.return Recv_poll])
+  let init_state  = []
+  let init_sut () = Chan.make_bounded capacity
+  let cleanup _   = ()
+
+  let next_state c s = match c with
+    | Send i      -> if List.length s < capacity then s@[i] else s
+    | Send_poll i -> if List.length s < capacity then s@[i] else s
+    | Recv        -> begin match s with [] -> [] | _::s' -> s' end
+    | Recv_poll   -> begin match s with [] -> [] | _::s' -> s' end
+
+  let precond c s = match c,s with
+    | Recv,   [] -> false
+    | Send _, _  -> List.length s < capacity
+    | _,      _  -> true
+
+  let run c chan =
+    match c with
+    | Send i       -> Res (unit, Chan.send chan i)
+    | Send_poll i  -> Res (bool, Chan.send_poll chan i)
+    | Recv         -> Res (int, Chan.recv chan)
+    | Recv_poll    -> Res (option int, Chan.recv_poll chan)
+
+  let postcond c s res = match c,res with
+    | Send _,      Res ((Unit,_),_) -> (List.length s < capacity)
+    | Send_poll _, Res ((Bool,_),res) -> res = (List.length s < capacity)
+    | Recv,        Res ((Int,_),res) -> (match s with [] -> false | res'::_ -> Int.equal res res')
+    | Recv_poll,   Res ((Option Int,_),opt) -> (match s with [] -> None | res'::_ -> Some res') = opt
+    | _,_ -> false
+end
+
+
+module ChT_seq = STM_sequential.Make(ChConf)
+module ChT_dom = STM_domain.Make(ChConf)
+
+let () =
+  let count = 500 in
+  QCheck_base_runner.run_tests_main [
+    ChT_seq.agree_test     ~count ~name:"STM Domainslib.Chan test sequential";
+    ChT_dom.agree_test_par ~count ~name:"STM Domainslib.Chan test parallel";
+  ]
diff --git a/test/dune b/test/dune
index 346e8e1..f84a968 100644
--- a/test/dune
+++ b/test/dune
@@ -110,3 +110,31 @@
  (libraries domainslib)
  (modules off_by_one)
  (modes native))
+
+;; Custom property-based tests using QCheck
+
+(test
+ (name task_one_dep)
+ (modules task_one_dep)
+ (libraries qcheck-multicoretests-util qcheck-core qcheck-core.runner domainslib)
+ (action (run %{test} --verbose)))
+
+(test
+ (name task_more_deps)
+ (modules task_more_deps)
+ (libraries qcheck-multicoretests-util qcheck-core qcheck-core.runner domainslib)
+ (action (run %{test} --verbose)))
+
+(test
+ (name task_parallel)
+ (modules task_parallel)
+ (libraries qcheck-multicoretests-util qcheck-core qcheck-core.runner domainslib)
+ (action (run %{test} --verbose)))
+
+;; STM_sequential and STM_domain test of Domainslib.Chan
+
+(test
+ (name chan_stm_tests)
+ (modules chan_stm_tests)
+ (libraries qcheck-stm.sequential qcheck-stm.domain domainslib)
+ (action (run %{test} --verbose)))
diff --git a/test/task_more_deps.ml b/test/task_more_deps.ml
new file mode 100644
index 0000000..79dd414
--- /dev/null
+++ b/test/task_more_deps.ml
@@ -0,0 +1,107 @@
+(**
+  Generate tests of async+await from Domainslib.Task.
+  It does so by generating a random, acyclic dependency graph of [async] tasks,
+  each [await]ing on its dependency.
+ *)
+
+open QCheck
+open Domainslib
+
+(* a simple work item, from ocaml/testsuite/tests/misc/takc.ml *)
+let rec tak x y z =
+  if x > y then tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y)
+           else z
+
+let work () =
+  for _ = 1 to 200 do
+    assert (7 = tak 18 12 6);
+  done
+
+(* Generates a DAG of dependencies                          *)
+(* Each task is represented by an array index w/a deps.list *)
+(* This example DAG
+
+     A/0 <--- B/1 <
+      ^.           \
+        \           \
+         `- C/2 <--- D/3
+
+   is represented as: [| []; [0]; [0]; [1;2] |] *)
+let gen_dag n st =
+  Array.init n (fun i ->
+      let deps = ref [] in
+      for dep = 0 to i-1 do
+        if Gen.bool st then deps := dep :: !deps
+      done;
+      List.rev !deps)
+
+type test_input =
+  {
+    num_domains  : int;
+    length       : int;
+    dependencies : int list array
+  }
+
+let show_test_input t =
+  Printf.sprintf
+    "{ num_domains : %i\n  length : %i\n  dependencies : %s }"
+    t.num_domains t.length Print.(array (list int) t.dependencies)
+
+let shrink_deps test_input =
+  let ls = Array.to_list test_input.dependencies in
+  let is = Shrink.list ~shrink:Shrink.list ls in
+  Iter.map
+    (fun deps ->
+       let len = List.length deps in
+       let arr = Array.of_list deps in
+       let deps = Array.mapi (fun i i_deps -> match i,i_deps with
+           | 0, _
+           | _,[] -> []
+           | _,[0] -> [0]
+           | _, _ ->
+             List.map (fun j ->
+                 if j<0 || j>=len || j>=i (* ensure reduced dep is valid *)
+                 then ((j + i) mod i)
+                 else j) i_deps) arr in
+       { test_input with length=len; dependencies=deps }) is
+
+let arb_deps domain_bound promise_bound =
+  let gen_deps =
+    Gen.(pair (int_bound (domain_bound-1)) (int_bound promise_bound) >>= fun (num_domains,length) ->
+         let num_domains = succ num_domains in
+         let length = succ length in
+         gen_dag length >>= fun dependencies -> return { num_domains; length; dependencies }) in
+  make ~print:show_test_input ~shrink:(shrink_deps) gen_deps
+
+let build_dep_graph pool test_input =
+  let len = test_input.length in
+  let deps = test_input.dependencies in
+  let rec build i promise_acc =
+    if i=len
+    then promise_acc
+    else
+      let p = (match deps.(i) with
+          | [] ->
+            Task.async pool work
+          | deps ->
+            Task.async pool (fun () ->
+                work ();
+                List.iter (fun dep -> Task.await pool (List.nth promise_acc (i-1-dep))) deps)) in
+      build (i+1) (p::promise_acc)
+  in
+  build 0 []
+
+let test_one_pool ~domain_bound ~promise_bound =
+  Test.make ~name:"Domainslib.Task.async/await, more deps, 1 work pool" ~count:100
+    (arb_deps domain_bound promise_bound)
+    (Util.repeat 10
+       (fun test_input ->
+          let pool = Task.setup_pool ~num_domains:test_input.num_domains () in
+          Task.run pool (fun () ->
+              let ps = build_dep_graph pool test_input in
+              List.iter (fun p -> Task.await pool p) ps);
+          Task.teardown_pool pool;
+          true))
+
+let () =
+  QCheck_base_runner.run_tests_main [test_one_pool ~domain_bound:8 ~promise_bound:10]
diff --git a/test/task_one_dep.ml b/test/task_one_dep.ml
new file mode 100644
index 0000000..c2b37fa
--- /dev/null
+++ b/test/task_one_dep.ml
@@ -0,0 +1,147 @@
+(**
+  Generate tests of async+await from Domainslib.Task.
+  It does so by generating a random, acyclic dependency graph of [async] tasks,
+  each [await]ing on its dependency.
+ *)
+
+open QCheck
+open Domainslib
+
+(* a simple work item, from ocaml/testsuite/tests/misc/takc.ml *)
+let rec tak x y z =
+  if x > y then tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y)
+           else z
+
+let work () =
+  for _ = 1 to 200 do
+    assert (7 = tak 18 12 6);
+  done
+
+(* Generates a sparse DAG of dependencies                           *)
+(* Each task is represented by an array index w/at most 1 dep. each *)
+(* This example DAG
+
+     A/0 <--- B/1
+      ^.
+        \
+         `- C/2 <--- D/3
+
+   is represented as: [| None; Some 0; Some 0; Some 2 |] *)
+let gen_deps n st =
+  let a = Array.make n None in
+  for i=1 to n-1 do
+    if Gen.bool st then a.(i) <- Some (Gen.int_bound (i-1) st)
+  done;
+  a
+
+type test_input =
+  {
+    num_domains  : int;
+    length       : int;
+    dependencies : int option array
+  }
+
+let show_test_input t =
+  Printf.sprintf
+    "{ num_domains : %i\n  length : %i\n  dependencies : %s }"
+    t.num_domains t.length Print.(array (option int) t.dependencies)
+
+let shrink_deps test_input =
+  let ls = Array.to_list test_input.dependencies in
+  let is = Shrink.list ~shrink:Shrink.(option nil) ls in
+  Iter.map
+    (fun deps ->
+       let len = List.length deps in
+       let arr = Array.of_list deps in
+       let deps = Array.mapi (fun i j_opt -> match i,j_opt with
+            | 0, _
+            | _,None -> None
+            | _,Some 0 -> Some 0
+            | _, Some j ->
+              if j<0 || j>=len || j>=i (* ensure reduced dep is valid *)
+              then Some ((j + i) mod i)
+              else Some j) arr in
+       { test_input with length=len; dependencies=deps }) is
+
+let arb_deps domain_bound promise_bound =
+  let gen_deps =
+    Gen.(pair (int_bound (domain_bound-1)) (int_bound promise_bound) >>= fun (num_domains,length) ->
+         let num_domains = succ num_domains in
+         let length = succ length in
+         gen_deps length >>= fun dependencies -> return { num_domains; length; dependencies }) in
+  let shrink_input input =
+    Iter.append
+      (Iter.map (fun doms' -> { input with num_domains = doms' }) (Shrink.int input.num_domains))
+      (shrink_deps input) in
+  make ~print:show_test_input ~shrink:shrink_input gen_deps
+
+let build_dep_graph pool test_input =
+  let len = test_input.length in
+  let deps = test_input.dependencies in
+  let rec build i promise_acc =
+    if i=len
+    then promise_acc
+    else
+      let p = (match deps.(i) with
+          | None ->
+            Task.async pool work
+          | Some dep ->
+            Task.async pool (fun () ->
+                work();
+                Task.await pool (List.nth promise_acc (i-1-dep)))) in
+      build (i+1) (p::promise_acc)
+  in
+  build 0 []
+
+let test_one_pool ~domain_bound ~promise_bound =
+  Test.make ~name:"Domainslib.Task.async/await, one dep, 1 work pool" ~count:100
+    (arb_deps domain_bound promise_bound)
+    (Util.repeat 10 @@
+     fun input ->
+     let pool = Task.setup_pool ~num_domains:input.num_domains () in
+     Task.run pool (fun () ->
+         let ps = build_dep_graph pool input in
+         List.iter (fun p -> Task.await pool p) ps);
+     Task.teardown_pool pool;
+     true)
+
+let test_two_pools_sync_last ~domain_bound ~promise_bound =
+  let gen = arb_deps domain_bound promise_bound in
+  Test.make ~name:"Domainslib.Task.async/await, one dep, w.2 pools, syncing at the end" ~count:100
+    (pair gen gen)
+    (Util.repeat 10 @@
+     fun (input1,input2) ->
+     let pool1 = Task.setup_pool ~num_domains:input1.num_domains () in
+     let pool2 = Task.setup_pool ~num_domains:input2.num_domains () in
+     let ps1 = build_dep_graph pool1 input1 in
+     let ps2 = build_dep_graph pool2 input2 in
+     Task.run pool1 (fun () -> List.iter (fun p -> Task.await pool1 p) ps1);
+     Task.run pool2 (fun () -> List.iter (fun p -> Task.await pool2 p) ps2);
+     Task.teardown_pool pool1;
+     Task.teardown_pool pool2;
+     true)
+
+let test_two_nested_pools ~domain_bound ~promise_bound =
+  let gen = arb_deps domain_bound promise_bound in
+  Test.make ~name:"Domainslib.Task.async/await, one dep, w.2 nested pools" ~count:100
+    (pair gen gen)
+    (Util.repeat 10 @@
+     fun (input1,input2) ->
+     let pool1 = Task.setup_pool ~num_domains:input1.num_domains () in
+     let pool2 = Task.setup_pool ~num_domains:input2.num_domains () in
+     Task.run pool1 (fun () ->
+         Task.run pool2 (fun () ->
+             let ps1 = build_dep_graph pool1 input1 in
+             let ps2 = build_dep_graph pool2 input2 in
+             List.iter (fun p -> Task.await pool1 p) ps1;
+             List.iter (fun p -> Task.await pool2 p) ps2));
+     Task.teardown_pool pool1;
+     Task.teardown_pool pool2;
+     true)
+
+let () =
+  QCheck_base_runner.run_tests_main [
+    test_one_pool            ~domain_bound:8 ~promise_bound:10;
+    test_two_pools_sync_last ~domain_bound:2 ~promise_bound:2;
+    test_two_nested_pools    ~domain_bound:8 ~promise_bound:10;
+  ]
diff --git a/test/task_parallel.ml b/test/task_parallel.ml
new file mode 100644
index 0000000..3888d6f
--- /dev/null
+++ b/test/task_parallel.ml
@@ -0,0 +1,44 @@
+open QCheck
+open Domainslib
+
+(** Property-based QCheck tests of Task.parallel_* *)
+
+let count = 250
+
+let test_parallel_for =
+  Test.make ~name:"Domainslib.Task.parallel_for test" ~count
+    (triple (int_bound 10) small_nat small_nat)
+    (fun (num_domains,array_size,chunk_size) ->
+       let pool = Task.setup_pool ~num_domains () in
+       let res = Task.run pool (fun () ->
+           let a = Atomic.make 0 in
+           Task.parallel_for ~chunk_size ~start:0 ~finish:(array_size-1) ~body:(fun _ -> Atomic.incr a) pool;
+           Atomic.get a) in
+       Task.teardown_pool pool;
+       res = array_size)
+
+let test_parallel_for_reduce =
+  Test.make ~name:"Domainslib.Task.parallel_for_reduce test" ~count
+    (triple (int_bound 10) small_nat small_nat)
+    (fun (num_domains,array_size,chunk_size) ->
+       let pool = Task.setup_pool ~num_domains () in
+       let res = Task.run pool (fun () ->
+           Task.parallel_for_reduce ~chunk_size ~start:0 ~finish:(array_size-1) ~body:(fun _ -> 1) pool (+) 0) in
+       Task.teardown_pool pool;
+       res = array_size)
+
+let test_parallel_scan =
+  Test.make ~name:"Domainslib.Task.parallel_scan test" ~count
+    (pair (int_bound 10) small_nat)
+    (fun (num_domains,array_size) ->
+       let pool = Task.setup_pool ~num_domains () in
+       let a = Task.run pool (fun () -> Task.parallel_scan pool (+) (Array.make array_size 1)) in
+       Task.teardown_pool pool;
+       a = Array.init array_size (fun i -> i + 1))
+
+let () =
+  QCheck_base_runner.run_tests_main [
+    test_parallel_for;
+    test_parallel_for_reduce;
+    test_parallel_scan;
+  ]