J Moore has been working on computer proof systems for some time, and has built one that he used to prove the AMD K12 architecture correct: http://userweb.cs.ut

J Moore has been working on computer proof systems for some time, and has built one that he used to prove the AMD K12 architecture correct: http://userweb.cs.utexas.edu/users/moore/acl2/acl2-doc.html http://userweb.cs.utexas.edu/users/moore/acl2/acl2-doc.html As a side note, he teaches a good introduction to logic course :)