As someone who doesn't quite get all this, isn't the proposal here just checkers all the way down?

The proposal is that multiple checkers are unlikely to all have the same bugs so the more kernels you can use to check the results the more likely it is that the proof/code is consistent & correct (modulo set theoretic assumptions necessary for the correctness of the kernel).