diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 43707acd1e..5895f242c9 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -200,6 +200,46 @@ struct
           M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
       in
 
+      let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
+
+        let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
+          let loc = loc_of_location location_invariant.location in
+          let inv = location_invariant.value in
+          let msgLoc: M.Location.t = CilLocation loc in
+
+          match Locator.find_opt locator loc with
+          | Some nodes ->
+            unassume_nodes_invariant ~loc ~nodes inv
+          | None ->
+            M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
+        in
+
+        let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
+          let loc = loc_of_location loop_invariant.location in
+          let inv = loop_invariant.value in
+          let msgLoc: M.Location.t = CilLocation loc in
+
+          match Locator.find_opt loop_locator loc with
+          | Some nodes ->
+            unassume_nodes_invariant ~loc ~nodes inv
+          | None ->
+            M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
+        in
+
+        let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
+          let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in
+          match YamlWitness.invariant_type_enabled target_type, invariant.invariant_type with
+          | true, LocationInvariant x ->
+            unassume_location_invariant x
+          | true, LoopInvariant x ->
+            unassume_loop_invariant x
+          | false, (LocationInvariant _ | LoopInvariant _) ->
+            M.info_noloc ~category:Witness "disabled invariant of type %s" target_type
+        in
+
+        List.iter validate_invariant invariant_set.content
+      in
+
       match YamlWitness.entry_type_enabled target_type, entry.entry_type with
       | true, LocationInvariant x ->
         unassume_location_invariant x
@@ -207,7 +247,9 @@ struct
         unassume_loop_invariant x
       | true, PreconditionLoopInvariant x ->
         unassume_precondition_loop_invariant x
-      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _) ->
+      | true, InvariantSet x ->
+        unassume_invariant_set x
+      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) ->
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type
       | _ ->
         M.info_noloc ~category:Witness "cannot unassume entry of type %s" target_type
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 4e282b19a4..fd8f210745 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -2418,6 +2418,16 @@
               "type": "boolean",
               "default": false
             },
+            "format-version": {
+              "title": "witness.yaml.format-version",
+              "description": "YAML witness format version",
+              "type": "string",
+              "enum": [
+                "0.1",
+                "2.0"
+              ],
+              "default": "0.1"
+            },
             "entry-types": {
               "title": "witness.yaml.entry-types",
               "description": "YAML witness entry types to output/input.",
@@ -2430,7 +2440,8 @@
                   "flow_insensitive_invariant",
                   "precondition_loop_invariant",
                   "loop_invariant_certificate",
-                  "precondition_loop_invariant_certificate"
+                  "precondition_loop_invariant_certificate",
+                  "invariant_set"
                 ]
               },
               "default": [
@@ -2438,7 +2449,24 @@
                 "loop_invariant",
                 "flow_insensitive_invariant",
                 "loop_invariant_certificate",
-                "precondition_loop_invariant_certificate"
+                "precondition_loop_invariant_certificate",
+                "invariant_set"
+              ]
+            },
+            "invariant-types": {
+              "title": "witness.yaml.invariant-types",
+              "description": "YAML witness invariant types to output/input.",
+              "type": "array",
+              "items": {
+                "type": "string",
+                "enum": [
+                  "location_invariant",
+                  "loop_invariant"
+                ]
+              },
+              "default": [
+                "location_invariant",
+                "loop_invariant"
               ]
             },
             "path": {
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 9e8ebeff51..f8532a1551 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -25,7 +25,7 @@ struct
     let uuid = Uuidm.v4_gen uuid_random_state () in
     let creation_time = TimeUtil.iso8601_now () in
     {
-      format_version = "0.1";
+      format_version = GobConfig.get_string "witness.yaml.format-version";
       uuid = Uuidm.to_string uuid;
       creation_time;
       producer;
@@ -91,6 +91,29 @@ struct
     metadata = metadata ~task ();
   }
 
+  let location_invariant' ~location ~(invariant): InvariantSet.Invariant.t = {
+    invariant_type = LocationInvariant {
+        location;
+        value = invariant;
+        format = "c_expression";
+      };
+  }
+
+  let loop_invariant' ~location ~(invariant): InvariantSet.Invariant.t = {
+    invariant_type = LoopInvariant {
+        location;
+        value = invariant;
+        format = "c_expression";
+      };
+  }
+
+  let invariant_set ~task ~(invariants): Entry.t = {
+    entry_type = InvariantSet {
+        content = invariants;
+      };
+    metadata = metadata ~task ();
+  }
+
   let target ~uuid ~type_ ~(file_name): Target.t = {
     uuid;
     type_;
@@ -120,12 +143,12 @@ struct
   }
 end
 
