We collaborated with the Open Software Foundation Research Institute to test the MK++ microkernel for compliance with its formal specification. For information, please visit our collaborator's project home page.
http://dirleton.csres.utexas.edu/software/os/index.html