> It's interesting (and no coincidence?) that the one caveat with the OK Labs (now General Dynamics) verified micro-kernel was "assuming the hardware satisfies

> It's interesting (and no coincidence?) that the one caveat with the OK Labs (now General Dynamics) verified micro-kernel was "assuming the hardware satisfies its specification". There is also SystemVerilog.