diff --git a/src/prover.ml b/src/prover.ml
index 847cc3e20e0896f11deb8cf00cf636834185642a..d5436fdb9002ba3523f6cd4167c4d0a2170e1362 100644
--- a/src/prover.ml
+++ b/src/prover.ml
@@ -22,9 +22,9 @@
 
 type t =
   | Marabou
-  | Pyrat
-  | Saver
-  | CVC5
+  | Pyrat [@name "PyRAT"]
+  | Saver [@name "SAVer"]
+  | CVC5 [@name "cvc5"]
 [@@deriving yojson, show]
 
 let list_available () = [ Marabou; Pyrat; Saver; CVC5 ]
diff --git a/src/prover.mli b/src/prover.mli
index 1ae811a671fa5d950f8c60f1f9baa0bfd4d9192d..f318d47119b7ef9ac7e5a9c509c0a176bba5e519 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -22,9 +22,9 @@
 
 type t = private
   | Marabou
-  | Pyrat
-  | Saver
-  | CVC5
+  | Pyrat [@name "PyRAT"]
+  | Saver [@name "SAVer"]
+  | CVC5 [@name "cvc5"]
 [@@deriving yojson, show]
 
 val list_available : unit -> t list
diff --git a/tests/pyrat_verify_json.t b/tests/pyrat_verify_json.t
index 9d1ddd4da9492bbe9542589225d528ed97b81ed5..feba4654be7a4b9d5a02478ba60b50fbf8e3406b 100644
--- a/tests/pyrat_verify_json.t
+++ b/tests/pyrat_verify_json.t
@@ -4,7 +4,7 @@ Test verify-json
   > EOF
 
   $ cat - > config.json << EOF
-  > {"prover":["Pyrat"],"model":"TestNetwork.nnet","property":{"dataset":"test_data.csv","normalization":["MinMax",{"clip":true,"min":0.0,"max":1.0}],"kind":["Robust",0.01]}}
+  > {"prover":["PyRAT"],"model":"TestNetwork.nnet","property":{"dataset":"test_data.csv","normalization":["MinMax",{"clip":true,"min":0.0,"max":1.0}],"kind":["Robust",0.01]}}
   > EOF
 
   $ chmod u+x bin/pyrat.py