I&#x27;ve been wondering for a while, and since this thread seems to have attracted people who may have answers…<p>Can you (or anyone) provide any insight as to why ACL2 doesn&#x27;t get mentioned much in discussions of formal methods? I&#x27;m interested in formal methods and ACL2 seems like a nice tool, but at least on HN all I usually see is Coq this and Coq that, with occasional mentions of TLA+ and Isabelle.