It sure makes auditing that code conforms to an expected design a lot easier, which is most security bugs. This is a fantastic design choice for a security focused kernel.

I will grant that proving something was implemented as designed does not rule out design flaws so, fair enough.