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. T

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).