diff --git a/dune-project b/dune-project
index 20da7e14..8cd96c93 100644
--- a/dune-project
+++ b/dune-project
@@ -1,5 +1,7 @@
-(lang dune 3.0)
+(lang dune 3.8)
 (using dune_site 0.1)
+(using mdx 0.4)
+
 (name ortac)
 
 (package
diff --git a/ortac-core.opam b/ortac-core.opam
index ce53b2fd..d32b0e31 100644
--- a/ortac-core.opam
+++ b/ortac-core.opam
@@ -29,7 +29,7 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "dune-site"
   "cmdliner" {>= "1.1.0"}
   "fmt"
diff --git a/ortac-monolith.opam b/ortac-monolith.opam
index f4e6803c..12fa2905 100644
--- a/ortac-monolith.opam
+++ b/ortac-monolith.opam
@@ -24,7 +24,7 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "cmdliner" {>= "1.1.0"}
   "fmt"
   "ppxlib" {>= "0.26.0"}
diff --git a/ortac-qcheck-stm.opam b/ortac-qcheck-stm.opam
index da64bad9..d752752a 100644
--- a/ortac-qcheck-stm.opam
+++ b/ortac-qcheck-stm.opam
@@ -27,10 +27,11 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "cmdliner" {>= "1.1.0"}
   "fmt"
   "ppxlib" {>= "0.26.0"}
+  "mdx" {with-test}
   "gospel" {>= "0.2.0"}
   "qcheck-core" {with-test}
   "qcheck-stm" {with-test}
diff --git a/ortac-runtime-monolith.opam b/ortac-runtime-monolith.opam
index 5e57e8bd..ecf32830 100644
--- a/ortac-runtime-monolith.opam
+++ b/ortac-runtime-monolith.opam
@@ -24,7 +24,7 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "monolith" {>= "20201026"}
   "pprint"
   "fmt" {>= "0.9.0"}
diff --git a/ortac-runtime.opam b/ortac-runtime.opam
index 21010c9a..b2e115f7 100644
--- a/ortac-runtime.opam
+++ b/ortac-runtime.opam
@@ -12,7 +12,7 @@ doc: "https://pascutto.github.io/ortac/"
 bug-reports: "https://github.com/ocaml-gospel/ortac/issues"
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "fmt"
   "zarith"
   "monolith" {with-test}
diff --git a/ortac-wrapper.opam b/ortac-wrapper.opam
index 4d254909..ae0f63e9 100644
--- a/ortac-wrapper.opam
+++ b/ortac-wrapper.opam
@@ -28,7 +28,7 @@ build: [
 
 depends: [
   "ocaml" {>= "4.11.0"}
-  "dune" {>= "3.0"}
+  "dune" {>= "3.8"}
   "dune-site"
   "cmdliner" {>= "1.1.0"}
   "fmt"
diff --git a/plugins/qcheck-stm/doc/dune b/plugins/qcheck-stm/doc/dune
new file mode 100644
index 00000000..598f57e0
--- /dev/null
+++ b/plugins/qcheck-stm/doc/dune
@@ -0,0 +1,20 @@
+(mdx
+ (package ortac-qcheck-stm)
+ (deps
+  (package ortac-core)
+  (package ortac-qcheck-stm)))
+
+(documentation
+ (package ortac-qcheck-stm)
+ (mld_files index))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (deps
+  (:examples
+   (glob_files *.mli))
+  (package gospel))
+ (action
+  (ignore-outputs
+   (run gospel check %{examples}))))
diff --git a/plugins/qcheck-stm/doc/example.mli b/plugins/qcheck-stm/doc/example.mli
new file mode 100644
index 00000000..169c245f
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example.mli
@@ -0,0 +1,36 @@
+(* $MDX part-begin=type-decl *)
+
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+(* $MDX part-end *)
+
+(* $MDX part-begin=make *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-end *)
+
+(* $MDX part-begin=set *)
+
+val set : 'a t -> int -> 'a -> unit
+(*@ set t i a
+    checks 0 <= i < t.size
+    modifies t.contents
+    ensures t.contents = List.mapi (fun j x -> if j = (i : integer) then a else x) (old t.contents) *)
+
+(* $MDX part-end *)
+
+(* $MDX part-begin=get *)
+
+val get : 'a t -> int -> 'a
+(*@ a = get t i
+    checks 0 <= i < t.size
+    ensures a = List.nth t.contents i *)
+
+(* $MDX part-end *)
diff --git a/plugins/qcheck-stm/doc/example_for_all.mli b/plugins/qcheck-stm/doc/example_for_all.mli
new file mode 100644
index 00000000..ee465bbe
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example_for_all.mli
@@ -0,0 +1,17 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val for_all : 'a t -> bool
+(*@ b = for_all t
+    ensures b = List.for_all (fun x -> x = x) t.contents *)
+
+(* $MDX part-end *)
diff --git a/plugins/qcheck-stm/doc/example_ghost.mli b/plugins/qcheck-stm/doc/example_ghost.mli
new file mode 100644
index 00000000..dd1b593d
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example_ghost.mli
@@ -0,0 +1,16 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val ghost_arg : char -> 'a t -> bool
+(*@ b = ghost_arg [ i : integer] c t *)
+
+(* $MDX part-end *)
diff --git a/plugins/qcheck-stm/doc/example_ill_formed_quantification.mli b/plugins/qcheck-stm/doc/example_ill_formed_quantification.mli
new file mode 100644
index 00000000..e226cd49
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example_ill_formed_quantification.mli
@@ -0,0 +1,17 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val unsupported_quantification : 'a t -> bool
+(*@ b = unsupported_quantification t
+    ensures b = forall a. List.mem a t.contents -> a = a *)
+
+(* $MDX part-end *)
diff --git a/plugins/qcheck-stm/doc/example_incompatible_type.mli b/plugins/qcheck-stm/doc/example_incompatible_type.mli
new file mode 100644
index 00000000..6b306f90
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example_incompatible_type.mli
@@ -0,0 +1,16 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val incompatible_type : char -> string t -> bool
+(*@ b = incompatible_type c t *)
+
+(* $MDX part-end *)
diff --git a/plugins/qcheck-stm/doc/example_limitations.mli b/plugins/qcheck-stm/doc/example_limitations.mli
new file mode 100644
index 00000000..c22da26e
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example_limitations.mli
@@ -0,0 +1,31 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val f : int -> int -> bool
+(*@ b = f x y *)
+
+val compare : 'a t -> 'a t -> bool
+(*@ b = compare t1 t2 *)
+
+val of_list : 'a list -> 'a t
+(*@ t = of_list xs *)
+
+val g : int * int -> 'a t -> bool
+(*@ b = g x t *)
+
+val h : 'a t -> 'a * 'a
+(*@ (l, r) = h t *)
+
+val for_all : ('a -> bool) -> 'a t -> bool
+(*@ b = for_all p t *)
+
+(* $MDX part-end *)
diff --git a/plugins/qcheck-stm/doc/example_next_state.mli b/plugins/qcheck-stm/doc/example_next_state.mli
new file mode 100644
index 00000000..55588930
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example_next_state.mli
@@ -0,0 +1,18 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+(* $MDX part-begin=fun-decl *)
+
+val ensures_not_found_for_next_state : 'a t -> unit
+(*@ ensures_not_found_for_next_state t
+    modifies t.contents
+    ensures List.length t.contents = List.length (old t.contents) *)
+
+(* $MDX part-end *)
diff --git a/plugins/qcheck-stm/doc/example_unknown_type.mli b/plugins/qcheck-stm/doc/example_unknown_type.mli
new file mode 100644
index 00000000..da158a84
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example_unknown_type.mli
@@ -0,0 +1,18 @@
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+
+type new_type
+
+(* $MDX part-begin=fun-decl *)
+
+val type_not_supported : new_type -> 'a t -> new_type
+(*@ y = type_not_supported x t *)
+
+(* $MDX part-end *)
diff --git a/plugins/qcheck-stm/doc/index.mld b/plugins/qcheck-stm/doc/index.mld
new file mode 100644
index 00000000..b29798d8
--- /dev/null
+++ b/plugins/qcheck-stm/doc/index.mld
@@ -0,0 +1,430 @@
+{0 Ortac/QCheck-STM}
+
+{1 Content}
+
+{1 Overview}
+
+The [qcheck-stm] plugin for [ortac] (called Ortac/QCheck-STM in order to avoid
+ambiguities) generates a standalone executable using
+{{:https://ocaml-multicore.github.io/multicoretests/ }QCheck-STM} to perform
+model-based state-machine testing of a module, building up the model from its
+{{: https://ocaml-gospel.github.io/gospel/ }Gospel} specifications.
+
+In order to be able to generate the STM module, the plugin will need five
+pieces of information:
+
+{ol {- What type do we want to test? This is called {e system under test} or {e
+       SUT} by QCheck-STM.}
+    {- How to generate a value of this type? The [init_sut] function.}
+    {- What is the model of this type? This is what is taken as the {e state} by QCheck-STM.}
+    {- How to generate the said model? The [init_state] function.}
+    {- How does the model change when calling a function? The [next_state] function.}}
+
+Answering these five questions is done part in the command-line arguments and
+part in the Gospel specifications that you will have to write in a specific
+style.
+
+This tutorial aims at showing how to write Gospel specifications for your
+modules in order to be able to automatically generate the QCheck-STM tests
+with the [ortac] command-line tool and its Ortac/QCheck-STM plugin.
+
+We are going to build an example for a simple fixed-size container library.
+
+{1 How to write Gospel specifications?}
+
+In order to use the Ortac/QCheck-STM, the module you want to test must
+contain three kinds of items:
+
+{ol {- The type declaration for [SUT]}
+    {- The function used to generate the initial value of [SUT]}
+    {- Functions to be tested}}
+
+Here is an example for the declaration of type [SUT]:
+
+{@ocaml file=example.mli,part=type-decl[
+type 'a t
+(*@ model size : int
+    mutable model contents : 'a list *)
+]}
+
+You'll notice the Gospel specifications under the type declaration, in the
+special Gospel comments. These specifications give two models to the type, one
+non mutable and one mutable. These models are necessary (or at least some
+models) in order to give enough information to the [qcheck-stm] plugin to build
+the functional {e state} that QCheck-STM will be using. This item is then
+bringing two needed pieces of information: what are the type of the [SUT] and
+the type of the [state].
+
+The second item is the function used for generating the inital value for [SUT].
+Here again, this item will bring two needed pieces of information: how to build
+the initial value of [SUT] and the corresponding [state]. This is the role of
+the [make] function along with its specification.
+
+{@ocaml file=example.mli,part=make[
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    checks i >= 0
+    ensures t.size = i
+    ensures t.contents = List.init i (fun j -> a) *)
+]}
+
+Obviously, the function should return a value of type [SUT]. But more
+importantly, the specification has to give a value to each of the models that
+were given to the type [SUT] in its specification. Here, this means we need to
+give a value to [t.size] and to [t.contents]. The [checks] clause is part of
+the Gospel specification of the function, but it won't be used by the plugin to
+generate any code. You can give more information that the plugin needs, for
+example if you are also using another tool based on Gospel specifications. The
+plugin will simply ignore them.
+
+Now that Ortac/QCheck-STM is able to generate an initial value for the type
+under test and its model, we can turn our attention to the functions we will
+want to test. Here is the example of the classic [set] function along with its
+Gospel specification written with the [qcheck-stm] ortac plugin in mind:
+
+{@ocaml file=example.mli,part=set[
+val set : 'a t -> int -> 'a -> unit
+(*@ set t i a
+    checks 0 <= i < t.size
+    modifies t.contents
+    ensures t.contents = List.mapi (fun j x -> if j = (i : integer) then a else x) (old t.contents) *)
+]}
+
+The most important purpose of the specifications (in the context of this
+tutorial) is to bring the last piece of information. That is to answer the
+question about how the model changes when calling the specified function.
+This is done in two steps.
+
+First, you have to declare which of the model's field are modified in the
+[modifies] clause. Note that if, like in the case of the [set] function, the
+function is returning [unit], it is a Gospel error to not give any [modifies]
+clause. But Gospel lets you write [modifies ()] in order to express the fact
+that the function is modifying something that is not in the model of any of the
+argument. However, Ortac/QCheck-STM will read the [modifies] clauses (if
+any) in order to determine which model's fields are modified when the function
+is called. The model's fields that don't appear in any of the [modifies]
+clauses will be considered as not modified.
+
+Then, the plugin will look at the [ensures] clauses (the postconditions) in
+order to find one clause per modified field that expresses how to compute the
+modification. For now, the tool is not very smart. The basic rule of thumb is
+that you need to write down a computable description of the new model's field
+as a function of the old one. This will often mean that you need to write
+stronger postconditions that what would be necessary in another context. If the
+plugin can't find any suitable [ensures] clause, it will raise a warning and
+skip the function for test.
+
+You can see again the [checks] clause. This time, as the function is a
+candidate for test, the [checks] clause will be used by the tool to check that
+if the condition of the clause is not respected, the function raises the
+[Invalid_arg] exception.
+
+Now that the [set] function is ready to be tested, let's turn our attention to
+another example. Here is the example of the [get] function along with its Gospel
+specifications:
+
+{@ocaml file=example.mli,part=get[
+val get : 'a t -> int -> 'a
+(*@ a = get t i
+    checks 0 <= i < t.size
+    ensures a = List.nth t.contents i *)
+]}
+
+Here, the [ensures] clause has another use. As the [get] function does not
+modifies anything, there is no need to give the values of the model’s fields
+after the function. Note that the [ensures] clause wouldn't have been fit for
+this purpose anyway. The [ensures] clauses that are not used for the
+[next_state] function are used for checking postconditions, here a postcondition
+stating a relation between the returned value and the function arguments. These
+[ensures] clauses are not necessary to generate the QCheck-STM tests, but they
+will bring strength to your tests.
+
+In order to generate postcondition-checking, Ortac/QCheck-STM uses the
+[ensures] clauses that were not used for the [next_state] function but it also
+uses the [checks] clauses and the [raises] ones.
+
+Now you can generate the QCheck-STM file by running the following command where
+you indicate the file you want to test, the function call to build a value of
+the type indicated in the third argument. You can write the generated code into
+a file, using the [-o] option.
+
+{@sh set-ORTAC_ONLY_PLUGIN=qcheck-stm[
+$ ortac qcheck-stm example.mli "make 42 'a'" "char t" -o stm_example.ml
+]}
+
+The generated OCaml file has a bunch of dependencies:
+
+{ul {li [qcheck-core] }
+    {li [qcheck-core.runner] }
+    {li [qcheck-stm.stm] }
+    {li [qcheck-stm.sequential] }
+    {li [qckeck-multicoretests-util] }
+    {li [ortac-runtime] } }
+
+Using the dune build system, your dune rule for the example above would look
+like the following:
+
+{@dune[
+(test
+ (name stm_example)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-multicoretests-util
+  ortac-runtime
+  example)
+ (action
+  (run %{test} --verbose)))
+]}
+
+{1 Warning system}
+
+Now that you know what Gospel specifications for the [qcheck-stm] plugin should
+look like and how to generate the QCheck-STM file, let's focus on what can go
+wrong. The [qcheck-stm] plugin has an extensive set of warnings to help you
+formulate your specifications in a way it can use.
+
+Most of the time, Ortac/QCheck-STM will skip a function if it can't generate
+one of the elements needed by QCheck-STM. Doing so, it will display a warning on
+[stderr] in order for you to be able to get an idea about test coverage.
+
+
+{2 Ortac/QCheck-STM specifics}
+
+Let's start with the warnings specific to the plugin.
+
+The principle at the core of Ortac/QCheck-STM is to turn the Gospel
+specifications into OCaml code needed by the QCheck-STM test framework. This
+means that you need to provide these pieces of information into the
+specification in a style that allows the plugin to understand them.
+
+The most delicate piece of information you have to give is how the function
+modifies the model of the [SUT]. As stated above, the plugin is looking for
+this information in the [ensures] clauses.
+
+If Ortac/QCheck-STM doesn't have enough information in your specifications in
+order to compute the next value for every model's field appearing in a
+[modifies] clause, it won't be able to test the function and inform you with a
+warning.
+
+For example, the following specifications are not enough for Ortac/QCheck-STM.
+
+{@ocaml file=example_next_state.mli,part=fun-decl[
+val ensures_not_found_for_next_state : 'a t -> unit
+(*@ ensures_not_found_for_next_state t
+    modifies t.contents
+    ensures List.length t.contents = List.length (old t.contents) *)
+]}
+
+Ortac/QCheck-STM will look at the [modifies] clause and then look for an
+[ensures] clause for each of the modified models that allows to compute its
+new value. Here, it won't find any and warn you with the following message:
+
+{@sh[
+$ ortac qcheck-stm example_next_state.mli "make 42 'a'" "char t" -o foo.ml
+File "example_next_state.mli", line 15, characters 13-23:
+15 |     modifies t.contents
+                  ^^^^^^^^^^
+Warning: Skipping ensures_not_found_for_next_state: model contents is
+         declared as modified by the function but no suitable ensures clause
+         was found. Specifications should contain at least one "ensures
+         x.contents = ..." where x is the SUT.
+]}
+
+Note that you don't have to rewrite the clause. Maybe it contains information
+you still want to state in your specifications. You can then add another
+[ensures] clause with the relevant information in order to compute the new value
+of the modified model. The warning message gives you the form in which the
+plugin expects to find the information, namely a description of the new state
+by an expression in which any reference to the state should be to the old
+state (that is the state before the function is called).
+
+Note also that if you write [modifies t], the plugin assumes that all the
+mutable fields are modified and will try to find a description for all of them.
+So you'll need to avoid being too general in the modifies clauses.
+
+Internally, QCheck-STM uses an extensible type to encode function's type
+signature. The plugin uses the type signature to automatically generate this
+encoding. But, in case you are using a type that is not yet encoded in this
+extensible type, Ortac/QCheck-STM will generate code using the not-yet-defined
+constructor using the implicit rule of capitalizing the name of the type. This
+will generate non-compiling code, but you'll then have the chance to add the
+new constructor by hand in the generated code.
+
+For example, looking at the following function along its specifications, the
+plugin will make the assumption that the  QCheck-STM `ty` is extended with a
+[New_type] constructor and a [new_type] functional combinator is defined.
+
+{@ocaml file=example_unknown_type.mli,part=fun-decl[
+val type_not_supported : new_type -> 'a t -> new_type
+(*@ y = type_not_supported x t *)
+]}
+
+{@sh[
+$ ortac qcheck-stm example_unknown_type.mli "make 42 'a'" "char t" -o foo.ml
+$ grep -A 1 "type cmd" foo.ml
+    type cmd =
+      | Type_not_supported of new_type
+$ grep -A 3 "let run" foo.ml
+    let run cmd__010_ sut__011_ =
+      match cmd__010_ with
+      | Type_not_supported x ->
+          Res (new_type, (type_not_supported x sut__011_))
+]}
+
+You can open the [foo.ml] file to edit it in this way.
+
+In Gospel, you have the possibility to use ghost values, as arguments and/or as
+returned values. As those values don’t exist in the actual code that will be
+called during the test, Ortac/QCheck-STM doesn't support Gospel specifications with
+ghost values in the header.
+
+If we add the following declaration to our example file,
+
+{@ocaml file=example_ghost.mli,part=fun-decl[
+val ghost_arg : char -> 'a t -> bool
+(*@ b = ghost_arg [ i : integer] c t *)
+]}
+
+the command will generate the following warning:
+
+{@sh[
+$ ortac qcheck-stm example_ghost.mli "make 42 'a'" "char t" -o foo.ml
+File "example_ghost.mli", line 14, characters 20-21:
+14 | (*@ b = ghost_arg [ i : integer] c t *)
+                         ^
+Warning: Skipping ghost_arg: functions with a ghost argument are not
+         supported.
+]}
+
+You'll need to write your specifications without using [ghost] arguments or
+returned value if you want to test this function with Ortac/QCheck-STM.
+
+Finally, when you want to test a library with a parameterized type, you need to
+instantiate the type parameter in order to generate the QCheck-STM tests.
+Choosing the right instantiation implies to be careful when the library
+contains specialized functions.
+
+For example, if we add the following declaration to our example file,
+
+{@ocaml file=example_incompatible_type.mli,part=fun-decl[
+val incompatible_type : char -> string t -> bool
+(*@ b = incompatible_type c t *)
+]}
+
+the plugin will generate a warning for this function and skip it.
+
+{@sh[
+$ ortac qcheck-stm example_incompatible_type.mli "make 42 'a'" "char t" -o foo.ml
+File "example_incompatible_type.mli", line 13, characters 32-40:
+13 | val incompatible_type : char -> string t -> bool
+                                     ^^^^^^^^
+Warning: Skipping incompatible_type: the type of its SUT-type argument is
+         incompatible with the configured SUT type: char t.
+]}
+
+In the case you have functions specialized with different instantiations, you
+can always generate one test per possible instantiation, of course.
+
+{2 [ortac] limitations}
+
+The second source of limitations is the [ocaml_of_gospel] translation provided
+by the [ortac-core] package. Gospel being a logical language, it is not fully
+executable. [ortac-core] identifies an executable subset of Gospel and
+translates it to OCaml. But there are still some limitations, in particular
+concerning quantification. For now, only well-bounded quantifications over
+integers are supported.
+
+If we add the following declaration to our example file,
+
+{@ocaml file=example_ill_formed_quantification.mli,part=fun-decl[
+val unsupported_quantification : 'a t -> bool
+(*@ b = unsupported_quantification t
+    ensures b = forall a. List.mem a t.contents -> a = a *)
+]}
+
+the command will generate the following warning:
+
+{@sh[
+$ ortac qcheck-stm example_ill_formed_quantification.mli "make 42 'a'" "char t" -o foo.ml
+File "example_ill_formed_quantification.mli", line 15, characters 16-56:
+15 |     ensures b = forall a. List.mem a t.contents -> a = a *)
+                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Warning: Skipping clause: unsupported quantification.
+]}
+
+Note that only the clause involving the unsupported quantification has not been
+translated. If your function's specification contains other clauses that can be
+translated and contain enough information for the plugin to do its job, then
+you will be able to test your function. If not, maybe you can rewrite the
+clause without involving this sort of quantification. In this particular
+example, you can use the [List.for_all] combinator from the Gospel standard
+library [List] module:
+
+{@ocaml file=example_for_all.mli,part=fun-decl[
+val for_all : 'a t -> bool
+(*@ b = for_all t
+    ensures b = List.for_all (fun x -> x = x) t.contents *)
+]}
+
+{2 Other limitations}
+
+Finally, note that this tool is still fairly new and comes with limitations
+that should be lifted in the future. Fow now, we only support testing functions
+with exactly one [SUT] argument in its signature, we don't support tuples and
+we only support first-order functions.
+
+If we add the following declarations to our example file,
+
+{@ocaml file=example_limitations.mli,part=fun-decl[
+val f : int -> int -> bool
+(*@ b = f x y *)
+
+val compare : 'a t -> 'a t -> bool
+(*@ b = compare t1 t2 *)
+
+val of_list : 'a list -> 'a t
+(*@ t = of_list xs *)
+
+val g : int * int -> 'a t -> bool
+(*@ b = g x t *)
+
+val h : 'a t -> 'a * 'a
+(*@ (l, r) = h t *)
+
+val for_all : ('a -> bool) -> 'a t -> bool
+(*@ b = for_all p t *)
+]}
+
+Ortac/QCheck-STM will generate the following warnings:
+
+{@sh[
+$ ortac qcheck-stm example_limitations.mli "make 42 'a'" "char t" -o foo.ml
+File "example_limitations.mli", line 13, characters 8-26:
+13 | val f : int -> int -> bool
+             ^^^^^^^^^^^^^^^^^^
+Warning: Skipping f: functions with no SUT argument cannot be tested.
+File "example_limitations.mli", line 16, characters 14-34:
+16 | val compare : 'a t -> 'a t -> bool
+                   ^^^^^^^^^^^^^^^^^^^^
+Warning: Skipping compare: functions with multiple SUT arguments cannot be
+         tested.
+File "example_limitations.mli", line 19, characters 25-29:
+19 | val of_list : 'a list -> 'a t
+                              ^^^^
+Warning: Skipping of_list: functions returning a SUT value cannot be tested.
+File "example_limitations.mli", line 25, characters 16-23:
+25 | val h : 'a t -> 'a * 'a
+                     ^^^^^^^
+Warning: Skipping h: functions returning tuples are not supported yet.
+File "example_limitations.mli", line 28, characters 15-25:
+28 | val for_all : ('a -> bool) -> 'a t -> bool
+                    ^^^^^^^^^^
+Warning: Skipping for_all: functions are not supported yet as arguments.
+File "example_limitations.mli", line 22, characters 8-17:
+22 | val g : int * int -> 'a t -> bool
+             ^^^^^^^^^
+Warning: Type (int * int) not supported.
+]}