Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong? Anyway, I'm going to read more about what and how they did, it's fascinating to see a non-trivial software system proven correct.
Yes, that's how they did it. Quoting from the paper:
"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."
> Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong?
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.
