diff --git a/src/params.ml b/src/params.ml
index 5ad2fbbd..0894bdea 100644
--- a/src/params.ml
+++ b/src/params.ml
@@ -102,7 +102,7 @@ type exec = executable ref
 let path_prefix =
   sprintf "PATH='%s';" Paths.backend_path_string
 
-let get_exec e =
+let get_exec err e =
   match !e with
   | Unchecked (exec, cmd, vers) ->
     (*
@@ -131,7 +131,7 @@ let get_exec e =
           else "."
         in
         let msg = msg1 ^ msg2 in
-        eprintf "%s" msg;
+        Format.fprintf err "%s" msg;
         e := NotFound msg;
         failwith msg;
      end;
@@ -450,14 +450,14 @@ let stats        = ref false
 
 let solve_cmd cmd file =
   if Sys.os_type = "Cygwin" then
-    sprintf "file=%s; winfile=\"`cygpath -a -w \"%s\"`\"; %s" file file (get_exec cmd)
+    sprintf "file=%s; winfile=\"`cygpath -a -w \"%s\"`\"; %s" file file (get_exec Format.err_formatter cmd)
   else
-    sprintf "file=%s; %s" file (get_exec cmd)
+    sprintf "file=%s; %s" file (get_exec Format.err_formatter cmd)
 
 
-let external_tool_config force (name, tool) =
+let external_tool_config (err : Format.formatter) force (name, tool) =
   if force then begin
-    try ignore (get_exec tool) with Failure _ -> ()
+    try ignore (get_exec err tool) with Failure _ -> ()
   end;
   match !tool with
   | Checked (cmd, []) ->
@@ -470,7 +470,7 @@ let external_tool_config force (name, tool) =
   | _ -> []
 
 
-let configuration toolbox force =
+let configuration err toolbox force =
   let library_path = (match stdlib_path with
   | Some path -> "\"" ^ (String.escaped path) ^ "\"";
   | None -> "N/A")
@@ -494,7 +494,7 @@ let configuration toolbox force =
           first_line :: mid_lines @ [last_line]
         end
       end
-    @ List.flatten (List.map (external_tool_config force)
+    @ List.flatten (List.map (external_tool_config err force)
                              [("Isabelle", isabelle);
                               ("zenon", zenon);
                               ("CVC4", cvc4);
@@ -517,17 +517,17 @@ let configuration toolbox force =
   header @ lines @ footer
 
 
-let printconfig force =
-  String.concat "\n" (configuration false force)
+let printconfig err force =
+  String.concat "\n" (configuration err false force)
 
 let print_config_toolbox force =
-  String.concat "\n" (configuration true force)
+  String.concat "\n" (configuration Format.err_formatter true force)
 
 
 let zenon_version = ref None
 
 let check_zenon_ver () =
-  let zen = get_exec zenon in
+  let zen = get_exec Format.err_formatter zenon in
   match get_version zenon with
   | [] -> ()
   | ret :: _ ->
@@ -543,7 +543,7 @@ let get_zenon_verfp () = if !zenon_version = None then check_zenon_ver ();
 let isabelle_version = ref None
 
 let check_isabelle_ver () =
-  (try ignore (get_exec isabelle) with Failure _ -> ());
+  (try ignore (get_exec Format.err_formatter isabelle) with Failure _ -> ());
   match get_version isabelle with
   | [] -> ()
   | ret :: _ ->
diff --git a/src/params.mli b/src/params.mli
index 52592cd3..adf1ed3e 100644
--- a/src/params.mli
+++ b/src/params.mli
@@ -66,7 +66,7 @@ val safefp: bool ref
 val fp_deb: bool ref
 
 (* util/util.ml *)
-val configuration: bool -> bool -> string list
+val configuration: Format.formatter -> bool -> bool -> string list
 
 (* module/save.ml *)
 val stdlib_search_paths : string list
@@ -97,7 +97,7 @@ val suppress_all: bool ref
 val set_smt_logic: string -> unit
 val set_smt_solver: string -> unit
 val set_tlapm_cache_dir: string -> unit
-val printconfig: bool -> string
+val printconfig: Format.formatter -> bool -> string
 val print_config_toolbox: bool -> string
 val check_zenon_ver: unit -> unit
 val fpf_out: string option ref
diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml
index 48c8599d..63acc4a5 100644
--- a/src/tlapm_args.ml
+++ b/src/tlapm_args.ml
@@ -6,11 +6,9 @@ open Ext
 open Params
 
 
-let show_config = ref false
-let show_version () =
-  print_endline (rawversion ()) ;
-  exit 0
-
+let show_version formatter terminate =
+  Format.fprintf formatter "%s\n" (rawversion ());
+  terminate 0
 
 let set_debug_flags flgs =
   let flgs = Ext.split flgs ',' in
@@ -52,24 +50,23 @@ let set_default_method meth =
   with Failure msg -> raise (Arg.Bad ("--method: " ^ msg))
 
 
-(* FIXME use Arg.parse instead *)
-let parse_args args opts mods usage_fmt =
+let parse_args executable_name args opts mods usage_fmt err terminate =
   try
-    Arg.parse_argv (Array.of_list args) opts (fun mfile -> mods := mfile :: !mods)
-      (Printf.sprintf usage_fmt (Filename.basename Sys.executable_name))
+    Arg.current := 0;
+    Arg.parse_argv args opts (fun mfile -> mods := mfile :: !mods)
+      (Printf.sprintf usage_fmt (Filename.basename executable_name))
   with Arg.Bad msg ->
-    print_endline msg ;
-    flush stdout ;
-    exit 2
+    Format.fprintf err "%s\n" msg;
+    terminate 2
 
-let show_where () =
+let show_where out terminate =
   match stdlib_path with
   | Some path  ->
-    Printf.printf "%s\n" path;
-    exit 0
+    Format.fprintf out "%s\n" path;
+    terminate 0
   | None ->
-    Printf.printf "N/A\n";
-    exit 1
+    Format.fprintf out "N/A\n";
+    terminate 1
 
 let set_nofp_start s =
   nofp_sl := s
@@ -134,7 +131,8 @@ let quote_if_needed s =
   end
 
 
-let init () =
+let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exit) (executable_name : string) (args : string array) =
+  let show_config = ref false in
   let mods = ref [] in
   let helpfn = ref (fun () -> ()) in
   let show_help () = !helpfn () in
@@ -147,11 +145,11 @@ let init () =
     blank;
     "--help", Arg.Unit show_help, " show this help message and exit" ;
     "-help", Arg.Unit show_help, " (same as --help)" ;
-    "--version", Arg.Unit show_version, " show version number and exit" ;
+    "--version", Arg.Unit (fun () -> show_version out terminate), " show version number and exit" ;
     "--verbose", Arg.Set verbose, " produce verbose messages" ;
     "-v", Arg.Set verbose, " (same as --verbose)" ;
     blank;
-    "--where", Arg.Unit show_where,
+    "--where", Arg.Unit (fun () -> show_where out terminate),
                " show location of standard library and exit" ;
     "--config", Arg.Set show_config, " show configuration and exit" ;
     "--summary", Arg.Set summary,
@@ -245,23 +243,23 @@ let init () =
     format_of_string "Usage: %s <options> FILE ...\noptions are:"
   in
   helpfn := begin fun () ->
-    Arg.usage opts
-      (Printf.sprintf usage_fmt (Filename.basename Sys.executable_name)) ;
-    exit 0
+    Arg.usage_string opts
+      (Printf.sprintf usage_fmt (Filename.basename executable_name))
+      |> Format.fprintf err "%s";
+    terminate 0
   end ;
-  let args = Array.to_list Sys.argv in
-  parse_args args opts mods usage_fmt ;
+  parse_args executable_name args opts mods usage_fmt err terminate;
   if !show_config || !verbose then begin
-    print_endline (printconfig true) ;
-    flush stdout
+    Format.fprintf out "%s\n" (printconfig err true);
   end ;
-  if !show_config then exit 0 ;
+  if !show_config then terminate 0 ;
   if !mods = [] then begin
-    Arg.usage opts
+    Arg.usage_string opts
       (Printf.sprintf "Need at least one module file.\n\n\
                        Usage: %s <options> FILE ...\noptions are:"
-         (Filename.basename Sys.executable_name)) ;
-    exit 2
+         (Filename.basename executable_name))
+         |> Format.fprintf err "%s";
+    terminate 2
   end ;
   if !summary then begin
     suppress_all := true ;
@@ -269,20 +267,20 @@ let init () =
   end ;
   check_zenon_ver () ;
   if !Params.toolbox then begin
-    Printf.printf "\n\\* TLAPM version %s\n"
+    Format.fprintf out "\n\\* TLAPM version %s\n"
                   (Params.rawversion ());
     let tm = Unix.localtime (Unix.gettimeofday ()) in
-    Printf.printf "\\* launched at %04d-%02d-%02d %02d:%02d:%02d"
+    Format.fprintf out "\\* launched at %04d-%02d-%02d %02d:%02d:%02d"
                   (tm.Unix.tm_year + 1900) (tm.Unix.tm_mon + 1) tm.Unix.tm_mday
                   tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec;
-    Printf.printf " with command line:\n\\*";
-    Array.iter (fun s -> Printf.printf " %s" (quote_if_needed s)) Sys.argv;
-    Printf.printf "\n\n%!"
+    Format.fprintf out " with command line:\n\\*";
+    Array.iter (fun s -> Format.fprintf out " %s" (quote_if_needed s)) args;
+    Format.fprintf out "\n\n%!"
   end;
   if !use_stdin && (List.length !mods) <> 1 then begin
     Arg.usage opts
       "Exactly 1 module has to be specified if TLAPM is invoked with\
        the --stdin option." ;
-    exit 2
+    terminate 2
   end;
   !mods
diff --git a/src/tlapm_args.mli b/src/tlapm_args.mli
index 550a04f0..02add406 100644
--- a/src/tlapm_args.mli
+++ b/src/tlapm_args.mli
@@ -2,4 +2,11 @@
 
 Copyright (C) 2011  INRIA and Microsoft Corporation
 *)
-val init: unit -> string list
+
+(** Given the executable name and an array of command-line arguments, parses
+    those arguments then either sets associated values in the Params module
+    or directly takes action such as printing out file contents or deleting
+    directories. Returns a list of files for proof checking. The optional
+    arguments are used for unit tests.
+*)
+val init: ?out:Format.formatter -> ?err:Format.formatter -> ?terminate:(int -> unit) -> string -> string array -> string list
diff --git a/src/tlapm_lib.ml b/src/tlapm_lib.ml
index a328d9ae..4bd57a16 100644
--- a/src/tlapm_lib.ml
+++ b/src/tlapm_lib.ml
@@ -586,9 +586,9 @@ let init () =
   Printexc.record_backtrace true;
   Format.pp_set_max_indent Format.err_formatter 35;
   if Params.debugging "main" then
-    main (Tlapm_args.init ())
+    main (Tlapm_args.init Sys.executable_name Sys.argv)
   else
-    try main (Tlapm_args.init ()) with
+    try main (Tlapm_args.init Sys.executable_name Sys.argv) with
     | Errors.Fatal ->
        Util.eprintf "tlapm: Exiting because of the above error.";
        exit 0;
diff --git a/src/util/util.ml b/src/util/util.ml
index 6f7096bf..b91c13ab 100644
--- a/src/util/util.ml
+++ b/src/util/util.ml
@@ -117,7 +117,7 @@ let bug ?at msg =
       "Please file a bug report, including as much information" ;
       "as you can. Mention the following in your report: " ;
       "" ]
-      @ Params.configuration false false
+      @ Params.configuration Format.err_formatter false false
     in
     String.concat "\n" lines ^ "\n"
   in
diff --git a/test/cli/cli_tests.ml b/test/cli/cli_tests.ml
new file mode 100644
index 00000000..e33601e2
--- /dev/null
+++ b/test/cli/cli_tests.ml
@@ -0,0 +1,602 @@
+(** Unit tests to ensure CLI parameter format does not change.
+*)
+
+type setting_value = [
+  `B of string * bool ref * bool
+  | `I of string * int ref * int
+  | `F of string * float ref * float
+  | `S of string * string ref * string
+  | `SO of string * string option ref * string option
+  | `SL of string * string list ref * string list
+  | `ML of string * Tlapm_lib__Method.t list ref * Tlapm_lib__Method.t list
+]
+
+let capture_output (f : Format.formatter -> unit) : string =
+  let out = Buffer.create 0 in
+  let out_format = Format.formatter_of_buffer out in
+  f out_format;
+  Format.pp_print_flush out_format ();
+  Buffer.contents out
+
+(** This function is a quick hack that is very inefficient; avoid using
+    it on large haystacks.
+*)
+let rec string_contains (needle : string) (haystack : string) : bool =
+  match haystack with
+  | "" -> false
+  | _ -> String.starts_with ~prefix:needle haystack ||
+    String.sub haystack 1 ((String.length haystack) - 1) |>
+    string_contains needle
+
+let str_ls_as_str (ls : string list) : string =
+  "[" ^ (String.concat "; " ls) ^ "]"
+
+let display_setting_value (v : setting_value) : string =
+  match v with
+  | `B (n, rf, v) -> Printf.sprintf "%s: %b [%b]" n v !rf
+  | `I (n, rf, v) -> Printf.sprintf "%s: %d [%d]" n v !rf
+  | `F (n, rf, v) -> Printf.sprintf "%s: %f [%f]" n v !rf
+  | `S (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n v !rf
+  | `SO (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (Option.value ~default:"None" v) (Option.value ~default:"None" !rf)
+  | `SL (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (str_ls_as_str v) (str_ls_as_str !rf)
+  | `ML (n, rf, v) -> Printf.sprintf "%s: %s [%s]" n (str_ls_as_str (List.map (fun m -> capture_output (fun f -> Tlapm_lib__Method.pp_print_tactic f m)) v)) (str_ls_as_str (List.map (fun m -> capture_output (fun f -> Tlapm_lib__Method.pp_print_tactic f m)) !rf))
+
+let print_string_diff (formatter : Format.formatter) ((expected, actual) : string * string) : unit =
+  Printf.sprintf "exp/act: (%s)/(%s)" expected actual |> Format.pp_print_text formatter
+
+let rec print_list_diff (formatter : Format.formatter) (expected : 'a list) (actual : 'a list) (as_string : 'a -> string) : unit =
+  match expected, actual with
+  | [], [] -> ()
+  | ex :: ex_tl, [] ->
+      ex |> as_string |> Printf.sprintf "+exp: %s" |> Format.pp_print_text formatter;
+      print_list_diff formatter ex_tl [] as_string;
+  | [], ac :: ac_tl ->
+      ac |> as_string |> Printf.sprintf "+act: %s" |> Format.pp_print_text formatter;
+      print_list_diff formatter ac_tl [] as_string;
+  | ex :: ex_tl, ac :: ac_tl ->
+      if not (ex = ac) then print_string_diff formatter (as_string ex, as_string ac);
+      print_list_diff formatter ex_tl ac_tl as_string
+
+let print_setting_list_diff (formatter : Format.formatter) ((expected, actual) : setting_value list * setting_value list) : unit =
+  print_list_diff formatter expected actual display_setting_value
+
+let print_mod_diff (formatter : Format.formatter) ((expected, actual) : string list * string list) : unit =
+  print_list_diff formatter expected actual (fun s -> s)
+
+let setting_value_changed (setting : setting_value) =
+  match setting with
+  | `B (_, rf, v) -> not (!rf = v)
+  | `I (_, rf, v) -> not (!rf = v)
+  | `F (_, rf, v) -> not (!rf = v)
+  | `S (_, rf, v) -> not (!rf = v)
+  | `SO (_, rf, v) -> not (!rf = v)
+  | `SL (_, rf, v) -> not (!rf = v)
+  | `ML (_, rf, v) -> not (!rf = v)
+
+let changed_setting_value (setting : setting_value) =
+  if setting_value_changed setting then
+    match setting with
+    | `B (n, rf, _) -> Some (`B (n, rf, !rf))
+    | `I (n, rf, _) -> Some (`I (n, rf, !rf))
+    | `F (n, rf, _) -> Some (`F (n, rf, !rf))
+    | `S (n, rf, _) -> Some (`S (n, rf, !rf))
+    | `SO (n, rf, _) -> Some (`SO (n, rf, !rf))
+    | `SL (n, rf, _) -> Some (`SL (n, rf, !rf))
+    | `ML (n, rf, _) -> Some (`ML (n, rf, !rf))
+  else None
+
+let set_setting_value (setting : setting_value) =
+  match setting with
+  | `B (_, rf, v) -> rf := v
+  | `I (_, rf, v) -> rf := v
+  | `F (_, rf, v) -> rf := v
+  | `S (_, rf, v) -> rf := v
+  | `SO (_, rf, v) -> rf := v
+  | `SL (_, rf, v) -> rf := v
+  | `ML (_, rf, v) -> rf := v
+
+open Tlapm_lib__Params;;
+
+let setting_values () : setting_value list = [
+  `B ("toolbox", toolbox, !toolbox);
+  `I ("toolbox_vsn", toolbox_vsn, !toolbox_vsn);
+  `B ("use_stdin", use_stdin, !use_stdin);
+  `B ("prefer_stdlib", prefer_stdlib, !prefer_stdlib);
+  `B ("notl", notl, !notl);
+  `B ("verbose", verbose, !verbose);
+  `B ("check", check, !check);
+  `S ("output_dir", output_dir, !output_dir);
+  `I ("wait", wait, !wait);
+  `B ("no_fp", no_fp, !no_fp);
+  `I ("nofp_sl", nofp_sl, !nofp_sl);
+  `I ("nofp_el", nofp_el, !nofp_el);
+  `B ("printallobs", printallobs, !printallobs);
+  `B ("pr_normal", pr_normal, !pr_normal);
+  `B ("ob_flatten", ob_flatten, !ob_flatten);
+  `B ("noproving", noproving, !noproving);
+  `S ("fp_hist_dir", fp_hist_dir, !fp_hist_dir);
+  `I ("fp_original_number", fp_original_number, !fp_original_number);
+  `B ("safefp", safefp, !safefp);
+  `B ("fp_deb", fp_deb, !fp_deb);
+  `B ("use_xtla", use_xtla, !use_xtla);
+  `B ("xtla", xtla, !xtla);
+  `I ("tb_sl", tb_sl, !tb_sl);
+  `I ("tb_el", tb_el, !tb_el);
+  `I ("max_threads", max_threads, !max_threads);
+  `B ("cleanfp", cleanfp, !cleanfp);
+  `SO ("fpf_in", fpf_in, !fpf_in);
+  `SO ("fpf_out", fpf_out, !fpf_out);
+  `B ("fp_loaded", fp_loaded, !fp_loaded);
+  `B ("summary", summary, !summary);
+  `B ("stats", stats, !stats);
+  `B ("keep_going", keep_going, !keep_going);
+  `B ("suppress_all", suppress_all, !suppress_all);
+  `F ("timeout_stretch", timeout_stretch, !timeout_stretch);
+  `F ("backend_timeout", backend_timeout, !backend_timeout);
+  `SL ("rev_search_path", rev_search_path, !rev_search_path);
+  `ML ("default_method", default_method, !default_method);
+  `S ("smt_logic", smt_logic, !smt_logic);
+  `S ("cachedir", cachedir, !cachedir);
+]
+
+let default_setting_values = setting_values ()
+
+let reset_setting_values () = List.iter set_setting_value default_setting_values
+
+let changed_setting_values () = List.filter_map changed_setting_value default_setting_values
+
+let parse_args (args : string list) : string list * string * string * int option =
+  let out = Buffer.create 0 in
+  let out_format = Format.formatter_of_buffer out in
+  let err = Buffer.create 0 in
+  let err_format = Format.formatter_of_buffer err in
+  let exception TrappedExit of int in
+  let terminate (code : int) = raise (TrappedExit code) in
+  try let mods = Tlapm_lib__Tlapm_args.init ~out:out_format ~err:err_format ~terminate:terminate "tlapm" (Array.of_list ("tlapm" :: args)) in
+    Format.pp_print_flush out_format ();
+    Format.pp_print_flush err_format ();
+    (mods, Buffer.contents out, Buffer.contents err, None)
+  with TrappedExit exit_code ->
+    Format.pp_print_flush out_format ();
+    Format.pp_print_flush err_format ();
+    ([], Buffer.contents out, Buffer.contents err, Some exit_code)
+
+open OUnit2;;
+
+let test_help _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--help"] in
+  assert_equal [] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_bool "Should print help text" (String.starts_with err ~prefix:"Usage: tlapm <options> FILE");
+  assert_equal (Some 0) exit_code;
+  let (mods, out, err, exit_code) = parse_args ["-help"] in
+  assert_equal [] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_bool "Should print help text" (String.starts_with err ~prefix:"Usage: tlapm <options> FILE");
+  assert_equal (Some 0) exit_code;
+  assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_version _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--version"] in
+  assert_equal [] mods ~pp_diff:print_mod_diff;
+  assert_equal (rawversion () ^ "\n") out;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal (Some 0) exit_code;
+  assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_basic _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_no_mods _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args [] in
+  assert_equal [] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_bool "Need module req message" (String.starts_with err ~prefix:"Need at least one module file");
+  assert_equal (Some 2) exit_code;
+  assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_verbose _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["-v"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------");
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;;
+  reset_setting_values ();
+  let (mods, out, _err, exit_code) = parse_args ["--verbose"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------");
+  (* err probably has output due to being unable to find tools; ignore *)
+  assert_equal None exit_code;
+  assert_equal [`B ("verbose", verbose, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_where _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--where"] in
+  assert_equal [] mods ~pp_diff:print_mod_diff;
+  assert_bool "Need stlib path" (not (String.equal out ""));
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal (Some 0) exit_code;
+  assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_config _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, _err, exit_code) = parse_args ["--config"] in
+  assert_equal [] mods ~pp_diff:print_mod_diff;
+  assert_bool "Need config" (String.starts_with out ~prefix:"-------------------- tlapm configuration --------------------");
+  (* err probably has output due to being unable to find tools; ignore *)
+  assert_equal (Some 0) exit_code;
+  assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_summary _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--summary"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("summary", summary, true); `B ("suppress_all", suppress_all, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  assert_equal false !check;
+  reset_setting_values ();;
+
+let test_timing _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--timing"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("stats", stats, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_search_paths _test_ctxt : unit =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["-I"; "some/module/path"; "-I"; "some/other/module/path"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  match changed_setting_values () with
+  | [`SL ("rev_search_path", _, [_; first_path; second_path])] ->
+      assert_bool "Should have first path" (string_contains "some/other/module/path" first_path);
+      assert_bool "Should have second path" (string_contains "some/module/path" second_path);
+  | _ -> assert_bool "Search path not as expected" false;
+  reset_setting_values ();;
+
+let test_keep_going _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["-k"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("keep_going", keep_going, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_suppress_all _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["-N"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("suppress_all", suppress_all, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_use_isabelle_tla _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["-C"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("check", check, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_set_max_threads _test_ctxt =
+  reset_setting_values ();
+  let thread_count = !max_threads + 1 in
+  let (mods, out, err, exit_code) = parse_args ["--threads"; Int.to_string thread_count; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`I ("max_threads", max_threads, thread_count)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_set_method _text_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--method"; "fail"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`ML ("default_method", default_method, [Tlapm_lib__Method.Fail])] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_set_solver _test_ctxt =
+  reset_setting_values ();
+  let solver_cmd = "my_solver_cmd" in
+  let (mods, out, err, exit_code) = parse_args ["--solver"; solver_cmd; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  (* Params.exec is unfortunately an opaque type whose value we cannot directly access *)
+  assert_bool "Solver command should be custom" (string_contains solver_cmd (solve_cmd smt "file.tla"));
+  reset_setting_values ();;
+
+let test_set_smt_logic _test_ctxt =
+  reset_setting_values ();
+  let expected_smt_logic = "my_smt_logic" in
+  let (mods, out, err, exit_code) = parse_args ["--smt-logic"; expected_smt_logic; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`S ("smt_logic", smt_logic, expected_smt_logic)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_stretch _test_ctxt =
+  reset_setting_values ();
+  let expected_stretch = Float.add !timeout_stretch 1.0 in
+  let (mods, out, err, exit_code) = parse_args ["--stretch"; Float.to_string expected_stretch; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`F ("timeout_stretch", timeout_stretch, expected_stretch)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_no_flatten _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--noflatten"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("ob_flatten", ob_flatten, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_no_normalize _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--nonormal"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("pr_normal", pr_normal, false)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_debug_flags _test_ctxt =
+  reset_setting_values ();
+  let expected_debug_flags = ["foo"; "bar"; "baz"] in
+  let (mods, out, err, exit_code) = parse_args ["--debug"; String.concat "," expected_debug_flags; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  List.iter (fun flag -> assert_bool flag (debugging flag)) expected_debug_flags;
+  List.iter rm_debug_flag expected_debug_flags;
+  reset_setting_values ();;
+
+let test_toolbox_mode _test_ctxt =
+  reset_setting_values ();
+  let (tb_start, tb_end) = (1, 2) in
+  let (mods, out, err, exit_code) = parse_args ["--toolbox"; Int.to_string tb_start; Int.to_string tb_end; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_bool "Expect toolbox output" (out <> "");
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("toolbox", toolbox, true); `I ("tb_sl", tb_sl, tb_start); `I ("tb_el", tb_el, tb_end)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_toolbox_protocol_version _test_ctxt =
+  reset_setting_values ();
+  let expected_toolbox_version = 3 in
+  let (mods, out, err, exit_code) = parse_args ["--toolbox-vsn"; Int.to_string expected_toolbox_version; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_bool "Expect toolbox output" (out <> "");
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("toolbox", toolbox, true); `I ("toolbox_vsn", toolbox_vsn, expected_toolbox_version)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_line _test_ctxt =
+  reset_setting_values ();
+  let expected_line = 10 in
+  let (mods, out, err, exit_code) = parse_args ["--line"; Int.to_string expected_line; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_bool "Expect toolbox output" (out <> "");
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("toolbox", toolbox, true); `I ("tb_sl", tb_sl, expected_line); `I ("tb_el", tb_el, expected_line)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_wait _test_ctxt =
+  reset_setting_values ();
+  let expected_wait = 30 in
+  let (mods, out, err, exit_code) = parse_args ["--wait"; Int.to_string expected_wait; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`I ("wait", wait, expected_wait)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_use_stdin _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--stdin"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("use_stdin", use_stdin, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_prefer_stdlib _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--prefer-stdlib"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("prefer_stdlib", prefer_stdlib, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_no_prove _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--noproving"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("noproving", noproving, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_print_all_obligations _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--printallobs"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("printallobs", printallobs, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_safe_fingerprints _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--safefp"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("safefp", safefp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_no_fingerprints _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--nofp"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("no_fp", no_fp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_no_fingerprints_between_lines _test_ctxt =
+  reset_setting_values ();
+  let (expected_start, expected_end) = (10, 20) in
+  let (mods, out, err, exit_code) = parse_args ["--nofpl"; Int.to_string expected_start; Int.to_string expected_end; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`I ("nofp_sl", nofp_sl, expected_start); `I ("nofp_el", nofp_el, expected_end)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_clean_fingerprints _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--cleanfp"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("cleanfp", cleanfp, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+(* Cannot test --erasefp due to side-effects *)
+(* Cannot test --printfp due to side-effects *)
+
+let test_use_fingerprints _test_ctxt =
+  reset_setting_values ();
+  let expected_fp_file = "FingerprintFile.txt" in
+  let (mods, out, err, exit_code) = parse_args ["--usefp"; expected_fp_file; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`SO ("fpf_in", fpf_in, Some expected_fp_file)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_fp_deb _test_ctxt =
+  reset_setting_values ();
+  let (mods, out, err, exit_code) = parse_args ["--fpp"; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`B ("fp_deb", fp_deb, true)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let test_cache_dir _test_ctxt =
+  reset_setting_values ();
+  let expected_cache_dir = "some/cache/dir" in
+  let (mods, out, err, exit_code) = parse_args ["--cache-dir"; expected_cache_dir; "Test.tla"] in
+  assert_equal ["Test.tla"] mods ~pp_diff:print_mod_diff;
+  assert_equal "" out ~pp_diff:print_string_diff;
+  assert_equal "" err ~pp_diff:print_string_diff;
+  assert_equal None exit_code;
+  assert_equal [`S ("cachedir", cachedir, expected_cache_dir)] (changed_setting_values ()) ~pp_diff:print_setting_list_diff;
+  reset_setting_values ();;
+
+let cli_test_suite = "Test CLI Parsing" >::: [
+  "Help Test" >:: test_help;
+  "Basic Test" >:: test_basic;
+  "Version Test" >:: test_version;
+  "No Mods Test" >:: test_no_mods;
+  "Verbose Test" >:: test_verbose;
+  "Print Stlib Location Test" >:: test_where;
+  "Print Config Test" >:: test_config;
+  "Print Summary Test" >:: test_summary;
+  "Print Stats Test" >:: test_timing;
+  "Search Paths Test" >:: test_search_paths;
+  "Keep Going Test" >:: test_keep_going;
+  "Suppress All Test" >:: test_suppress_all;
+  "Isabelle/TLA+ Check Test" >:: test_use_isabelle_tla;
+  "Max Threads Test" >:: test_set_max_threads;
+  "Set Method Test" >:: test_set_method;
+  "Custom Solver Test" >:: test_set_solver;
+  "Custom SMT Logic Test" >:: test_set_smt_logic;
+  "Stretch Test" >:: test_stretch;
+  "No Flatten Test" >:: test_no_flatten;
+  "No Normalize Test" >:: test_no_normalize;
+  "Debug Flag Test" >:: test_debug_flags;
+  "Toolbox Mode Test" >:: test_toolbox_mode;
+  "Toolbox Protocol Version Test" >:: test_toolbox_protocol_version;
+  "Check Specific Line Test" >:: test_line;
+  "Wait Before Printing Obligations Test" >:: test_wait;
+  "Use Stdin Test" >:: test_use_stdin;
+  "Prefer Stdlib Test" >:: test_prefer_stdlib;
+  "Skip Proving Test" >:: test_no_prove;
+  "Print All Obligations Test" >:: test_print_all_obligations;
+  "Safe Fingerprint Check Test" >:: test_safe_fingerprints;
+  "No Fingerprints Test" >:: test_no_fingerprints;
+  "No Fingerprints Between Specific Lines Test" >:: test_no_fingerprints_between_lines;
+  "Clean Fingerprints Test" >:: test_clean_fingerprints;
+  "Use Specififc Fingerprint File Test" >:: test_use_fingerprints;
+  "Test Print Fingerprints in Toolbox Messages" >:: test_fp_deb;
+  "Cache Dir Test" >:: test_cache_dir;
+];;
+
+let () = run_test_tt_main cli_test_suite
+
diff --git a/test/cli/dune b/test/cli/dune
new file mode 100644
index 00000000..4c31849e
--- /dev/null
+++ b/test/cli/dune
@@ -0,0 +1,5 @@
+(test
+ (name cli_tests)
+ (modes exe)
+ (libraries tlapm_lib ounit2)
+)