Milawa is an automated theorem prover for an ACL2-like logic. It features a small trusted core and "self-verified" extensions. Milawa is free software released under the GNU General Public License, "version 2 or later."
NOTE: Milawa is still in early development and is not yet ready for any serious use. As a result, there are no nice packages. However, anonymous subversion access is available; you can "svn checkout" the current version from:
svn://nemesis.cs.utexas.edu/u/jared/Subversion/Milawa/trunk
You can also browse the file listing from the web server.
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.