## 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.
(This link takes you off the main route of the tour. You'll see some Common
Lisp on the tour, so visit this later!)

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.