> The practical consequence: checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on it need current versions of both.
Things like this aren't too surprising, given that even much simpler type checkers like Rust's have soundness issues occasionally. I think it's very important to view verified results not as an absolute and unbreakable guarantee, just an extraordinarily strong one where (1) the surface area for soundness issues has been painstakingly minimized and (2) any realized soundness issues are taken very seriously and fixed in short order.
The implementation of the kernel is relatively trivial, it's an intentional design choice.
As claude would say, "relatively" is carrying a lot of weight in that frase. Definitely load-bearing — would not pass a quick smoke test.
[dead]