Proof assistant kernel, not operating system kernel - in case, like me, you clicked in hoping to debate the merits of microkernels vs monolithic:) Although I suppose there is a significant analogy, since the argument here... if I understood right... is very close to the classic 'and now a small defect in a device driver just panicked the system or gave an attacker root', just in math terms.

Here is the postmortem of the lean bug: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...

Previous related discussion: https://news.ycombinator.com/item?id=49137060