That&#x27;s interesting work. Hardin is the name that was on the other ones. No surprise they dragged LLVM intermediate form into ACL2 to leverage their prior work. Good that it&#x27;s fast but I&#x27;m more interested in what analysis they can do and how easily. Wish it had more of that.<p>Still added it to my collection as it might come in handy for future ACL2 work. :)