Main Page

From Openproofs

Jump to: navigation, search

 

An "open proof" is software or a system where all of the following are free-libre / open source software (FLOSS):

  • the entire implementation
  • automatically-verifiable proof(s) of at least one key property, and
  • required tools (for use and modification)

Something is FLOSS if it gives anyone the freedom to use, study, modify, and redistribute modified and unmodified versions of it, meeting the Free software definition and the open source definition.

News:

 

This site, http://www.openproofs.org, is dedicated to defining and encouraging the development of open proofs and other publicly-available proofs of software/system implementations. Open proofs can aid software developers, tool developers, users, and teachers. This encouragement includes packaging supporting tools, coordinating the development of open proofs, and identifying existing open proofs or the tools to help create them. Open proofs will encourage the maturation and application of formal methods.


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; one reason is 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. For example, many of the tools are hard to use, or scale poorly, in part because without examples it's difficult to improve the tools.

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

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

What's Here?

You can see:

Interested in helping?

Please see:

Our thanks to our Sponsors!

Companies and products are mentioned for information purposes only; no endorsement is implied.

Personal tools