Earlier quoted context omitted.
If you find this amazing, perhaps you should take a look at seL4, which has formal proofs of correctness, going all the way down to the generated assembly code still satisfying the requirements. It also has a much better overall architecture, the best currently available: A third generation microkernel multiserver system. It provides a protected (with proof of isolation) RTOS with hard realtime, proof of worst case t…
Eh, seL4 has a suite of tools that turn their pile of C and ASM into an obscure intermediate language that has some formally verifiable properties. IMO this is just shifting the compiler problem somewhere else, into a dark corner where no one is looking. I highly doubt that it will ever have a practical use beyond teaching kids in the classroom that formal verification is fun, and maybe nerd-sniping some defense weir…
There is also an interesting case study[1][2] where seL4 was shown to prevent malicious access to a drone. Using seL4 doesn't necessarily make an entire system safe but for high security applications you have to build from the ground up and having a formally proven kernel is the first step in doing that.
I have been fortunate enough to play a small role in developing some stuff to be used with seL4 and it's obvious that the team are passionate about what they've got and I wish them the best of luck
0 - https://news.ycombinator.com/item?id=25552222 1 - https://www.youtube.com/watch?v=TH0tDGk19_c 2 - http://loonwerks.com/publications/pdf/Steal-This-Drone-READM...