People have been talking about this stuff for decades. I found a paper from 1975 right in the top of my search results: http://csrc.nist.gov/publications/history/neum75.pdf. That eventually became PSOS.

There was also KSOS which had formal proofs both of the design and that the code conformed to the design.

There is a whole batch of TE based kernels that are descendants from Secure Ada Target/FLASK: SCOMP, LOCK, DTOS, Trusted MACH, TrustedBSD, and of course Sidewinder made a big deal about their firewalls using a provably secure kernel which was based on that work. The NSA even opensourced the Tokeneer project: http://www.adacore.com/sparkpro/tokeneer

Then there is MITRE, UCLA's DSU, AIM, etc.

I could swear there was at least once SELinux vendor that claimed it was providing the "only" provably secure kernel.

There was also HYDRA...

Anyway, there are lots.