List of Known Open Proofs
From Openproofs
Contents |
List of Known Open Proofs
Here are some known open proofs:
- Tokeneer is an example proven program, developed by Praxis. The proof itself is FLOSS. It is written in SPARK, a variant of Ada; it can be compiled by GNAT (a FLOSS compiler), and proven using the SPARK tools (released as GPL in June 2009).
- Ivy (proof verifier that has been proved using ACL2)
- Queens on a chessboard with Caduceus (toy size)
We're well aware that the list needs to be longer. Please fill in other known open proofs here!
Potential Open Proofs
General sources
The following should be examined to see if they identify open proofs (note that the proofs and implementations have to be provided, not just described):
- ACL2 publications
- Caduceus/Frama-C/Krakatoa examples
- Pacemaker Formal Methods Challenge
- Verified Software Library (at SourceForge)
- NASA Langley formal methods work
- Secure Microkernel Project (seL4) (need to check licenses, etc.)
FM9001
It seems that the verification of the FM9001 processor may constitute an open proof. The basic idea was that the processor's high-level semantics were formalized in a prover along with a specification in a hardware description language for a gate-level simulator, DUAL-EVAL, which was proven to correctly simulate gate primitives and their formation into more complicated circuits. Ultimately, the main proof was that the state of the processor (flags, registers, memory) when interpreted at the high-level and run for any number of instructions matches the state of the processor when instead first interpreted at the netlist level, simulated for some number of steps, and then interpreted at the user-level. Although the proof was done using the predecessor to ACL2, Nqthm, it is likely that the proof can be upgraded or even that latter efforts along the same lines can be analyzed. Another promising aspect of this effort is that there are further efforts building on this one including a verified assembler and compiler for a Pascal-like language.
The parts of showing this proof is an open proof would likely be:
- Fully packaging ACL2 (which is in progress)
- Ensuring that the associated proofs are runnable in ACL2 (potentially after an upgrade)
- Providing an open tool to examine the produced Network Description Language netlist (as this is the official netlist that was used to manufacture the chip)
- Checking licensing on all appropriate materials. The main distribution of software for the FM9001 has license http://www.computationallogic.com/hardware/fm9001-license.html, so the licensing for at least the FM9001 part is likely not to be difficult
List of Known Proof-Available
- Paul E. Black's Axiomatic Semantics Verification of a Secure Web Server provides a publicly-readable proof of a webserver by Fred Cohen. The webserver is not currently released as open source software, but under an unusual license that is similar to one.
- Compcert verified compiler uses Coq, and some pieces may be FLOSS, but many other pieces are released under a non-commercial license (inhibiting commercial use/improvement).
