Hey, there's more than one way to overflow an integer!

Trivially true things cannot depend on "fairly obvious" observations. In fact you cannot reason locally here: you must understand the whole code to convince yourself that it does not overflow. Consider an off-by-one error, like replacing line 318 with:

   s=&tail[0..];

and now base will overflow.

Anyways the point of formal methods is to give yourself something better than "read carefully" to convince yourself of correctness.