The runtime verification subsystem

The main advantage of an explicit model is that it will express the kernel's desired behavior. BUG_ON() etc. are needed because the kernel's actual behavior deviates from the model. One can envision a future where a patch that addresses the problem that triggers a backtrace would be required to include a diagram illustrating the deviation from the agreed model. Imagine how much easier such a practice would make reading Linux mailing lists!