> I don't want to stick linear or dependent types into TLA+. Proving dynamic properties with an exhaustive runtime is a totally different game from what you might do statically.

Yup, TLA+ is a totally different beast from, say, Lean 4. Both are useful. I don't want dependent types in TLA+ either.