[seL4][1] is a formally verified microKernel which is used by billions of smartphones as part of their baseband OS. The part which is completely separate from Android or iOS.
[1]:http://sel4.systems/
I haven't worked with seL4, but used an earlier branch of the L4 family (L4Ka::Pistachio) as a base for a toy OS (university project).
If I had the time to tinker with base OS design today, I'd definitely start with seL4.
Edited to add: the whitepaper here is a good intro to seL4: https://sel4.systems/About/seL4-whitepaper.pdf
oooooh.
It's almost a lame/inane question when framed this broadly, but: where can I read more about similarly incredibly obscure yet Really Important™ applications of technology that have just about completely disappeared into the woodwork?
For example, a quick google search of "how many microcontrollers in a car?" gives 50 as a common answer. For every system that people think about as a computer (entertainment, engine controller, airbags) there are another 10 systems that are also tiny computers that we kind of expect to mostly work together just about perfectly, forever.
Feels pretty obscure and somewhat important, but maybe not incredibly obscure and really important. :/