The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

This is an interesting question, and I believe that the answer depends in large part on the proof and its degree of automation. Some proofs may be derivative works while some other would not. But for today's typical proof style, I would argue that yes, formal proofs are derivative work, and the formal proof of a GPL program should also be released under a GPL-compatible license.

## Proofs as derivative work

If we had a magical program verifier, a correctness proof could be as simple as (1) the correctness statement you want to prove, and (2) the invocation of the verifier tactic.

In this case the answer would depend entirely on the correctness statement: if it is just "does not crash", or a generic specification that applies to many programs ("is a sorting function"), this proof would be not be a derivative work of the program. If the toplevel correctness statement depends in a deep way on the internals of the function, and in particular in creative choices that were made during the design of this function, then you may have a derivative.

On the other hand, typical proofs these days are tightly coupled to the source code of the original program. They would not be valid anymore if we changed the source of the original program, especially if we changed the creative parts that carry copyright. For this reason, to me they clearly qualify as a derivative work.

## Citing some copyright law

Wikipedia ( https://en.wikipedia.org/wiki/Derivative_work ) cites this sentence from the US Copyright act:

A work consisting of editorial revisions, annotations, elaborations, or other modifications which, as a whole, represent an original work of authorship, is a “derivative work”.

Of course "formal proofs of program correctness" was not considered when writing these laws (or even software licenses), so we will not find specific wording for this, but I would consider "annotations" or "elaborations" of an original work to adequately-enough capture the relation between a program and its proof.

(It may be the case that reproducing a program for the purpose of a correctness proof would qualify as "Fair use" for US copyright law, which would free you from copyright-related demands of the original work. But this concept is not recognized internationally so I would not recommend relying on it.)

## (L)GPL licensing

To me it is very clear that if a source code is written with the GPL license (v2 or later), then under the terms of the GPL a corresponding correctness proof should also be distributed under a compatible license. I believe that the same requirement would in fact apply if the source code was distributed under the less demanding LGPL license.

The GPL (either v2, v2.1 or v3) and the LGPL are distinguished by how much "coupling" they require between the distributed program and derivative work to demand that the derivative be also distributed under the (L)GPL. For the GPL, basically any dependency on the GPL software specifically (as opposed to a dependency on a generic interface that has other non-GPL implementations) requires that the dependent work be GPL as well. The LGPL allows non-LGPL dependencies, as long as they ( https://www.gnu.org/licenses/lgpl-3.0.en.html )

(b) will operate properly with a modified version of the Library that is interface-compatible with the Linked Version.

It is clear to me that the degree of coupling between a source program/library and its correctness proof, with today's proof style, is much higher than this standard. Most interface-compatible changes (here by interface we mean the interface between the program/library and the rest of its software ecosystem, not between the program and the proof) will make the proof document invalid. So this suggests that even if the source program was LGPL, the proof should also be LGPL.

GPL is designed as a stronger license requiring less coupling, so (to me) clearly correctness proofs of GPL programs should also be GPL.

On Thu, Jul 16, 2020 at 3:37 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

On Wed, Jul 15, 2020 at 1:45 PM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

Another approach would be to ask the owner of the C code whether they have any objection to your publishing the proof.  Seems to me your proving it would make their code more valuable.

The C code is available publically under GPLv2 license. The main question is whether the correctness proof (just the .v file(s) containing the specs and proofs, NOT the code or the .v file containing the code AST) can be released under a different license (possibly incompatible with GPLv2).