Aug 2010 - May 2011. Magnus Myreen has developed a verified Lisp system, named Jitawa, which can run Milawa. Our paper about this project was accepted to ITP 2011:
Magnus O. Myreen and Jared Davis. A verified runtime for a verified theorem prover. Interactive Theorem Proving, August 2011, Nijmegen, The Netherlands.
For more about this project (such as the source code), please see Magnus's Jitawa page and also my Milawa on Jitawa page.
Milawa is a "self-verifying" theorem prover for an ACL2-like logic.
We begin with a simple proof checker, call it A, which is short enough to verify by the "social process" of mathematics.
We then develop a series of increasingly powerful proof checkers, call them B, C, D, and so on. We show each of these programs only accepts the same formulas as A, using A to verify B, and B to verify C, and so on. Then, since we trust A, and A says B is trustworthy, we can trust B. Then, since we trust B, and B says C is trustworthy, we can trust C. And so on for all the rest.
Our final proof checker is really a theorem prover; it can carry out a goal-directed proof search using assumptions, calculation, rewrite rules, and so on. We use this theorem prover to discover the proofs of soundness for B, C, and so on, and to emit these proofs in a format that A can check. Hence, "self verifying."
Milawa is free software released under the GNU General Public License, "version 2 or later."
Milawa has changed since my dissertation; the links and instructions here lead to the most recent version. An archive of the "original" Milawa web site is also available, which for instance includes compressed versions of the original, pre-generated proofs, and full proof-checker output, logs, etc.
A full build includes
You can also browse the file listing from the web server without downloading anything. This listing does not include any of the proof files, certifications, logs, etc., which are available in the archived version, because I am no longer doing my development from this directory.
Contact: jared@cs.utexas.edu
This material is based upon work supported by the National Science Foundation under Grant No 0429591. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Contract NBCH30390004.