So this operating system has 'flawless operation'. I take it the C compiler has ...

		abdulhaq on Aug 13, 2009 \| parent \| context \| favorite \| on: World’s first formal machine-checked proof of a ke... So this operating system has 'flawless operation'. I take it the C compiler has also been verified, then, not to mention the cpu microcode.