And as soon as one person makes a commit, that proof is invalid right?
"Note that we have integrated all proofs into an automated proof checking suite, similar to an automated regression-test suite, but using machine-checked formal proofs instead of executable tests. This provides an automatic check, after each commit into the version control system, of the state of all the existing formal proofs, and identifies which specific portions of the proof must be re-established."
Yes, that's the plan.
Internally this is how we have been operating since 2009, when the proof was first completed: You don't push a change to the verified kernel branch unless you are willing (or are able to convince someone else) to do the proof updates.
We don't yet have a regression website publicly available, but it's on the short-term roadmap.
Could you please name the other five?
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.
As others have mentioned, seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement." But for many years it was proprietary, and only available under commercial terms. The paper was published in 2009, so it's been five years that it was proprietary.
As of today at noon, the kernel was released under GPLv2 and userland under two-clause BSD. That is exciting.