diff --git a/.ocamlformat b/.ocamlformat
index a28746123cf756ec8868b9bbc35f8f1281da2563..7523471a153000d1fd87a948aa5f33b4a63dacab 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,5 +1,5 @@
 version=0.19.0
-exp-grouping=preserve
+exp-grouping=parens
 if-then-else=keyword-first
 max-indent=2
 wrap-comments=true
diff --git a/src/language.mli b/src/language.mli
index 23ef26ce41c38fd194c55736af8953ab786b1a90..f1812f1d3e175236b0ffaa112cf1eeb77088284b 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -1,3 +1,9 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
 type nnet = {
   nb_inputs : int;
   nb_outputs : int;
@@ -6,7 +12,7 @@ type nnet = {
 }
 
 val lookup_loaded_nnets : Why3.Term.lsymbol -> nnet option
-(** Return the filename of an nnets Why3 representation *)
+(** @return the filename of an nnets Why3 representation. *)
 
 val register_nnet_support : unit -> unit
-(** register nnet parser *)
+(** Register nnet parser. *)
diff --git a/src/main.ml b/src/main.ml
index 5e07bf7e8eae3065ea3935259f72ebd8054f9863..8d5bdaf6e8a2d530a59fe3a0f3404e081332c06b 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -6,7 +6,6 @@
 
 open Base
 open Cmdliner
-module Format = Caml.Format
 
 let caisar = "caisar"
 
@@ -45,7 +44,7 @@ let setup_logs =
 
 let config detect () =
   if detect
-  then begin
+  then (
     Logs.debug (fun m -> m "Automatic detection.");
     let config =
       let debug = match Logs.level () with Some Debug -> true | _ -> false in
@@ -57,8 +56,7 @@ let config detect () =
       m "@[<v>%a@]"
         (Pp.print_iter2 Whyconf.Mprover.iter Pp.newline Pp.nothing
            Whyconf.print_prover Pp.nothing)
-        provers)
-  end
+        provers))
 
 let verify format loadpath prover files =
   List.iter ~f:(Verification.verify format loadpath prover) files
@@ -83,17 +81,16 @@ let config_cmd =
   in
   let detect =
     let doc =
-      Format.sprintf "Detect solvers in \\$PATH (or \\$%s, if specified)."
-        dirvar
+      Fmt.str "Detect solvers in \\$PATH (or \\$%s, if specified)." dirvar
     in
     Arg.(value & flag & info [ "d"; "detect" ] ~doc)
   in
-  let doc = Format.sprintf "%s configuration." caisar in
+  let doc = Fmt.str "%s configuration." caisar in
   let exits = Term.default_exits in
   let man =
     [
       `S Manpage.s_description;
-      `P (Format.sprintf "Handle the configuration of %s." caisar);
+      `P (Fmt.str "Handle the configuration of %s." caisar);
     ]
   in
   ( Term.(
diff --git a/src/transformations.ml b/src/transformations.ml
index e8ceeb81866b1c2ce7fe30d0a1917e5f3dd048f1..762bd9d674ca257d90508c58d4c4f4d2246d476d 100644
--- a/src/transformations.ml
+++ b/src/transformations.ml
@@ -1,15 +1,21 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
 open Base
 
 let meta_input =
   Why3.Theory.(
     register_meta "caisar_input"
-      ~desc:"Indicate the position of the input in the neural network"
+      ~desc:"Indicates the position of the input in the neural network"
       [ MTlsymbol; MTint ])
 
 let meta_output =
   Why3.Theory.(
     register_meta "caisar_output"
-      ~desc:"Indicate the position of the output in the neural network"
+      ~desc:"Indicates the position of the output in the neural network"
       [ MTlsymbol; MTint ])
 
 let get_input_variables =
@@ -96,8 +102,8 @@ let simplify_goal env input_variables =
 let caisar_native_prover env =
   Why3.Trans.seq
     [
-      Why3.Trans.bind get_input_variables (simplify_goal env);
-      (* Why3.Simplify_formula.simplify_; *)
+      Why3.Trans.bind get_input_variables (simplify_goal env)
+      (* Why3.Simplify_formula.simplify_; *);
     ]
 
 let init () =
diff --git a/src/transformations.mli b/src/transformations.mli
index 1d3779c269fa019d0f01e8b827d7ce09dbf7567a..0df41287e55f0f129b1160b22da6b0096c6e0cc3 100644
--- a/src/transformations.mli
+++ b/src/transformations.mli
@@ -1,2 +1,8 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
 val init : unit -> unit
-(** register the transformations *)
+(** Register the transformations. *)
diff --git a/src/verification.ml b/src/verification.ml
index 624acb456644a7e87f214636bd4114dda8837696..02f14d60e3a8dda70cc368d3fb89ca31e16cf76d 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -5,7 +5,6 @@
 (**************************************************************************)
 
 open Base
-module Format = Caml.Format
 module Filename = Caml.Filename
 
 let () = Language.register_nnet_support ()
@@ -46,5 +45,5 @@ let verify format loadpath prover file =
           in
           Driver.load_driver_absolute env file prover.extra_drivers
       in
-      List.iter tasks ~f:(Format.printf "%a" (Driver.print_task driver)))
+      List.iter tasks ~f:(Fmt.pr "%a" (Driver.print_task driver)))
     mstr_theory