Main Page
From Openproofs
An "open proof" is software or a system where all of the following are freelibre / open source software (FLOSS):
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 publiclyavailable 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 fullypublic 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:
 Open Proof FAQ
 Packaging status  We're packaging FLOSS formal methods tools for widelyused 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?
Please see:
 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 mailarchive.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.