|
|
|---|
|
|
|
|---|
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.
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.