Yes but the spec is often unknown (C language, GCC compiler, Linux) or flawed (speculative execution processors, which we know since Spectre). The fact there i

Yes but the spec is often unknown (C language, GCC compiler, Linux) or flawed (speculative execution processors, which we know since Spectre). The fact there is a formally verified piece of design and software is not bullshit. I said the marketing here is bullshit. This shiny piece of great software won't solve our security problems in multiuser environments, because the proof works only under a very limited set of assumptions. You can't just run your VMs in the cloud on this FV hypervisor and think your software security problems are solved.