> I sear this is like the sixth distinct solution I've seen claiming to be the first of those...

Could you please name the other five?

I'm not so good at names. Let's see if Google can help me...

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.