The key objective fact to be proven is that the secrecy and integrity of your critical information within a computer is at risk to (relies on) a very small portion of the software that runs on that computer. The typical Keykos application will rely on the kernel, of course, and also several software components outside the kernel. If formal security assurance is required for this application then we must deal formally with the behavior of these additional components.
I resist the project of “implementing Unix within Keykos” for it would probably lead to a situation where applications would typically rely on something like a Unix kernel and I find it unlikely that suitable theorems for Unix exist. The Capsicum project may shed light on this. Also I would rather implement necessary Unix kernel function by small units and connect these units with capability discipline. This will cause Unix bugs but few if any security bugs. In short: I do not understand Unix.