RTEMS is one and there is also eCOS. RTEMS has flown in space a few times so it is proven.

Forgot to mention: the neat part of RTEMS is it allows one to sort of turn a Unix program into a bare metal program.

I believe seL4 is formally verified.

chibios is great, but I haven't followed their culture or licensing in a few years now.

my experiences then would lead me to recommend it, though.