TLA+ is mathematics. The TLC module introduces some operators that
aren't mathematics. They are there because they can be useful when
running TLC, but you have to understand how TLC works to make good use
of them. The formula e = e is true for any mathematical _expression_ e.
It isn't true if e is Random(...). Hence Random isn't mathematics, so
you shouldn't use it unless you understand how TLC works.
We all wish there were more examples of TLA+ specs, but we all have
lots of things to do. Industrial users generally don't publish their
specifications. One exception is a book that describes the use of
TLA+ to design a real-time operating system for the European Space
Agency spacecraft that's now sitting in the shade on a comet that I
believe is now heading away from the sun. The principal author is
Eric Verhulst. However, did you really want to read a few hundred
pages of an example? You can read about how TLA+ helped at Amazon,
without any actual specifications, in an article published in
Communications of the ACM in spring 2015 with Chris Newcombe as