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