ACL2 is a [theorem prover](id:0999656e-5b44-455f-8c33-bd51b0365b6b) based on Common Lisp commonly used for the verification of hardware.

[The wiki](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____TOP?path=3486) is an excellent source of information on the language. [This work](https://www.researchgate.net/publication/236578406_Verified_AIG_Algorithms_in_ACL2) discusses the verification of AIG graph representations of boolean functions. [This page](https://www.cs.utexas.edu/users/moore/publications/acl2-programming-exercises1.html) has good programming exercises for ACL2.

Often used in [Emacs](id:62a9456a-e08a-4dc4-8e9d-310deffdb720) with [Proof General](http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+user+manual&file=releases%2FProofGeneral%2Fdoc%2FProofGeneral%2FProofGeneral_2.html). 
[Introduction to ACL2 programming.](https://www.cs.utexas.edu/users/moore/publications/gentle-intro-to-acl2-programming.html)
[Computer Aided Reasoning](https://www.cs.utexas.edu/users/moore/publications/acl2-books/car/), the textbook out of UT, is likely worth spending time reading as well.

[Pete's site for Computer-Aided Reasoning](http://www.ccs.neu.edu/home/pete/courses/Computer-Aided-Reasoning/2018-Fall/): 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!