I tried to read the wiki article on PikeOS, but apparently it too is a written ad seemingly from sysgo. Anyone with any knowledge and not their marketing department to key us in? I'd welcome words from people there who are not in marketing.

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-elphi...

[2] https://docs.sel4.systems/projects/sel4/frequently-asked-que...

[3] https://github.com/seL4/seL4

[4] https://github.com/kernkonzept/l4re-core

[5] https://www.youtube.com/watch?v=ijTTZgQ8cB4

[6] https://opensource.googleblog.com/2022/10/announcing-kataos-...