Top
User manual for the ACL2 Theorem Prover and
the ACL2 Community Books
Introduction
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 interesting systems in
academia and industry.
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 May 7, 2025 21:22:09. 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!
Subtopics
- 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.
- 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.
- Projects
- The projects directory of the Community Books contains a variety
of projects that have been carried out with ACL2.
- Debugging
- Tools for debugging failed or slow proofs, or misbehaving
functions.
- 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.
