diff --git a/src/AIMOS.ml b/src/AIMOS.ml
index f4e0c737144cb58d6fb2ca8e239d0f518979bd2f..1588dd387b51c22a05e63516f8cc16bc572c7499 100644
--- a/src/AIMOS.ml
+++ b/src/AIMOS.ml
@@ -34,7 +34,7 @@ let re_aimos_output = Re__Pcre.regexp "((,\\s)(\\d+\\.\\d+))"
 let build_answer predicate_kind prover_result =
   let threshold =
     match predicate_kind with
-    | Dataset.MetaRobust f -> Float.of_string (Dataset.string_of_eps f)
+    | Dataset.MetaRobust f -> Float.of_string (Dataset.string_of_threshold f)
     | _ -> failwith "Unsupported property"
   in
   match prover_result.Call_provers.pr_answer with
diff --git a/src/JSON.ml b/src/JSON.ml
index 26b9a7c9c546c8290324fb61dc57e9b73f046303..502f4be324baa12ef40c083556898b0627f6b432 100644
--- a/src/JSON.ml
+++ b/src/JSON.ml
@@ -120,7 +120,7 @@ let theory_of_input env input =
         in
         let t_eps = Dataset.term_of_eps env eps in
         Term.t_app_infer ls_robust [ t_model; t_dataset; t_eps ]
-      | CondRobust _ -> invalid_arg "Not yet supported property"
+      | CondRobust _ | MetaRobust _ -> invalid_arg "Not yet supported property"
     in
     let prsymbol = Decl.create_prsymbol (Ident.id_fresh "property") in
     Theory.add_prop_decl th_uc Decl.Pgoal prsymbol t_property
diff --git a/src/SAVer.ml b/src/SAVer.ml
index f5347ecdebf748bc620f16b69910d0b6ca46cabe..40511c632e36025ae564c0660be34f2d8ddc012c 100644
--- a/src/SAVer.ml
+++ b/src/SAVer.ml
@@ -74,12 +74,14 @@ let re_group_number_of_predicate = function
   | Dataset.Correct -> 2
   | Robust _ -> 3
   | CondRobust _ -> 4
+  | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"
 
 let negative_answer = function
   | Dataset.Correct ->
     (* SAVer is complete wrt [Correct] predicate. *)
     Call_provers.Invalid
   | Robust _ | CondRobust _ -> Call_provers.Unknown ""
+  | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"
 
 let build_answer predicate_kind prover_result =
   match prover_result.Call_provers.pr_answer with
@@ -114,6 +116,7 @@ let call_prover limit config config_prover predicate =
       match predicate.property with
       | Dataset.Correct -> None
       | Robust e | CondRobust e -> Some e
+      | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"
     in
     build_command config_prover svm dataset eps
   in
diff --git a/src/dataset.ml b/src/dataset.ml
index e46e698a8350983f41fbda03efd30def1ad4887f..5221dd9ad2b08ae53dded4d3b9b729ed5ff0c3f7 100644
--- a/src/dataset.ml
+++ b/src/dataset.ml
@@ -49,10 +49,15 @@ let term_of_eps env eps =
   let ty = Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) [] in
   Term.t_const (real_constant_of_float eps) ty
 
+type threshold = float [@@deriving yojson, show]
+
+let string_of_threshold threshold = Float.to_string threshold
+
 type property =
   | Correct
   | Robust of eps
   | CondRobust of eps
+  | MetaRobust of threshold
 [@@deriving yojson, show]
 
 type ('a, 'b) predicate = {
@@ -65,6 +70,7 @@ let string_of_predicate_kind = function
   | Correct -> "correct"
   | Robust _ -> "robust"
   | CondRobust _ -> "condrobust"
+  | MetaRobust _ -> "meta_robust"
 
 let find_predicate_ls env p =
   let th = Pmodule.read_module env [ "caisar" ] "DatasetClassificationProps" in
@@ -95,11 +101,14 @@ let interpret_predicate env ~on_model ~on_dataset task =
       | [ { t_node = Tconst (Constant.ConstReal e); _ } ] ->
         let robust_predicate = find_predicate_ls env "robust" in
         let cond_robust_predicate = find_predicate_ls env "cond_robust" in
+        let meta_robust_predicate = find_predicate_ls env "meta_robust" in
         let f = float_of_real_constant e in
         if Term.ls_equal ls robust_predicate
         then Robust f
         else if Term.ls_equal ls cond_robust_predicate
         then CondRobust f
+        else if Term.ls_equal ls meta_robust_predicate
+        then MetaRobust f
         else failwith_unsupported_ls ls
       | _ -> failwith_unsupported_term term
     in
@@ -150,6 +159,7 @@ let add_input_decls predicate_kind ~inputs ~record th task =
     | Correct -> None
     | Robust eps -> Some (string_of_eps eps)
     | CondRobust _ -> failwith "Unsupported conditional robustness predicate"
+    | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"
   in
   List.fold2_exn inputs features ~init:task ~f:(add_axioms ?eps th)
 
diff --git a/src/dataset.mli b/src/dataset.mli
index ef90cafb58675813ff0af71eda92b7b1c79d928c..a9fcef615ba5ea28ae15429713c022b4e6a5dffb 100644
--- a/src/dataset.mli
+++ b/src/dataset.mli
@@ -27,10 +27,15 @@ type eps [@@deriving yojson, show]
 val string_of_eps : eps -> string
 val term_of_eps : Env.env -> eps -> Term.term
 
+type threshold [@@deriving yojson, show]
+
+val string_of_threshold : threshold -> string
+
 type property = private
   | Correct
   | Robust of eps
   | CondRobust of eps
+  | MetaRobust of threshold
 [@@deriving yojson, show]
 
 type ('model, 'dataset) predicate = private {
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 88422668ce03cd48622b9fd95c481eecc0dc009c..aeea7093ede433c836821d58fd184d9c7097a2e4 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -68,6 +68,8 @@ theory DatasetClassificationProps
 
   predicate cond_robust (m: model) (d: dataset) (eps: t) =
     correct m d /\ robust m d eps
+
+  predicate meta_robust (m: model) (d: dataset) (threshold: t)
 end
 
 theory NN