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. We
call this process *bootstrapping*.

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 bootstrapping proofs needed to verify B, and to emit these proofs in a format that A can check. We then use it to discover the proof for C, and emit it in a format suitable for B, and so on. In this way, Milawa discovers its own soundness proof, hence "self-verifying".

Milawa was originally developed as part of Jared Davis' Ph.D. dissertation, A self-verifying theorem prover.. The dissertation covers the process described above, i.e., it explains how the question of trusting the prover's tactics may be reduced to that of trusting its kernel. The kernel and its logical foundations are addressed informally but, at some level, its correctness is simply assumed.

More recently, Magnus Myreen has applied ideas from his Ph.D. research to develop and formally verify Jitawa, a Lisp runtime that is capable of running Milawa through its full bootstrapping process. Going further, Magnus has developed a HOL4-checked proof showing that Milawa's kernel is sound when run on Jitawa.

This HOL4 proof, combined with Milawa's kernel's processing of the bootstrapping proofs, yields an impressive result: it establishes the correctness of a heuristic, Boyer-Moore style theorem prover, all the way down to the x86 machine code that runs it.

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

See build for information about how to obtain and build Milawa.

The authoritative description of Milawa is:

Jared Davis. *A
self-verifying theorem prover*. Ph.D. thesis, University of Texas at
Austin, December 2009. Defense
slides. See also errata.

See jitawa for information about Jitawa and the HOL4 verification of Milawa's kernel.

Finally, history takes a look back at the project's timeline, and how things went.

- Jared Davis.
*The Milawa rewriter*. Unpublished. October 5, 2007.

and an ACL2 proof of its soundness - Jared Davis.
*A trustworthy, extensible theorem prover*. Ph.D. dissertation proposal. October 22, 2007. Also a technical report: The University of Texas at Austin, Department of Computer Sciences, Report #TR-08-14, March 2008. See also the slides from the proposal talk. - Jared Davis.
*The Milawa rewriter and an ACL2 proof of its soundness*

Slides from the ACL2 Workshop 2007. November 16, 2007. - Jared Davis.
*Tactics and tracing*. Slides from an ACL2 Seminar talk, March 28, 2007. - Jared Davis.
*Adding a computation rule*. Slides from an ACL2 Seminar talk, August 2, 2006. - Jared Davis.
*Milawa: an extensible proof checker*. Slides form an ACL2 Seminar talk, November 16, 2005.

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.

- Final-checks
- How to build the Milawa kernel on your choice of Lisps, and use it to check the proofs produced by the bootstrapping process.
- History
- A short history of Milawa's development, merely for posterity.
- Build
- Instructions for obtaining and building Milawa.
- Jitawa
- Jitawa is a Lisp runtime developed by Magnus Myreen that is capable of running the Milawa kernel and checking through the entire bootstrapping process, and which is verified down to the machine code with HOL4.
- Errata
- Errata for
*A Self-Verifying Theorem Prover*. - Jitawa-checks
- How to do the final-checks using jitawa as the host Lisp, instead of a Common Lisp system.