ACL2 Version 5.0

ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models.

ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award.

Start Here: Applications, Tours, and Tutorials/Demos ACL2 Workshops and UT ACL2 Seminar
Books and Papers about ACL2 and Its Applications The User's Manual and Hyper-Card
Lemma Libraries and Utilities Mailing Lists
Recent changes to this page Obtaining, Installing, and License
Differences from Version 4.3 Other Releases
How to contribute libraries and documentation

Matt Kaufmann and J Strother Moore
University of Texas at Austin
August 23, 2012

The ACL2 distribution includes several extensions, which were contributed by the individuals shown.

The distribution also includes libraries of books (files containing definitions and theorems) that extend the code that we have written. Books are contributed and maintained by the ACL2 community (see and their authors are generally noted in each book or its README file. There is a combined manual that incorporates not only The User's Manual for ACL2 but also documentation for many books; thanks to Jared Davis for building this view of the documentation.

Another extension of ACL2 is the Eclipse-based ACL2 Sedan (ACL2s). Unlike the systems above, ACL2s is distributed and maintained by Pete Manolios and his research group. ACL2s comes with a standard executable ACL2 image for Windows, but it also comes with pre-certified books and an extension of ACL2 with additional features, including extra automation for termination proofs as well as counterexample generation.

We gratefully acknowledge substantial support from the following. (These are included in a much more complete acknowledgments page.)

The User's Manual

ACL2's user manual is a vast hypertext document. You can wander through it here, in its HTML format.

Here are the two common entries to the documentation graph:
Major Topics (Table of Contents)
Index of all documented topics
The tiny warning signs, , indicate that the links lead out of introductory level material and into reference manual material. Once in the reference manual, virtually all links are into the manual and none of them is marked with the warning sign! It is easy for the newcomer to get lost.

Here is how we recommend you use this documentation.

If you are a newcomer to ACL2, we do not recommend that you wander off into the full documentation. Instead start with the ACL2-TUTORIAL documentation topic. Experienced users tend mostly to use the ``Index'' to look up concepts mentioned in error messages or vaguely remembered from their past experiences with ACL2.

Note: The documentation is available for reading in a Web browser (recommended), in Emacs Info, using the ACL2 :DOC command, or as a printed book (about 2050 pages). These are available as follows.

Lemma Libraries and Utilities; and, How to Contribute

A companion to ACL2 is the library of distributed books, which have been developed by many users over the years. These books contain definitions and theorems that you might find useful in your models and proofs. The installation instructions explain how to download and install the distributed books. These books include some tools built by users. The above download link will also take you to additional books in support of the ACL2 Workshops (``workshops'') and non-standard analysis (``nonstd'').

We strongly encourage users to submit additional books by following the instructions for contributing books to ACL2.

We also distribute a few interface tools, such as support for infix printing. For these, see the Utilities section of Books and Papers about ACL2 and Its Applications. Some of the papers mentioned in that collection contain utilities, scripts, or ACL2 books the problem domains in question.

How to contribute libraries and documentation

As mentioned above, we strongly encourage users to submit additional books by following the instructions for contributing books to ACL2.

Also, if you have written up (or are interested in writing) text that may be helpful to other ACL2 users, we invite you to contribute it to the community. Such user documentation may be in any format that is readable by web browsers (for example html, pdf, and plain text). User-contributed documentation can link back to the ACL2 documentation proper, by using links such as:
(In general, substitute the upper-case of the documentation topic for "MAKE-EVENT" in the example above.)

To contribute user documentation, send email to the ACL2 developers, for example at