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.

Often used in Emacswith Proof General Introduction to ACL2 programming. Computer Aided Reasoning the textbook out of UT, is likely worth spending time reading as well.

Pete's site for Computer-Aided Reasoning lots of good resources for ACL2/S and working with the technology. Add his setup - or some modification of it - to your emacs configuration as a module!