## 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 Common Lisp.

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.