Hacker News Reader

The kernel of an automatic proof checker is much easier to test and verify than the programs you verify using a proof checker though.

+1 verification tends to be the easy part.

Sure, not all bugs are kernel bugs though.