Installing ACL2
See the installation-instructions for steps to install ACL2.
If you encounter problems installing ACL2, or need more information, see installation-support.
See copyright for information about copyright, license, and authorship of the ACL2 system, and see acknowledgments for sponsorship information.
For a variant of ACL2 that supports reasoning about the real numbers, see real.
See mailing-lists for information about mailing lists for ACL2 users, including how to post and how to access archives.
ACL2 may be exported to any countries except those subject to embargoes under various laws administered by the Office of Foreign Assets Control (“OFAC”) of the U. S. Department of the Treasury.
For more information about getting started with ACL2, see start-here. Also see using-ACL2 for information about running ACL2 and about its documentation.