Personally, I think the verus! macro is too much in the way for this approach to be feasible. Kani or Prusti syntax is much more usable for real projects.