A few OS's and a micro-hypervisor done in Ada or SPARK including a high-assurance, secure kernel for Ada apps with strong isolation and leak resistance. Given i

A few OS's and a micro-hypervisor done in Ada or SPARK including a high-assurance, secure kernel for Ada apps with strong isolation and leak resistance. Given its main domain, Ada is often used to write bare metal with no OS or for the app (not OS) in a runtime on top of a RTOS. They're usually C and/or assembly since those are dominant for OS work. https://www.muen.sk/ https://www.muen.sk/ https://marte.unican.es/ https://marte.unican.es/ https://en.wikipedia.org/wiki/BiiN https://en.wikipedia.org/wiki/BiiN https://apps.dtic.mil/dtic/tr/fulltext/u2/a340370.pdf https://apps.dtic.mil/dtic/tr/fulltext/u2/a340370.pdf https://www.researchgate.net/publication/220713695_Specification_and_Verification_of_the_ASOS_Kernel https://www.researchgate.net/publication/220713695_Specifica... Note: This one is also downloadable on ACM or IEEE. I got it off of one of them. Has good example of Gypsy language for verifying systems.