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.