On 23 Jan 2020, at 14:02, Heiser, Gernot (Data61, Kensington NSW) <Gernot.Heiser@data61.csiro.au> wrote:

On 23 Jan 2020, at 13:08, Demi M. Obenour <demiobenour@gmail.com> wrote:

Would you be willing to accept PRs that include the corresponding
changes to the proofs, or which don’t affect verification?

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.

Because CLA sounds scary: Currently we still have the CLA process, but we’re hoping to move to something simpler and less legalistic in the future: a Developer Certificate of Origin [see e.g. https://julien.ponge.org/blog/developer-certificate-of-origin-versus-contributor-license-agreements/].This is exactly the process that Linux uses for contributions.