That looks incredibly useful. Proving the absence of panics and overflows is already great, and with the annotations you can guarantee properties you'd normally write property tests for, like in this example from the docs:

  impl List {
      #[ensures(self.len() == old(self.len()) + 1)]
      pub fn push(&mut self, elem: i32) {
          // TODO
      }
  }