[deterministic]

I recommend learning Dafny instead of TLA+. It gives you all of the same reasoning power, with the added advantage that you can run your proven code in production.