ACL2 is a mechanical theorem prover whose underlying logic is based on an applicative subset of Common Lisp. It is also written in the same applicative subset of Common Lisp that it provides and can be run in most Common Lisp implementations. It has a high degree of automation and its specifications can be directly compiled and executed by the underlying Common Lisp implementation. ACL2 is an "industrial strength" version of the Boyer-Moore theorem prover, NQTHM.
For detailed information see:
