diff --git a/src/main.ml b/src/main.ml
index 0a45a7074090a2f85e7479b8fa71233bfa3ba22a..4aea0394418298f5d8f77124354a3ed0f3802869 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -122,7 +122,8 @@ let verify_cmd =
   let cmdname = "verify" in
   let files =
     let doc = "Files to verify." in
-    Arg.(value & pos_all string [] & info [] ~doc)
+    let file_or_stdin = Verification.File.(of_string, pretty) in
+    Arg.(value & pos_all file_or_stdin [] & info [] ~doc)
   in
   let format =
     let doc = "File format." in
diff --git a/src/verification.ml b/src/verification.ml
index 863155b30186f8742fe3552928f12c5607f81de3..51dd4f56180f2f9f985dc814596f57ae484a44cc 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -8,6 +8,21 @@ open Why3
 open Base
 module Filename = Caml.Filename
 
+module File = struct
+  type t = Stdin | File of string
+
+  let of_string s =
+    if String.equal s "-"
+    then `Ok Stdin
+    else if Caml.Sys.file_exists s
+    then `Ok (File s)
+    else `Error (Fmt.str "no '%s' file or directory" s)
+
+  let pretty fmt = function
+    | Stdin -> Fmt.string fmt "-"
+    | File f -> Fmt.string fmt f
+end
+
 let () =
   Language.register_nnet_support ();
   Language.register_onnx_support ()
@@ -84,9 +99,9 @@ let verify ?(debug = false) format loadpath ?memlimit ?timeout prover file =
   in
   let _, mstr_theory =
     match file with
-    | "-" ->
+    | File.Stdin ->
       ("stdin", Env.(read_channel ?format base_language env "stdin" Caml.stdin))
-    | file ->
+    | File file ->
       let mlw_files, _ = Env.(read_file ?format base_language env file) in
       (file, mlw_files)
   in
diff --git a/src/verification.mli b/src/verification.mli
index 117f64ca7ce5370e5d0896b2a06998fe70b3237c..36ba72e042266b79b26d41b084004b02575e4586 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -4,6 +4,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module File : sig
+  type t
+
+  val of_string : string -> [ `Ok of t | `Error of string ]
+  val pretty : Format.formatter -> t -> unit
+end
+
 val verify :
   ?debug:bool ->
   string option ->
@@ -11,7 +18,7 @@ val verify :
   ?memlimit:int ->
   ?timeout:int ->
   Prover.t ->
-  string ->
+  File.t ->
   unit
 (** [verify debug format loadpath memlimit timeout prover file] launches a
     verification of the given [file] with the provided [prover].