You're right, but invariants are the most bang for the buck you can get out of formal methods without having to use a DSL built for computer assisted proofs.

That they work for binary search is a very strong signal to people not familiar with them that they work for nearly everything (they do).