[igornotarobot]

> TLA+ can specify anything that could be specified in mathematics.

You are talking about the logic of TLA+, that is, its mathematical definition. No tool for TLA+ can handle all of mathematics at the moment. The language was designed for specifying systems, not all of mathematics.