(Is it that you don't know of any yourself? Or that you think I can't provide examples? In what world is what I said even slightly controversial? Type checking is just catching on now, decades after it was invented and implemented. C'mon.)

Anyway, off the top of my head, Ada.

https://en.wikipedia.org/wiki/Ada_(programming_language)

and E...

https://en.wikipedia.org/wiki/E_(programming_language) https://en.wikipedia.org/wiki/CapROS

Qubes and SEL4 are Operating systems. (OK Labs was acquired by General Dynamics. That seems like a pretty good recommendation to me.)

https://en.wikipedia.org/wiki/Qubes_OS

https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...