Comment by andor

1) The halting problem only states that you cannot create a program that can decide whether any given program will finish. It is possible for special cases, though.

2) They didn't automatically verify the kernel. Coq is a proof assistant.