TLA+ is only for specification. In one of the papers on it Lamport mentions just putting a copy of the specification in a comment above the implementation. If you get a bug you just need to find where your implementation differs from your specification which he finds is usually pretty easy.

If your code doesn't have a specification (of course usually less precise), fixing bugs is incoherent. How can you say come behavior is a bug?