ACL2 is distributed on the Web without fee.
There is a License agreement, which is available via the ACL2 Home Page link below.
ACL2 currently runs on Unix, Linux, Windows, and Macintosh operating systems.
It can be built in any of the following Common Lisps:
* Allegro, * GCL (Gnu Common Lisp), * Lispworks, * CLISP, * CMU Common Lisp, * SBCL, * OpenMCL, and * MCL (Macintosh Common Lisp).