		Search-engine friendly clone of the ACL2 documentation.

Community

How to join the ACL2 Community.

ACL2 has an active user community that welcomes new users. There are several ways to get involved.

GitHub Project

ACL2 is developed via the ACL2 GitHub project, which also contains the ACL2 libraries maintained by the community (see community-books). The GitHub repository is very active, with thousands of commits per year. Users are invited to contribute new developments, usually in the form of new books (collections of definitions, proofs, etc.), so that the community can benefit from them. Collaboration occurs via Pull Requests and GitHub Issues. See also git-quick-start.

Mailing Lists

We maintain several mailing lists for ACL2 announcements, discussions, and questions. See this page.

Zulip Chat

Zulip is a chat application similar to Slack. We use it to discuss many ACL2 topics and to help each other with ACL2 issues. It is accessible at this page or via the Zulip desktop or mobile app. Email Eric Smith at eric.smith@kestrel.edu for an invitation. As an anti-spam measure, please include in your email a sentence or two about how you heard about ACL2 and/or how you plan to use it.

ACL2 Workshops

ACL2 users gather to present their work at the ACL2 Workshops, which have taken place approximately every 18 months since 1999. See this page for more information.

The 100 Theorems page

We maintain a list of the theorems from the Formalizing 100 Theorems page that have been proved in ACL2. See 100-theorems. Users are invited to attempt to prove additional theorems from the list, though this may be challenging!