本文翻译自2023年HOTOS Conference中的论文–Kernel extension verification is untenable