ACL2 is distributed on the Web without fee.
There is a license agreement based on the 3-clause BSD license. See the file LICENSE in the ACL2 distribution.
ACL2 currently runs on Unix, Linux, Windows, and Macintosh OS X operating systems.
It can be built in any of the following Common Lisps:
* Allegro Common Lisp, * CCL (formerly OpenMCL) * CLISP, * CMU Common Lisp, * GCL (Gnu Common Lisp), * LispWorks, and * SBCL (Steel Bank Common Lisp)
