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.
