**June 2015.** Our final, comprehensive Milawa/Jitawa paper is now available
in the Journal of Automated Reasoning!

Jared Davis and Magnus O. Myreen.The reflective Milawa theorem prover is sound (down to the machine code that runs it). Journal of Automated Reasoning. June, 2015. Springer. (official version / pre-print version).

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—and more recently with a theorem prover
for a more expressive logic. 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."

When I wrote my dissertation, that was the story. Since then,
Magnus Myreen has developed
Jitawa, a verified
Lisp runtime that is capable of hosting Milawa and running through its
entire bootstrapping process. Magnus went on to prove, using HOL4, that
Milawa is *sound all the way down to the machine code*
when run on this Lisp. For more on this project (including source code), see
the Magnus' Jitawa page and also my
Milawa on Jitawa page.

Milawa is free software released under a permissive MIT/X11 style license.

The current version of Milawa is now distributed as part of the
ACL2 Books project.
See the `books/projects/milawa` directory and also see the
Milawa XDOC
documentation.

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.

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.

- Jared Davis and Magnus O. Myreen.
**The reflective Milawa theorem prover is sound (down to the machine code that runs it)**. Journal of Automated Reasoning. June, 2015. Springer. (Official version (Springer) / Author's pre-print version) - Magnus Myreen and Jared Davis.
*The reflective Milawa theorem prover is sound (down to the machine code that runs it)*. In ITP 2014. July, 2014. Springer, LNCS 8558. Pages 421-436.

**Note:**You may prefer the more comprehensive 2015 JAR paper above.

Slides from my July 2012 talk at Northeastern University - Magnus Myreen and Jared Davis.
*A verified runtime for a verified theorem prover*. ITP 2011.

*A self-verifying theorem prover*

Ph.D. thesis, University of Texas at Austin

December 2009.

PDF paper, 2 MB

Errata*A self-verifying theorem prover*

Ph.D. defense

September 18, 2009

PDF slides; 352 KB

*The Milawa rewriter*

and an ACL2 proof of its soundness

Not published

October 5, 2007.

PDF paper, 202 KB*A trustworthy, extensible theorem prover*

Ph.D. dissertation proposal

October 22, 2007

Screen version (PDF, 305 KB)

Print version (PDF, 305 KB)

(Also a technical report: The University of Texas at Austin, Department of Computer Sciences, Report #TR-08-14, March 2008. [link])

*The Milawa rewriter*

and an ACL2 proof of its soundness

PDF slides; 580 KB

November 16, 2007 (ACL2 '07)*A trustworthy, extensible theorem prover*

Ph.D. dissertation proposal

PDF slides; 961 KB

AVI movie with commentary; 16 MB, 19 minutes

October 24, 2007*Tactics and tracing*

PDF slides; 550 KB

ACL2 seminar, March 28, 2007*Adding a computation rule*

PDF slides; 387 KB

Also available as a WMV movie; 88 MB, 67 mins

ACL2 seminar, August 2, 2006*Designing a trustworthy, extensible theorem prover*

PDF poster; 350 KB

Gradfest, March 2006*Milawa: an extensible proof checker*

PDF slides; 760 KB

ACL2 seminar, November 16, 2005

Contact: jared.c.davis@gmail.com

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.