... and also to classical logic. Liveness proofs typically require finding a variant that converges to some terminal value, and that's just as easy to do in classical logic as in constructive logic.

I've been using formal methods for years now and have yet to see where constructive logic makes things easier (I'm not saying it necessarily makes things harder, either).