ACL2

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!