-let yaml_entries_to_file yaml_entries file =
+let yaml_entries_to_file ?(invariants=0) yaml_entries file =
   let yaml = `A yaml_entries in
   (* Yaml_unix.to_file_exn file yaml *)
   (* to_file/to_string uses a fixed-size buffer... *)
   (* estimate how big it should be + extra in case empty *)
-  let text = match Yaml.to_string ~len:(List.length yaml_entries * 4096 + 2048) yaml with
+  let text = match Yaml.to_string ~len:((List.length yaml_entries + invariants) * 4096 + 2048) yaml with
     | Ok text -> text
     | Error (`Msg m) -> failwith ("Yaml.to_string: " ^ m)
   in
@@ -134,6 +157,9 @@ let yaml_entries_to_file yaml_entries file =
 let entry_type_enabled entry_type =
   List.mem entry_type (GobConfig.get_string_list "witness.yaml.entry-types")
 
+let invariant_type_enabled invariant_type =
+  List.mem invariant_type (GobConfig.get_string_list "witness.yaml.invariant-types")
+
 module Make (R: ResultQuery.SpecSysSol2) =
 struct
   open R
@@ -385,13 +411,81 @@ struct
         entries
     in
 
+    (* Generate invariant set *)
+    let (entries, invariants) =
+      if entry_type_enabled YamlWitnessType.InvariantSet.entry_type then (
+        let invariants = [] in
+
+        (* Generate location invariants *)
+        let invariants =
+          if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then (
+            NH.fold (fun n local acc ->
+                let loc = Node.location n in
+                if is_invariant_node n then (
+                  let lvals = local_lvals n local in
+                  match R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals}) with
+                  | `Lifted inv ->
+                    let invs = WitnessUtil.InvariantExp.process_exp inv in
+                    List.fold_left (fun acc inv ->
+                        let location_function = (Node.find_fundec n).svar.vname in
+                        let location = Entry.location ~location:loc ~location_function in
+                        let invariant = CilType.Exp.show inv in
+                        let invariant = Entry.location_invariant' ~location ~invariant in
+                        invariant :: acc
+                      ) acc invs
+                  | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
+                    acc
+                )
+                else
+                  acc
+              ) (Lazy.force nh) invariants
+          )
+          else
+            invariants
+        in
+
+        (* Generate loop invariants *)
+        let invariants =
+          if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then (
+            NH.fold (fun n local acc ->
+                let loc = Node.location n in
+                if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then (
+                  match R.ask_local_node n ~local (Invariant Invariant.default_context) with
+                  | `Lifted inv ->
+                    let invs = WitnessUtil.InvariantExp.process_exp inv in
+                    List.fold_left (fun acc inv ->
+                        let location_function = (Node.find_fundec n).svar.vname in
+                        let location = Entry.location ~location:loc ~location_function in
+                        let invariant = CilType.Exp.show inv in
+                        let invariant = Entry.loop_invariant' ~location ~invariant in
+                        invariant :: acc
+                      ) acc invs
+                  | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
+                    acc
+                )
+                else
+                  acc
+              ) (Lazy.force nh) invariants
+          )
+          else
+            invariants
+        in
+
+        let invariants = List.rev invariants in
+        let entry = Entry.invariant_set ~task ~invariants in
+        (entry :: entries, List.length invariants)
+      )
+      else
+        (entries, 0)
+    in
+
     let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in (* reverse to make entries in file in the same order as generation messages *)
 
     M.msg_group Info ~category:Witness "witness generation summary" [
       (Pretty.dprintf "total generation entries: %d" (List.length yaml_entries), None);
     ];
 
-    yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
+    yaml_entries_to_file ~invariants yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
 
   let write () =
     Timing.wrap "yaml witness" write ()
@@ -639,6 +733,48 @@ struct
           None
       in
 
+      let validate_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
+
+        let validate_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
+          let loc = loc_of_location location_invariant.location in
+          let inv = location_invariant.value in
+
+          match Locator.find_opt locator loc with
+          | Some lvars ->
+            ignore (validate_lvars_invariant ~entry_certificate:None ~loc ~lvars inv)
+          | None ->
+            incr cnt_error;
+            M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv;
+        in
+
+        let validate_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
+          let loc = loc_of_location loop_invariant.location in
+          let inv = loop_invariant.value in
+
+          match Locator.find_opt loop_locator loc with
+          | Some lvars ->
+            ignore (validate_lvars_invariant ~entry_certificate:None ~loc ~lvars inv)
+          | None ->
+            incr cnt_error;
+            M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv;
+        in
+
+        let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
+          let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in
+          match invariant_type_enabled target_type, invariant.invariant_type with
+          | true, LocationInvariant x ->
+            validate_location_invariant x
+          | true, LoopInvariant x ->
+            validate_loop_invariant x
+          | false, (LocationInvariant _ | LoopInvariant _) ->
+            incr cnt_disabled;
+            M.info_noloc ~category:Witness "disabled invariant of type %s" target_type;
+        in
+
+        List.iter validate_invariant invariant_set.content;
+        None
+      in
+
       match entry_type_enabled target_type, entry.entry_type with
       | true, LocationInvariant x ->
         validate_location_invariant x
