There was some discussion on the original post to HN about this announcement. In particular, look at this:

http://ertos.nicta.com.au/research/l4.verified/proof.pml

Which talks about the limits of provability.

In short, a "proof" that contains errors isn't really a proof of anything. And you build your proof inside an automated theorem prover so that it can be mechanically checked for internal inconsistency (i.e. contradictions), or for a completely inability to be false (i.e. tautologies).