[LiamPowell]

You can't have the borrow checker without bringing the rest of SPARK with it as far as I'm aware, so this comes with the requirement that you prove the your program contains no other runtime errors.