Remember that a few of those RTOS's, although OS itself is C, have runtimes for Ada and Java that apparently sold well enough they continue to be updated. Only RTOS I know still done in Ada is MaRTE OS:

http://marte.unican.es/

Well, Muen is done in SPARK but it's a separation kernel rather than full OS:

https://muen.sk/#_features

That it was integrated into GenodeOS framework shows one could build a system around it but it's not quite one itself. There's also the JavaCard OS's for low-level stuff and even Java CPU's on market.