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.