[daveasdf]

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