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 OS X operating systems.
It can be built in any of the following Common Lisps:
* Allegro, * GCL (Gnu Common Lisp), * CLISP, * CMU Common Lisp, * SBCL, and * CCL (OpenMCL)