> If you mean you want it to be automated ACL2 is an alternative that strives to strike a balance between interaction and automation. - It is more automated t

> If you mean you want it to be automated ACL2 is an alternative that strives to strike a balance between interaction and automation. - It is more automated than any of the interactive theorem provers including Isabelle/HOL, Coq, etc. - Its authors received the ACM software system award in 2005. -It is used in commercial products since several years in companies including AMD, Centaur , Rockwell Collins, etc. There is a not-so comprehensive but yet impressive list of applications here: http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html http://www.cs.utexas.edu/users/moore/publications/acl2-paper... - Also, since the language is a subset of Common-lisp, any one who knows a bit of programming can very quickly start using ACL2. One does not need to learn type theory/logical formalism to start using it. It has an eclipse plugin that is used by first and second year undergraduate students (http://acl2s.ccs.neu.edu/acl2s/doc/ http://acl2s.ccs.neu.edu/acl2s/doc/).