Open Proofs

The problem:

The world depends on having secure, accurate, and reliable software - but most software isn't. In some circumstances we need "high confidence" (aka "high assurance") software built on top of verified software. Verified software, in this context, is software that has been proved to have or not have some property using formal methods (formal methods apply mathematical techniques to prove properties of software). Yet developing verified software is currently very difficult to do, or improve on, because there are few fully-public examples of verified software. Verified software is often highly classified, sensitive, and/or proprietary. This lack of detailed examples impedes progress by software developers, tool developers, users, teachers, and even current practitioners.

Unlike a mathematical proof, software normally undergoes change due to changing conditions and needs. So just publishing unchangeable software, with an unchangeable proof, isn't enough. Instead, we need a number of "open proofs".

The solution:

"Open proofs" solve the problem by releasing implementation, proofs, and tools as FLOSS. With such rights, developers can build on the examples to build larger works, teachers and students can use the examples for learning and research, users can verify that the proof is valid, and tool suppliers can use real examples to improve tools. Both realistic examples (for building on and tool development) and small examples (for teaching) are needed.

Not all systems need to be revealed to the public, but we need public examples as "seed corn" to develop more verified software. To be high assurance, such software would need to come with some automated test suite, but that isn't a strict requirement to be an open proof.

Open proofs do not solve every possible problem, of course. For example: (1) the formal specification might be wrong or incomplete for its purpose; (2) the tools might be incorrect; (3) one or more assumptions might be wrong. But they would still be a big improvement from where we are today. Many formal method approaches have historically not scaled up to larger programs, but open proofs may help counter that by enabling tool developers to work with others.