Disclaimer: I don't know how much formal you want your proof to be and I'm not familiar with formal proofs.
- induction on the while loop: Is it true at the beginning? Does it remain true after a step (quite simple path property)?
- same idea, induction on k (why k+1???): Is it true at the beginning? Does it remain true after a step (quite simple path property)?
- Think Reach as a strictly increasing set.
Termination: maybe you can use a quite simple property linked to the diameter of the graph?
(This question could probably be better answered elsewhere, on https://cstheory.stackexchange.com/ maybe?)