An "open proof" is software or a system where all of the following are free-libre / open source software (FLOSS):
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 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.
You can see:
- Open Proof FAQ
- Packaging status - We're packaging FLOSS formal methods tools for widely-used systems - please help us!
- List of Known Open Proofs
- Notes for specific implementation languages: Ada | C and C++ | Haskell | Java | Lisp
- Presentations and papers about open proofs
- Current events
- Components that should be Open Proofs
- All content pages on the wiki
Interested in helping?
- What can I do to help? - which notes Components that should be Open Proofs and Packaging status
- Request a Wiki account (you have to have an account before editing the Wiki - this counters spam)
- View or Join the open proof mailing list. You can see the openproofs archive or mail-archive.com's openproofs archive.
- Terms of Service
- Contact the webmasters, David A. Wheeler, at dwheeler at ida dot (org) or Alan Dunn, at amdunn at gmail dot (com).
Our thanks to our Sponsors!
Companies and products are mentioned for information purposes only; no endorsement is implied.