This system is intended for specifying and proving properties of computing machines. It has also been used in several projects (some described here). A listing of publications about ACL2 can be found here.) for modeling and proving properties of **commercial microprocessor products** by Motorola, AMD, Rockwell Collins, and IBM.

ACL2 works with GCL, CMUCL, CLISP and a number of commercial Common Lisp systems. Source code distributed under the terms of the GPL, and a lot of documentation, are available at the project page.

It can be used with a web interface: proof-pad.

Theorem Provers