PRs that don’t affect verification will be accepted subject to standard quality control (and availability of a CLA). These are not frequent, but happen. Typically they are platform ports.

One of the things we’d like to set up is a way for developers to check this for themselves, which should certainly help contributions. Not sure when this will be ready.

The same applies, in principle, to PRs that come with proof updates. We haven’t seen one of these yet. 

The bar will be higher if the change affects kernel semantics (even if accompanied by proof), as we need to ensure that the design stays clean and principled.

Gernot