I'm not sure why it doesn't get mentioned a lot. I do know that both LISP and best use of ACL2 (i.e. hardware verification) both get little mention in general. A variant of one to do the other should be similar.

The best work I've seen in ACL2 comes from Rockwell-Collins and their SHADE verification suite. They've verified raw hardware, microcode, processor ISA, security policies, crypto systems... you name it. They give plenty of detail in their papers in how they do that albeit some are paywalled. The resulting AAMP7G processor is used in commercial applications needing reliability and security.

I haven't done a straight survey on ACL2 in a while, though. Might be worth a reader doing and posting in case something interesting was overlooked. Rockwell's stuff seems to be best use of it, though.