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

The wikiis an excellent source of information on the language. This workdiscusses the verification of AIG graph representations of boolean functions. This pagehas good programming exercises for ACL2.

ACL2 is often used in Emacswith Proof General