ACL2 is a logic and programming language in which you can model computer
systems, together with a tool to help you prove properties of those
models. "ACL2" denotes "A Computational Logic for Applicative Common
Lisp".

ACL2 is part of the Boyer-Moore family of provers, for which its authors
have received the 2005 ACM Software System Award.

This package installs the main ACL2 executable acl2, as well as the
build tools cert.pl and clean.pl, renamed to acl2-cert and
acl2-clean.

The community books are not included in this package.

Acl2