There have been a number of OS-type systems in Ada/SPARK, though at least mainly in the embedded space. E.g. the Muen verified separation kernel: https://muen.

There have been a number of OS-type systems in Ada/SPARK, though at least mainly in the embedded space. E.g. the Muen verified separation kernel: https://muen.sk/ https://muen.sk/