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
As a side note, he teaches a good introduction to logic course :)