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 the Unix, Linux, Windows 98, and Macintosh operating systems. The changes made to support Windows 98 may well support ACL2 running on other Microsoft Windows platforms; the implementors would be interested in hearing of people's experiences in any such attempts.
It can be built in any of the following Common Lisps:
* Allegro, * GCL (Gnu Common Lisp), * Lispworks, * CLISP, * CMU Common Lisp, * OpenMCL, and * MCL (Macintosh Common Lisp).
We recommend running ACL2 with at least 16MB of memory and prefer significantly more (e.g., 64MB).