Aren't invariants essentially just a very specific "what do you want"? TLA+ doesn't know what you want the code to do. It can only tell you if it's doing it properly.