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.
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.