diff --git a/src/main.ml b/src/main.ml
index 9c37d26c125ddc8757b958d7199fdad3dd906095..c59b9740df57988f8f391843a1640aab3441af4f 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -120,7 +120,7 @@ let timelimit_of_string s =
   | [ v ], [ "h" ] -> Int.of_string v * 3600
   | _ -> invalid_arg "Unrecognized time limit"
 
-let verify ?format loadpath ?memlimit ?timelimit prover ?dataset_csv files =
+let verify ?format ~loadpath ?memlimit ?timelimit prover ?dataset_csv files =
   let debug = log_level_is_debug () in
   let memlimit = Option.map memlimit ~f:memlimit_of_string in
   let timelimit = Option.map timelimit ~f:timelimit_of_string in
@@ -130,12 +130,12 @@ let verify ?format loadpath ?memlimit ?timelimit prover ?dataset_csv files =
          ?dataset_csv)
     files
 
-let verify_json loadpath ?memlimit ?timelimit file =
+let verify_json ?memlimit ?timelimit file =
   let jc = Result.ok_exn (Verification.JSON.of_string file) in
   let prover = jc.Verification.JSON.prover in
   let dataset_csv = jc.Verification.JSON.property.dataset in
   let file = Result.ok_or_failwith (Verification.File.of_json_config jc) in
-  verify loadpath ?memlimit ?timelimit prover ~dataset_csv [ file ]
+  verify ~loadpath:[] ?memlimit ?timelimit prover ~dataset_csv [ file ]
 
 let exec_cmd cmdname cmd =
   Logs.debug (fun m -> m "Command `%s'" cmdname);
@@ -190,10 +190,6 @@ let timelimit =
   Arg.(
     value & opt (some string) None & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
 
-let loadpath =
-  let doc = "Additional loadpath." in
-  Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
-
 let verify_cmd =
   let cmdname = "verify" in
   let info =
@@ -202,6 +198,10 @@ let verify_cmd =
       ~doc
       ~man:[ `S Manpage.s_description; `P doc ]
   in
+  let loadpath =
+    let doc = "Additional loadpath." in
+    Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
+  in
   let format =
     let doc = "File format." in
     Arg.(value & opt (some string) None & info [ "format" ] ~doc)
@@ -233,7 +233,8 @@ let verify_cmd =
       const
         (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
         exec_cmd cmdname (fun () ->
-          verify ?format loadpath ?memlimit ?timelimit prover ?dataset_csv files))
+          verify ?format ~loadpath ?memlimit ?timelimit prover ?dataset_csv
+            files))
       $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv $ files
       $ setup_logs)
   in
@@ -257,10 +258,9 @@ let verify_json_cmd =
         required & pos ~rev:true 0 (some file) None & info [] ~doc ~docv:"FILE")
     in
     Term.(
-      const (fun loadpath memlimit timelimit json _ ->
-        exec_cmd cmdname (fun () ->
-          verify_json loadpath ?memlimit ?timelimit json))
-      $ loadpath $ memlimit $ timelimit $ json $ setup_logs)
+      const (fun memlimit timelimit json _ ->
+        exec_cmd cmdname (fun () -> verify_json ?memlimit ?timelimit json))
+      $ memlimit $ timelimit $ json $ setup_logs)
   in
   Cmd.v info term