Yes, the model is more like an executable form of documentation. There’s no guarantee that code comments match what the code actually does; similarly there’s no guarantee that the TLA+ model matches what the system does.

Documentation is still generally useful, and so is a model. You have to be committed to keeping both up to date as the code evolves.