It can model that if you add it. You can model total or partial hardware failure if you want and its a case you care about, you can add steps that corrupt your data or steps that kills machines at any time. TLA+ is just a way of defining state transitions and temporal properties, inside that add the use cases you need and it will handle them just fine.
And then calling that C API, that Vulkan shader with a broken SPIR-V driver, the automated router firmware update done overnight, just brings down all the hard verification work, done in an external tool.
So because a tool doesn't fix everything it's best not to use it? Each tool has its place, its uses and their limitations. You buy a car even if it doesn't cook you food. If you have multiprocess algorithms, distributed systems or concurrency at all, TLA+ is a lifesaver to understand and fix fundamental issues in your system, if you care about a broken shader, it's just not your tool. When there is a bug you can discard a whole part of the problems and you can check the implementation against a known specification that works.
I wouldn't think I need to explain this to a professional developer, if you are waiting for the silver bullet that solves all your problems you may as well go take care of goats.
To pick up your example, it is more like getting the driver license with only the theorical written test, and only thereafter drive a car for the very first time on the road with the newly received license.
Yes, we should be open minded, and the tools should also be improved so that developers on the trenches bother to learn and use them.
You are clearly engaging in bad faith at this point when you pick the "car not being useful for everything" analogy and you cherrypick it into absurdity. For someone that says is interested in distributed algorithms it's clear you are not interested in being able to reason, about them.
EDIT: There was an edit adding the final part of the comment after I submitted mine above. Here is my response to the last part, since the comment was toned down a bit:
Yes, we need to improve the tooling, and TLA+ can be improved a lot, I'd love for it to be able to reason about my code and to have an easier bridge between both words. However engaging in the discussion of how it can be improved without acknowledging what good and usefulness it brings is just not useful in general, and it just puts off people that could benefit from it from ever using it.
TLA+ has a lot of value in some cases, and we should be acknowledging that!
