Yes!

Dafny puts this stuff front and center, it's all well and good to think about invariants, but if they're just expressed in a comment and not actually verified, they might as well be filler text!

If there's anything I hope the mainstream adopts at some point, it is some variation of what Dafny offers here.