Hillel Wayne's "Practical TLA+" book and the TLA+ examples repository (https://github.com/tlaplus/Examples) both contain excellent worked examples ranging from simple algorithms to complex distributed systems.

Thanks. Tangentially TLA+ seems to be most useful for finding concurrency bugs. I'm yet to find a compelling example of it used for a fairly mundane, by that I mean composed of mainly sequential processes, systems architecture.