You can think about a TLA+ spec as the level of design between the "natural language design" you have in your head or on paper and the code. It makes it easier to go from the idea to the code, and allows you to explore ideas, at any level of abstraction, with full rigour.
The question of how you maintain the spec as the code changes could be the same as how you maintain the natural language spec as the code changes. Sometimes you just don't, and you may want to only when there is a very substantial change that you'd also like to explore with rigour.
However, there are several approaches for creating a more formal (i.e. mechanical) connection between the code and the TLA+ spec, such as generating tests or checking production logs against the high-level spec, but I would say that you already get so much benefit even without such a mechanical connection that having it is not needed, but could be the cherry on top in some situations that really require it.
I think that the greatest hurdle in getting the most out of TLA+ is internalising that the spec isn't code, and isn't supposed to be. For example, if you're making use of some hashing function or a sorting function and the subject of your design isn't the hashing or sorting algorithm itself, in TLA+ you want write a hashing/sorting spec or reuse one from a library; rather you'd write something like "assume there exists a hashing/sorting function".
That's why you may end up writing different specs for the same application, each focusing on a particular aspect of the system at the appropriate level of detail for that aspect. A single line of TLA+ spec could correspond to anywhere between 1 and 100K lines of code. The use is more similar to how a physicist would describe a system than to code, which is (part of) the system. For example, if the physicist is interested only in the orbit of a planet around its star, it may represent it as a point-mass; if she's interested in weather patterns on the planet, then there's an entire different description. It's a map, not the territory.
The question of how you maintain the spec as the code changes could be the same as how you maintain the natural language spec as the code changes. Sometimes you just don't, and you may want to only when there is a very substantial change that you'd also like to explore with rigour.
However, there are several approaches for creating a more formal (i.e. mechanical) connection between the code and the TLA+ spec, such as generating tests or checking production logs against the high-level spec, but I would say that you already get so much benefit even without such a mechanical connection that having it is not needed, but could be the cherry on top in some situations that really require it.
I think that the greatest hurdle in getting the most out of TLA+ is internalising that the spec isn't code, and isn't supposed to be. For example, if you're making use of some hashing function or a sorting function and the subject of your design isn't the hashing or sorting algorithm itself, in TLA+ you want write a hashing/sorting spec or reuse one from a library; rather you'd write something like "assume there exists a hashing/sorting function".
That's why you may end up writing different specs for the same application, each focusing on a particular aspect of the system at the appropriate level of detail for that aspect. A single line of TLA+ spec could correspond to anywhere between 1 and 100K lines of code. The use is more similar to how a physicist would describe a system than to code, which is (part of) the system. For example, if the physicist is interested only in the orbit of a planet around its star, it may represent it as a point-mass; if she's interested in weather patterns on the planet, then there's an entire different description. It's a map, not the territory.