ACL2 Version 2.9 ACL2 is both a programming language in which you can model systems and a tool to help you prove properties of those models. lispWelcome to the ACL2 home page! We highlight a few aspects of ACL2: Libraries (Books). Libraries of books (files containing definitions and theorems) extend the code that we have written. In particular, the distribution tarball includes the community books, which are contributed and maintained by the members of the ACL2 community. Documentation. There is an extensive user's manual for the ACL2 syst
