Boxed Comments

It's a common practice to use boxed comments in TLA⁺ specifications:

(**************************************************************)
(* This is a boxed comment.                                   *)
(* Such comment format is used in lots of specifications.     *)
(**************************************************************)

If you'd like to format your comments this way easily, you might want to install the Comment Box extension, and add the following settings to your settings.json:

"commentBox.styles": {
    "defaultStyle": {
        "commentStartToken": "(**",
        "commentEndToken": "**)",
        "leftEdgeToken": "(* ",
        "rightEdgeToken": " *)",
        "topEdgeToken": "*",
        "bottomEdgeToken": "*",
        "topRightToken": "**)",
        "bottomLeftToken": "(**",
        "capitalize": false,
        "ignoreInnerIndentation": false,
        "ignoreOuterIndentation": false,
        "removeEmptyLines": false,
        "textAlignment": "left"
    }
}

You can add multiple styles with different settings, add shortcuts to quickly apply formatting, etc. Please, refer to the Comment Box documentation for the full feature list.