While TLA+ is not intended to verify specific code implementations, we have to admit that that is the holy grail. In my view there are 2 main spheres of practic

While TLA+ is not intended to verify specific code implementations, we have to admit that that is the holy grail. In my view there are 2 main spheres of practical software: design and construction. Unfortunately, today's construction tools are so error-prone that simply implementing a given design doesn't guarantee that the code is error-free. I think people see TLA+ as an escape from this construction nightmare - because its model is so simple and elegant. I know my wheels have been spinning trying to think about the best way to unify the design and construction processes. So I definitely don't fault people for trying to specify lower and lower levels.