PikeOS is a proprietary variant in the L4 microkernel family (see Figure 1 in [1], and [2]). Open source variants include the more well-known seL4 [3] and L4Re

PikeOS is a proprietary variant in the L4 microkernel family (see Figure 1 in [1], and [2]). Open source variants include the more well-known seL4 [3] and L4Re [4]. The L4 family is known for formal verification of significant parts of the system, and is used in safety-critical systems [5]. Google recently announced a system based on seL4 [6]. [1] https://sigops.org/s/conferences/sosp/2013/papers/p133-elphinstone.pdf https://sigops.org/s/conferences/sosp/2013/papers/p133-elphi... [2] https://docs.sel4.systems/projects/sel4/frequently-asked-questions https://docs.sel4.systems/projects/sel4/frequently-asked-que... [3] https://github.com/seL4/seL4 https://github.com/seL4/seL4 [4] https://github.com/kernkonzept/l4re-core https://github.com/kernkonzept/l4re-core [5] https://www.youtube.com/watch?v=ijTTZgQ8cB4 https://www.youtube.com/watch?v=ijTTZgQ8cB4 [6] https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html https://opensource.googleblog.com/2022/10/announcing-kataos-...