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.
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!