seL4 comes to mind. Also IronFleet[1], which is small but end-to-end verified in Dafny. People tend to verify the cores of complex systems, not the entire thing

seL4 comes to mind. Also IronFleet[1], which is small but end-to-end verified in Dafny. People tend to verify the cores of complex systems, not the entire thing. See here[2] for more on that. I suspect there'd be a lot of stuff using either SPARK or Event-B, but Tokeneer[3] is the only thing I found with five minutes of Googling. [1]: https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/ https://www.microsoft.com/en-us/research/publication/ironfle... [2]: https://www.cs.purdue.edu/homes/pfonseca//papers/eurosys2017-dsbugs.pdf https://www.cs.purdue.edu/homes/pfonseca//papers/eurosys2017... [3]: https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer