This sounds a lot like the invariant that they're checking is that, _given a conforming counter-party_, nothing illegal will happen. But this doesn't tell you

This sounds a lot like the invariant that they're checking is that, _given a conforming counter-party_, nothing illegal will happen. But this doesn't tell you anything about what happens to you when your peer passes between states in an illegal manner. I'd expect this to have been emphasised in the paper. Especially if their threat model includes it, it would be a key selling point.