formatting2.v

Notation "⊤" := True : dms_scope.
Notation " {@ T1 } " := ( and T1 True ) (format "{@  T1  }"): dms_scope.
Notation " {@ T1 ; T2 ; .. ; Tn } " :=
  (and T1 (and T2 .. (and Tn True)..))
  (format "'[v' {@  '[' T1 ']'  ;  '//' '[' T2 ']'  ;  '//' ..  ;  '//' '[' Tn ']'  } ']'") : dms_scope.
Open Scope dms_scope.
Close Scope dms_scope.
Delimit Scope dms_scope with dms.
Check {@ True ; True -> False ; False } % dms.

3rd line gives error:
The format is not the same on the right- and left-hand sides of the special token "..".

The explicit boxes around T1, T2 and Tn are not needed. There is always a default hov box around any notation as soon as it is liable to be broken over several lines.

Maybe Coq could warn when seeing such '[' T1 ']'?

A warning would help. I also didn't find this in the docs about defaulting, but a warning is easier to understand anyway :-)