User manual for the ACL2 Theorem Prover and the ACL2 Community Books

ACL2 is an
interactive theorem prover. It combines a Lisp-based programming language for
developing formal models of systems with a reasoning engine that can prove
properties about these models. It has been used to formally verify
many

The ACL2 Community Books are the canonical set of open-source libraries ("books") for ACL2. They include lemma libraries for reasoning in many domains, macro libraries for more quickly writing and documenting code, interfacing tools for connecting ACL2 to other systems, productivity tools for better proof automation and debugging, and specialty libraries for areas like hardware-verification.

This manual was generated on **September 25, 2023 19:51:56**. It covers
both ACL2 and the Community Books. It is derived by combining

- the documentation for the ACL2 system itself—mostly written by Matt Kaufmann and J Moore
- the documentation for many Community Books—contributed by numerous members of the ACL2 community

Besides just importing the documentation, we also rearrange the topic hierarchy to try to provide a coherent organization.

This manual is very much a work in progress. If you would like to contribute to its development, please join the acl2 project on GitHub!

- Documentation
- Information about options for downloading and viewing the ACL2 documentation, contributing documentation, and the available tools for documenting your own books.
- Books
*Books*are files of ACL2 events—they are the main way to split up large ACL2 developments into separate modules.- Recursion-and-induction
- Recursion and Induction
- Boolean-reasoning
- Libraries related to representing and processing Boolean functions, geared toward large-scale automatic reasoning, e.g., via SAT solving and AIG or BDD packages.
- Debugging
- Tools for debugging failed or slow proofs, or misbehaving functions.
- Projects
- The
projects directory of the Community Books contains a variety of projects that have been carried out with ACL2. - Std
- Standard libraries for ACL2.
- Proof-automation
- Tools, utilities, and strategies for dealing with particular kinds of proofs.
- Macro-libraries
- Generally useful macros for writing more concise code, and frameworks for quickly introducing concepts like typed structures, typed lists, defining functions with type signatures, and automating other common tasks.
- ACL2
- Documentation for the ACL2 Theorem Prover.
- Interfacing-tools
- Libraries and tools for doing basic
file i/o, using raw Common Lisp libraries, working with the operating system, and interfacing with other programs. - Hardware-verification
- Libraries for working with hardware description languages, modeling circuits, etc.
- Software-verification
- Software verification projects, tools, etc.
- Math
- Math-related libraries: arithmetic, algebra, bit-vectors.
- Testing-utilities
- Tools for developing and running tests.