In this case, exactly what does "mathematical rigour" mean? I imagine there are several responses to this question, but even a conceptual overview of how math can prove bug-freeness would have been nice.
The safety properties might be things like who can write to what memory, and when it is acceptable for bits of the kernel to do certain things. Lock freedom in scheduling is probably also a big thing. I haven't looked at any of this very closely, but I'm just guessing based on the sorts of properties I would try to prove initially.
And no project is ever without such assumptions. You can't have abstractions without them.
Some may argue that there's no guarantee that such proofs apply to real world systems. But really, there's no guarantee that any abstract model does. We humans have to get paid for something.
I would argue that those who would argue that have probably not spent a lot of time doing any real-world formal verification.
People seem to like arguing about its utility in the abstract without ever doing it.
In short: most of the objections people have to formal verification also apply to modeling something in software to begin with.