@mattblaze @0xabad1dea I think it's practically ok, we have good human measures in place to avoid such bugs having serious consequences. Of course, on the long run this is a strong motivation to apply serious formal methods to proof assistant kernels, ideally towards full verification!