diff --git a/dune-project b/dune-project
index 1194593485..b475e45fb1 100644
--- a/dune-project
+++ b/dune-project
@@ -38,6 +38,7 @@
   unionFind
   ocamlformat
   (junit_alcotest :with-test)
-  ocaml-lsp-server)) ; After upgrading to opam 2.2 use with-dev https://opam.ocaml.org/blog/opam-2-2-0/
+  ocaml-lsp-server
+  (base_quickcheck (>= 0.17.0)))) ; After upgrading to opam 2.2 use with-dev https://opam.ocaml.org/blog/opam-2-2-0/
 
 ; See the complete stanza docs at https://dune.readthedocs.io/en/stable/reference/dune-project/index.html
diff --git a/dune-workspace b/dune-workspace
index 480ccb1514..e070305f87 100644
--- a/dune-workspace
+++ b/dune-workspace
@@ -3,7 +3,7 @@
 (env
  (dev
   (flags
-   (:standard -warn-error -A)))
+   (:standard -w +30 -warn-error -A)))
  (release
   (flags
    (:standard -warn-error +A-58))))
diff --git a/hazel.opam b/hazel.opam
index e78b188325..6ab8569f67 100644
--- a/hazel.opam
+++ b/hazel.opam
@@ -24,6 +24,7 @@ depends: [
   "ocamlformat"
   "junit_alcotest" {with-test}
   "ocaml-lsp-server"
+  "base_quickcheck" {>= "0.17.0"}
   "odoc" {with-doc}
 ]
 build: [
diff --git a/hazel.opam.locked b/hazel.opam.locked
index b2cfce2cea..a5c499f8b5 100644
--- a/hazel.opam.locked
+++ b/hazel.opam.locked
@@ -1,7 +1,7 @@
 
 opam-version: "2.0"
 name: "hazel"
-version: "dev"
+version: "~dev"
 synopsis: "Hazel, a live functional programming environment with typed holes"
 maintainer: "Hazel Development Team"
 authors: "Hazel Development Team"
diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune
index 77e2ca3fe1..6581635b0e 100644
--- a/src/haz3lcore/dune
+++ b/src/haz3lcore/dune
@@ -10,7 +10,8 @@
    js_of_ocaml-ppx
    ppx_let
    ppx_sexp_conv
-   ppx_deriving.show)))
+   ppx_deriving.show
+   base_quickcheck.ppx_quickcheck)))
 
 (env
  (dev
diff --git a/src/haz3lcore/dynamics/FilterAction.re b/src/haz3lcore/dynamics/FilterAction.re
index 6a4dce5ca3..adb9f49986 100644
--- a/src/haz3lcore/dynamics/FilterAction.re
+++ b/src/haz3lcore/dynamics/FilterAction.re
@@ -1,14 +1,14 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type action =
   | Step
   | Eval;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type count =
   | One
   | All;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type t = (action, count);
 
 let string_of_t = v => {
diff --git a/src/haz3lcore/dynamics/InvalidOperationError.re b/src/haz3lcore/dynamics/InvalidOperationError.re
index b317e64254..187f59398f 100644
--- a/src/haz3lcore/dynamics/InvalidOperationError.re
+++ b/src/haz3lcore/dynamics/InvalidOperationError.re
@@ -1,4 +1,4 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type t =
   | InvalidOfString
   | IndexOutOfBounds
diff --git a/src/haz3lcore/dynamics/VarBstMap.re b/src/haz3lcore/dynamics/VarBstMap.re
index 2952690388..570bbc2653 100644
--- a/src/haz3lcore/dynamics/VarBstMap.re
+++ b/src/haz3lcore/dynamics/VarBstMap.re
@@ -1,5 +1,6 @@
 open Util;
 open Ppx_yojson_conv_lib.Yojson_conv;
+open Base_quickcheck;
 module Sexp = Sexplib.Sexp;
 
 module Inner = {
@@ -206,6 +207,9 @@ module Ordered = {
   let without_keys = (keys, m) => {
     filterk(((s, _)) => !List.exists(x => x == s, keys), m);
   };
+
+  let quickcheck_observer_t_ = __ => Observer.opaque;
+  let quickcheck_shrinker_t_ = __ => Shrinker.atomic;
 };
 
 include VarBstMap0;
diff --git a/src/haz3lcore/dynamics/VarBstMap.rei b/src/haz3lcore/dynamics/VarBstMap.rei
index 36a3a20659..cfa3bf3765 100644
--- a/src/haz3lcore/dynamics/VarBstMap.rei
+++ b/src/haz3lcore/dynamics/VarBstMap.rei
@@ -174,4 +174,9 @@ module Ordered: {
     [without_keys] removes all entires with the given keys from the map
    */
   let without_keys: (list(Var.t), t_('a)) => t_('a);
+
+  let quickcheck_observer_t_:
+    Base_quickcheck.Observer.t('a) => Base_quickcheck.Observer.t(t_('a));
+  let quickcheck_shrinker_t_:
+    Base_quickcheck.Shrinker.t('a) => Base_quickcheck.Shrinker.t(t_('a));
 };
diff --git a/src/haz3lcore/lang/Operators.re b/src/haz3lcore/lang/Operators.re
index aa8842b72b..32efc0c398 100644
--- a/src/haz3lcore/lang/Operators.re
+++ b/src/haz3lcore/lang/Operators.re
@@ -1,21 +1,21 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_un_bool =
   | Not;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_un_meta =
   | Unquote;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_un_int =
   | Minus;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin_bool =
   | And
   | Or;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin_int =
   | Plus
   | Minus
@@ -29,7 +29,7 @@ type op_bin_int =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin_float =
   | Plus
   | Minus
@@ -43,25 +43,25 @@ type op_bin_float =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin_string =
   | Concat
   | Equals;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_un =
   | Meta(op_un_meta)
   | Int(op_un_int)
   | Bool(op_un_bool);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin =
   | Int(op_bin_int)
   | Float(op_bin_float)
   | Bool(op_bin_bool)
   | String(op_bin_string);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type ap_direction =
   | Forward
   | Reverse;
diff --git a/src/haz3lcore/lang/term/IdTagged.re b/src/haz3lcore/lang/term/IdTagged.re
index 3812b0e83f..5791b1911f 100644
--- a/src/haz3lcore/lang/term/IdTagged.re
+++ b/src/haz3lcore/lang/term/IdTagged.re
@@ -1,6 +1,7 @@
 open Util;
+open Base_quickcheck;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type t('a) = {
   [@show.opaque]
   ids: list(Id.t),
diff --git a/src/haz3lcore/statics/Constructor.re b/src/haz3lcore/statics/Constructor.re
index 02e897a030..9287eea921 100644
--- a/src/haz3lcore/statics/Constructor.re
+++ b/src/haz3lcore/statics/Constructor.re
@@ -1,6 +1,7 @@
 open Util;
-
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t = string;
+open Base_quickcheck;
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
+type t =
+  [@quickcheck.generator Generator.string_of(Generator.char_alpha)] string;
 
 let equal = String.equal;
diff --git a/src/haz3lcore/statics/ConstructorMap.re b/src/haz3lcore/statics/ConstructorMap.re
index bd4ac26195..00dd3a92e6 100644
--- a/src/haz3lcore/statics/ConstructorMap.re
+++ b/src/haz3lcore/statics/ConstructorMap.re
@@ -1,13 +1,13 @@
 open Util.OptUtil.Syntax;
 open Util;
-
-[@deriving (show({with_path: false}), sexp, yojson)]
+open Base_quickcheck;
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type variant('a) =
   | Variant(Constructor.t, list(Id.t), option('a))
   | BadEntry('a);
 
 // Invariant: Must not have duplicate constructors
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type t('a) = list(variant('a));
 
 let mk =
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index 0c888d8ef7..51df788812 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -1,8 +1,9 @@
 open Util;
+open Base_quickcheck;
 
 let continue = x => x;
 let stop = (_, x) => x;
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type deferral_position_t =
   | InAp
   | OutsideAp;
@@ -45,8 +46,7 @@ type deferral_position_t =
      structural equality except for the case of closures, where it just compares
      the id of the closure.
  */
-
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type any_t =
   | Exp(exp_t)
   | Pat(pat_t)
@@ -146,7 +146,9 @@ and rul_term =
   | Hole(list(any_t))
   | Rules(exp_t, list((pat_t, exp_t)))
 and rul_t = IdTagged.t(rul_term)
-and environment_t = VarBstMap.Ordered.t_(exp_t)
+and environment_t =
+  [@quickcheck.generator Generator.return(VarBstMap.Ordered.empty)]
+  VarBstMap.Ordered.t_(exp_t)
 and closure_environment_t = (Id.t, environment_t)
 and stepper_filter_kind_t =
   | FilterStepper(filter)
diff --git a/src/haz3lcore/statics/Var.re b/src/haz3lcore/statics/Var.re
index 68c3d9d1b3..687dfdca32 100644
--- a/src/haz3lcore/statics/Var.re
+++ b/src/haz3lcore/statics/Var.re
@@ -1,7 +1,8 @@
 open Util;
-
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t = string;
+open Base_quickcheck;
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
+type t =
+  [@quickcheck.generator Generator.string_of(Generator.char_alpha)] string;
 
 let eq = String.equal;
 
diff --git a/src/haz3lcore/tiles/Id.re b/src/haz3lcore/tiles/Id.re
index 5046dd63c5..3b34588113 100644
--- a/src/haz3lcore/tiles/Id.re
+++ b/src/haz3lcore/tiles/Id.re
@@ -1,5 +1,5 @@
 open Util;
-
+open Base_quickcheck;
 /* ID FAQ
 
    WHATS AN ID?
@@ -34,7 +34,7 @@ open Util;
 
    */
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 let sexp_of_t: Uuidm.t => Sexplib.Sexp.t =
   t => Sexplib.Sexp.Atom(Uuidm.to_string(t));
 
@@ -59,6 +59,9 @@ let t_of_yojson: Yojson.Safe.t => Uuidm.t =
 type t = Uuidm.t;
 
 let mk: unit => t = Uuidm.v4_gen(Random.State.make_self_init());
+let quickcheck_generator = Generator.return(mk()); // TODO
+let quickcheck_observer = Observer.opaque;
+let quickcheck_shrinker = Shrinker.atomic;
 
 let compare: (t, t) => int = Uuidm.compare;
 let to_string: (~upper: bool=?, t) => string = Uuidm.to_string;