If only TLA+ could work with the actual product code, or even some machine-translation of same.
Then it will be too noisy or too slow to be useful due to too many intermediate states. The feature of TLA+ is that it forces you to greatly dumb down the code to be able to use it, so it's more of verifying an algorithm represented as visual graph blocks rather than verifying assembly instructions.
I understand the wish for a magic bullet to just verify already existing code, but I recon the answer to this is to verify code before it's even written.
Hmm well obviously I know this, and it's like that because doing it properly is so far unachievable. Problem is there's an uncontrolled step between the code being run and the code being verified. This means we only verify an artist's sketch of the thing we want to test.