An obligatory mention when we talk about secure operating systems is the seL4 microkernel (https://github.com/seL4/seL4) where they have formally verified every line of code using the proof assistant Isabelle/HOL.
and it's interesting to note that even then, they still had a few bugs here and there due to incomplete / wrong formalisation
The other link provided is a press release in German: http://pressetext.de/news/090817022/sicherheits-beweis-fuer-...
IMHO the reason that few use seL4 is that it isn't ready: AFAIK seL4 isn't able to use efficiently multiple core with power savings, which is mandatory for usage in phones (and phones can use complex CPU with big and little cores).