What Is ACL2?

ACL2 is a **mathematical logic** together with a **mechanical theorem
prover** to help you reason in the logic.

The logic is just a subset of applicative

The theorem prover is an ``industrial strength'' version of the Boyer-Moore theorem prover, Nqthm.

**Models** of all kinds of computing systems can be built in ACL2, just
as in Nqthm, even though the formal logic is Lisp.

Once you've built an ACL2 model of a system, you can run it.

You can also use ACL2 to prove theorems about the model.