An interactive theorem prover's kernel is the mechanism used to check that a proof reported as correct has not been accepted due to a mistake.

“The kernel answers the first question anyone asks when they learn about an ITP, which is that if the ITP says a proof is correct, how do I know it hasn't made a mistake?”

“The kernel is how.”