Proving the correctness of a square summing algorithm
Assuming $n ≥ 0$, 
let $$ P(n) \;≡\; ∀ a.\, sumHelper(n, a) = a + ∑_{i = 0}^n i² $$

Then we prove this is always true by induction on $n$.

The base case, n = 0:

  sumHelper(n, a)
={ Case n = 0 }
  sumHelper(0, a
={ Definition }
  a
={ Arithmetic }
  a + 0²
={ Arithmetic }
  a + ∑_{i = 0}^0 i²
={ Case n = 0 }
  a + ∑_{i = 0}^n i²


The induction step, assuming P(n) let us show P(n+1),

 sumHelper(n+1, a)
={ Definition }
  if   (n+1==0) a  
  else sumHelper(n+1-1, a + (n+1)*(n+1))
={ Since we assumed n ≥ 0, we have n+1 ≠ 0.
   Hence we have the else-branch. }
  sumHelper(n+1-1, a + (n+1)*(n+1))
={ Arithmetic }
  sumHelper(n, a + (n+1)*(n+1))
={ Apply the inductive hypotheis with a ≔ a + (n+1)*(n+1) }
  (a + (n+1)*(n+1))) + ∑_{i = 0}^n i²
={ Arithmetic: Bringing the `n+1` term back into the sum }
  a + ∑_{i = 0}^{n+1} i²


We're done :-)