This is a common question among TLA+ beginners.

There can be bugs in the implementation. Those would either be bugs due to a mistranslation of the spec -- i.e., an error in the implementation -- or, because the spec also implicitly or explicitly describes the assumptions about the environment, a mismatch between the actual environment (hardware, software stack, user behavior) and the spec -- i.e. an error in the spec.

In both cases, having the spec makes finding those bugs easier, and in the first case, the bugs are usually cheap to find and fix. The costliest bugs are in the design, and that's where TLC, a model checker for TLA+, can automatically spot them.

Now, what if you want a formal -- i.e. mechanical -- relationship between the code and the spec? In principle, this is possible, and has been done; e.g. see [1] for C, and there have been other, similar projects for Java. In practice, we don't do it. Why? Well, we can't. There is no known technique that can verify anything but small programs/specs for arbitrary correctness properties. The reason is that the scalability of all formal methods has limitations. Currently, we can formally verify a few thousand lines of formal specification. That specification can be either code or a high-level spec. That means that we can either verify very small programs, or a high-level spec that represents a large program. The latter is the only thing available to us to help with large program, and how TLA+ is normally used. Small programs are verified end-to-end (i.e., that the actual code, or even machine code, conforms to a high-level spec) only in very special, niche, cases, and/or at a great cost.

What else can we do? We can verify code not against a high-level spec, but against some specification of small, local properties. This way, every code unit is verified separately [2]. This could help catch errors in translation, but, while useful, the benefit is not as great as verifying a high-level spec. This approach, a high-level spec verified formally, translated informally to code, and the code is then verified formally against local properties only, is how Altran UK builds their software; they use the older Z, instead of TLA+ for the high-level spec, and SPARK for code-level verification. Local properties can be verified with languages/tools like SPARK, JML and its various tools for Java, ACSL and various tools for C, and others, including dependent type languages used in research.

There is also an affordable way to mechanically check a program's conformance to a TLA+ spec, but only approximately -- it isn't sound. It's called "model-based trace-checking," and the idea is to grab logs from the program, or an entire distributed system, and let TLC check that they conform to a possible execution of the spec. I've written about this technique here [3].

It is important to realize that all kinds of software assurance techniques, from proof assistants to unit tests, come with significant tradeoffs to confidence, effort and scale, and that none can guarantee that a system will not fail. We must choose an appropriate balance for our specific system, usually by employing more than one approach (usually more than two). Personally, I think that high-level TLA+ specifications, checked with the TLC model checker (not with the TLAPS proof assistant) are at a pretty good sweet-spot for a relatively large number of mainstream software projects in terms of cost/benefit compared to other tools and approaches (but should still be combined with testing and code review).

[1]: https://cedric.cnam.fr/fichiers/art_3439.pdf

[2]: You may think that it's possible to verify local properties of local units, and then compose them to ensure conformance to a high-level spec. Unfortunately, this way doesn't beat the scalability limitation, and also works only on very small programs.

[3]: https://pron.github.io/files/Trace.pdf