ACL2 doesn't get a lot of love from the side of the verification community that focuses on the proof systems that are more academically popular (HOL family, CIC family, etc.). A lot of interesting industrial work has been done with ACL2 and related systems.

▲

Animats 3 days ago | parent [-]

Yes. Been there, done that, with the pre-ACL2 Boyer-Moore prover. We had the Oppen-Nelson prover (the first SAT solver) handling the easy stuff, and used the Boyer-Moore prover for the hard stuff. Not that much manual work.

	▲	porcoda 3 days ago \| parent [-]
		I assume you mean first SMT solver when you refer to Oppen-Nelson? I thought their contribution was the basis for SMT methods.