diff --git a/src/AIMOS.ml b/src/aimos.ml
similarity index 100%
rename from src/AIMOS.ml
rename to src/aimos.ml
diff --git a/src/AIMOS.mli b/src/aimos.mli
similarity index 100%
rename from src/AIMOS.mli
rename to src/aimos.mli
diff --git a/src/JSON.ml b/src/json.ml
similarity index 100%
rename from src/JSON.ml
rename to src/json.ml
diff --git a/src/JSON.mli b/src/json.mli
similarity index 100%
rename from src/JSON.mli
rename to src/json.mli
diff --git a/src/main.ml b/src/main.ml
index b060e14aecd8ca5825cecd0f78856efc397e8c51..e59de66665051c381e87c0b7a40428e5c7ac416f 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -159,9 +159,9 @@ let record_json_output id prover_answer dataset_results file =
     let total = Float.of_int (List.length dataset_results) in
     nb_valid /. total *. 100.
   in
-  let output = { JSON.id; prover_answer; percentage_valid; dataset_results } in
+  let output = { Json.id; prover_answer; percentage_valid; dataset_results } in
   let out_channel = Stdlib.open_out file in
-  Yojson.Safe.to_channel out_channel (JSON.output_to_yojson output);
+  Yojson.Safe.to_channel out_channel (Json.output_to_yojson output);
   Logs.info (fun m -> m "@[Results recorded in file '%s'@]" file);
   Stdlib.close_out out_channel
 
@@ -175,7 +175,7 @@ let record_verification_result id verification_result file =
     verification_result
 
 let verify_json ?memlimit ?timelimit ?outfile json =
-  let jin = JSON.input_of_string json in
+  let jin = Json.input_of_string json in
   let memlimit =
     (* Precedence to the command line option, if any. *)
     match memlimit with
diff --git a/src/SAVer.ml b/src/saver.ml
similarity index 100%
rename from src/SAVer.ml
rename to src/saver.ml
diff --git a/src/SAVer.mli b/src/saver.mli
similarity index 100%
rename from src/SAVer.mli
rename to src/saver.mli
diff --git a/src/verification.ml b/src/verification.ml
index 2d806e90e8e6bcc6e029d610e7616b487e2b9053..f02325fce7629d6b81f7974d02a6c05623096b34 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -28,10 +28,10 @@ module File = struct
   type t =
     | Stdin
     | File of string
-    | JSON of JSON.input
+    | JSON of Json.input
 
   let of_json_input jin =
-    if Caml.Sys.file_exists jin.JSON.model
+    if Caml.Sys.file_exists jin.Json.model
     then
       if Caml.Sys.file_exists jin.property.dataset
       then
@@ -54,7 +54,7 @@ module File = struct
   let pretty fmt = function
     | Stdin -> Fmt.string fmt "-"
     | File f -> Fmt.string fmt f
-    | JSON jin -> JSON.pretty_input fmt jin
+    | JSON jin -> Json.pretty_input fmt jin
 end
 
 type verification_result = answer list Wstdlib.Mstr.t
@@ -112,7 +112,7 @@ let answer_saver limit config env config_prover dataset task =
     in
     Dataset.interpret_predicate env ~on_model ~on_dataset task
   in
-  let answer = SAVer.call_prover limit config config_prover dataset_predicate in
+  let answer = Saver.call_prover limit config config_prover dataset_predicate in
   match answer.prover_answer with
   | Call_provers.Unknown "" ->
     let additional_info = Fmt.str "%d/%d" answer.nb_proved answer.nb_total in
@@ -145,7 +145,7 @@ let answer_aimos limit config env config_prover dataset task =
     in
     Dataset.interpret_predicate env ~on_model ~on_dataset task
   in
-  let answer = AIMOS.call_prover limit config config_prover predicate in
+  let answer = Aimos.call_prover limit config config_prover predicate in
   let additional_info = Generic None in
   (answer, additional_info)
 
@@ -273,7 +273,7 @@ let open_file ?(debug = false) ?format ~loadpath file =
       let mlw_files, _ = Env.(read_file ?format base_language env file) in
       mlw_files
     | JSON jin ->
-      let th = JSON.theory_of_input env jin in
+      let th = Json.theory_of_input env jin in
       Wstdlib.Mstr.singleton th.th_name.id_string th
   in
   (env, config, mstr_theory)
diff --git a/src/verification.mli b/src/verification.mli
index 95ebc1649cc095c1fbc245b405729a751a55fb73..82a575f331515156abf0d1a7e3445557ce42c6fc 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -26,9 +26,9 @@ module File : sig
   type t = private
     | Stdin
     | File of string
-    | JSON of JSON.input
+    | JSON of Json.input
 
-  val of_json_input : JSON.input -> (t, string) result
+  val of_json_input : Json.input -> (t, string) result
   val of_string : string -> (t, string) result
   val pretty : Format.formatter -> t -> unit
 end