The separation core was released (separation kernel) Muen, developed by a Swiss company codelabs.
Muen only supports Intel x86_64 platforms and ensures that OS kernels and applications running on it cannot access resources beyond their allocated quota. This applies, among other things, to RAM, CPU time and access to I/O devices.
The Linux kernel, Ada/SPARK programs, as well as library OSes written using the Solo5 framework (for example, MirageOS on OCaml) are supported as guest applications. Kernel drivers are provided for Linux to speed up access to PCI and other host resources.
Muen itself is entirely implemented in SPARK, a secure subset of the Ada language, and has been verified to be free of runtime errors. The code is distributed under the GPLv3 license.
Source: linux.org.ru