Defthm Consulting LLC came into being in 2013 and exists as a mechanism for funding projects of interest to the ACL2 community.  Please contact David Rager ( with any questions you may have.

Thanks to J Moore, Matt Kaufmann, and Bob Boyer for inspiring the name of the company.  And thanks to Pete Manolios for contributing the 2013 slogan: Pain is temporary; theorems are forever.  I like this slogan so much, that I’ve adapted part of it as the website’s motto.