Using Nqthm, we verified the ``CLI Stack,'' a sequence of four languages and/or computing machines, each implemented atop the previous one.
By composing the verified compiler, assembler and linker we obtain ``verified bits.'' Closely related to the stack is a verified operating system kernel. The CLI Stack work was done in collaboration with Bill Bevier, Bishop Brock, Warren Hunt, Matt Kaufmann, and Bill Young.