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.

Often used in Emacs with 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!