This system is intended for specifying and proving properties of computing machines. It has also been used in several projects (some described here (dead link, 1/15/2007). 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 (A Computational Logic for Applicative Common Lisp) is a theorem prover for industrial Applications. It is both a mathematical logic and a system of tools for constructing proofs in the logic.