I think I read somewhare that the QNX kernel has been logically verified / model checked, but I’m not sure. I cannot find the document…
If this is true, which techniques / algorithms / software have been used for this?
I don’t believe this is true. I do recall a suggestion that the QNX4 microkernel could be verified (i.e. that it was small enough that it was within the realm of possibility).
The QNX6 microkernel is much bigger than QNX4, and I would guess that verifying it would be impractical for any purpose.
I seem to recall having heard that some real-time executives have been formally verified, but a RT executive typically has a microscopically small feature set with respect to the QNX6 kernel.