In other words, you believe that Kaspersky OS has its place and future market? > Anything IoT needs a full network stack at least ... My point really is, ever

In other words, you believe that Kaspersky OS has its place and future market? > Anything IoT needs a full network stack at least ... My point really is, every IoT device would need only its part of the full network stack, not all the protocols currently implemented in, say, Linux, and chances are, some device will require extremely reduced subset of the network stack, especially at the lower layers and with respect to kernel interaction. I am not a verification expert, but verifying a very reduced subset of a well-defined specs seems at least feasible -- how would we verify something open-ended? Those pesky little theorems would become much more general and would come in even greater numbers? Verifying a generic OS, good for all devices and all application, if at all doable from theoretical standpoint, looks too much of work for no particular profit for the verifier (very similar to the validation of the Linux kernel which is relayed on to the distro builders). I wouldn't be as pessimistic either about the hardware vendors. After all, (some of them) already use formal verification in (some of) the silicon design, and verifying closer to the silicon seems simpler -- the closer to the metal the less genericity (assuming the verified silicon underneath).