@@ -646,7 +782,9 @@ struct
         validate_loop_invariant x
       | true, PreconditionLoopInvariant x ->
         validate_precondition_loop_invariant x
-      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _) ->
+      | true, InvariantSet x ->
+        validate_invariant_set x
+      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) ->
         incr cnt_disabled;
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type;
         None
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
index 3390c1e3ab..f9bcf3235f 100644
--- a/src/witness/yamlWitnessType.ml
+++ b/src/witness/yamlWitnessType.ml
@@ -242,6 +242,100 @@ struct
     {location; loop_invariant; precondition}
 end
 
+module InvariantSet =
+struct
+  module LoopInvariant =
+  struct
+    type t = {
+      location: Location.t;
+      value: string;
+      format: string;
+    }
+
+    let invariant_type = "loop_invariant"
+
+    let to_yaml' {location; value; format} =
+      [
+        ("location", Location.to_yaml location);
+        ("value", `String value);
+        ("format", `String format);
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ location = y |> find "location" >>= Location.of_yaml
+      and+ value = y |> find "value" >>= to_string
+      and+ format = y |> find "format" >>= to_string in
+      {location; value; format}
+  end
+
+  module LocationInvariant =
+  struct
+    include LoopInvariant
+
+    let invariant_type = "location_invariant"
+  end
+
+  (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *)
+  module InvariantType =
+  struct
+    type t =
+      | LocationInvariant of LocationInvariant.t
+      | LoopInvariant of LoopInvariant.t
+
+    let invariant_type = function
+      | LocationInvariant _ -> LocationInvariant.invariant_type
+      | LoopInvariant _ -> LoopInvariant.invariant_type
+
+    let to_yaml' = function
+      | LocationInvariant x -> LocationInvariant.to_yaml' x
+      | LoopInvariant x -> LoopInvariant.to_yaml' x
+
+    let of_yaml y =
+      let open GobYaml in
+      let* invariant_type = y |> find "type" >>= to_string in
+      if invariant_type = LocationInvariant.invariant_type then
+        let+ x = y |> LocationInvariant.of_yaml in
+        LocationInvariant x
+      else if invariant_type = LoopInvariant.invariant_type then
+        let+ x = y |> LoopInvariant.of_yaml in
+        LoopInvariant x
+      else
+        Error (`Msg "type")
+  end
+
+  module Invariant =
+  struct
+    type t = {
+      invariant_type: InvariantType.t;
+    }
+
+    let to_yaml {invariant_type} =
+      `O ([
+          ("type", `String (InvariantType.invariant_type invariant_type));
+        ] @ InvariantType.to_yaml' invariant_type)
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ invariant_type = y |> InvariantType.of_yaml in
+      {invariant_type}
+  end
+
+  type t = {
+    content: Invariant.t list;
+  }
+
+  let entry_type = "invariant_set"
+
+  let to_yaml' {content} =
+    [("content", `A (List.map Invariant.to_yaml content))]
+
+  let of_yaml y =
+    let open GobYaml in
+    let+ content = y |> find "content" >>= list >>= list_map Invariant.of_yaml in
+    {content}
+end
+
 module Target =
 struct
   type t = {
@@ -326,6 +420,7 @@ struct
     | PreconditionLoopInvariant of PreconditionLoopInvariant.t
     | LoopInvariantCertificate of LoopInvariantCertificate.t
     | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t
+    | InvariantSet of InvariantSet.t
 
   let entry_type = function
     | LocationInvariant _ -> LocationInvariant.entry_type
@@ -334,6 +429,7 @@ struct
     | PreconditionLoopInvariant _ -> PreconditionLoopInvariant.entry_type
     | LoopInvariantCertificate _ -> LoopInvariantCertificate.entry_type
     | PreconditionLoopInvariantCertificate _ -> PreconditionLoopInvariantCertificate.entry_type
+    | InvariantSet _ -> InvariantSet.entry_type
 
   let to_yaml' = function
     | LocationInvariant x -> LocationInvariant.to_yaml' x
@@ -342,6 +438,7 @@ struct
     | PreconditionLoopInvariant x -> PreconditionLoopInvariant.to_yaml' x
     | LoopInvariantCertificate x -> LoopInvariantCertificate.to_yaml' x
     | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate.to_yaml' x
+    | InvariantSet x -> InvariantSet.to_yaml' x
 
   let of_yaml y =
     let open GobYaml in
@@ -364,6 +461,9 @@ struct
     else if entry_type = PreconditionLoopInvariantCertificate.entry_type then
       let+ x = y |> PreconditionLoopInvariantCertificate.of_yaml in
       PreconditionLoopInvariantCertificate x
+    else if entry_type = InvariantSet.entry_type then
+      let+ x = y |> InvariantSet.of_yaml in
+      InvariantSet x
     else
       Error (`Msg "entry_type")
 end