WARNING: ARCHIVE VERSION

Milawa has changed since my dissertation. The current version can be found here. This page is a "snapshot" of how the original web site looked, mostly. (I screwed up the file listing slightly by svn updating to revision 507, but otherwise things are unchanged.)

Milawa

What is Milawa?

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 that each of these is sound: they accept only the same formulas as A. We use A to verify B, and B to verify C, and so on. Then, since we trust A, and A says B is sound, we can trust B, and so on for C, D, and 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."

Getting Milawa

There are two options.

A full build includes

  1. An ACL2 sketch of Milawa's soundness proof
  2. A user interface for developing Milawa proofs and translating ACL2 proofs into Milawa
  3. Bootstrapping to use Milawa to discover its soundness proof

Alternately, you can check the proofs without doing a full build, by downloading pre-generated proofs. Note that this gives you no interface for constructing your own Milawa proofs.

You can also browse the file listing from the web server without downloading anything.

Milawa is free software released under the GNU General Public License, "version 2 or later."

Main Documentation

Older Papers

Older Talks

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.