ACL2 is a theorem prover based on Common Lisp commonly used for the verification of hardware.

The wiki is an excellent source of information on the language. This work discusses the verification of AIG graph representations of boolean functions. This page has good programming exercises for ACL2.

ACL2 is often used in Emacs with Proof General.