diff --git a/.ocamlformat b/.ocamlformat
index 7523471a153000d1fd87a948aa5f33b4a63dacab..b883181edadd567d23d0f89fc479c33bdc6e4e3e 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -3,3 +3,4 @@ exp-grouping=parens
 if-then-else=keyword-first
 max-indent=2
 wrap-comments=true
+parse-docstrings=true
diff --git a/src/autodetection.mli b/src/autodetection.mli
new file mode 100644
index 0000000000000000000000000000000000000000..42842afef2bfe1c9d74610dbf3e45bd2dc0ab3e2
--- /dev/null
+++ b/src/autodetection.mli
@@ -0,0 +1,10 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+val autodetect : debug:bool -> unit -> Why3.Whyconf.config
+(** Perform the autodetection of provers.
+
+    @param debug activates debug information. *)
diff --git a/src/verification.mli b/src/verification.mli
new file mode 100644
index 0000000000000000000000000000000000000000..95432d0952df6c2e820e53e62ddc68acc87f9310
--- /dev/null
+++ b/src/verification.mli
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+val verify :
+  string option ->
+  string list ->
+  ?memlimit:int ->
+  prover:string ->
+  string ->
+  unit
+(** [verify format loadpath memlimit prover file] launches a verification of the
+    given [file] with the provided [prover].
+
+    @param format is the [file] format.
+    @param loadpath is the additional loadpath.
+    @param memlimit
+      is the memory limit (in megabytes) granted to the verification. *)