All users of Dyn.anonymous (ie Store.field and Proof.new_focus_kind) use it with a local counter, eg

  let next = ref 0
  let field () =
    let f = Dyn.anonymous !next in
    incr next;
    f

If 2 plugins which don't depend on each other generate such tags and pass them to other processes through marshal, demarshalling correctly depends on plugin link order and is buggy.
ie

Declare ML Module "plugin1". (* now plugin1 has anonymous 0 : plugin1.t tag *)
Declare ML Module "plugin2". (* now plugin1 has anonymous 1 : plugin2.t tag *)

Reset Initial. (* plugins are still linked and have use the same tags *)

Declare ML Module "plugin2".
Declare ML Module "plugin1".
(* still no change in tags *)

Goal True.
Proof.
(* with async proofs, the async process links plugin2 first so the tags are swapped *)
exact I.
Qed.

Current coq-core plugins either depend on each other (which forces link order) or do not make new tags in the same dyn instance, eg

• new_focus_kind is used by ssr but no other plugin
• the exninfo store gets new tags from ltac1 debug and ltac2 backtrace, but ltac2 depends on ltac1
• etc

so the bug currently cannot be triggered.

NB: #17098 adds a new user of Dyn.anonymous through grammar entry creation, but is not bugged because the entries don't get marshalled.