> Proof assistant kernel, not operating system kernel

It's the neologism they use to own the word and define it however they want. The other one is 'harness' that I didn't even click to see what they want it to mean.

I mean it's an old term in algebra/analytics that predates sytem-kernels by 50 years or so. And even in the meaning compute/solver/gpu-kernel, even thuough predated by systems kernel, it has still been in use at least 30 years.

So proof kernel is not that far fetched, I think. I only skimmed the article though ... so not saying if it was good use here or not.