Just glancing at their site, I suspect it's real, however, I doubt it's interesting to us except as an academic example: Only open source code I could find (an

Just glancing at their site, I suspect it's real, however, I doubt it's interesting to us except as an academic example: Only open source code I could find (and it's not linked from their site that I could find) is here, it's tooling: https://github.com/CertiKOS https://github.com/CertiKOS For Coq, which is the proof system they use, but also for extending the CompCert verified C compiler, which requires a commercial licence if you use it beyond "evaluation, research and education purposes". And given the domain, and of course you have to talk to a salesman, I'm sure it's not cheap, 6 figures a seat in USD would not be out of the question if not likely, I'm sure it's 5 figures at minimum. This is in part because this sort of software is inherently more expensive, and for the people who really need to use these sorts of tools, like those building airplanes, it's cheap at the price. But by basing it on CompCert, they've got what's likely to be a very high floor for playing the game they've not (yet) invited us to. By comparison, seL4 is now totally free (well, GPLed, but that's not a problem for software like it), and part of that is because they actually tried CompCert, but there was an impedance mismatch in connecting it to their higher level stuff, so they went with Magnus Myreen and his approach of analyzing (GCC produced in this case) binary code and connecting that to the higher level proofs.