I am a world-class expert with the ACL2 theorem prover with years of experience in formal hardware and software verification. For my Ph.D. research at UT Austin, I developed Milawa, a self-verified theorem prover. Today I work full time at Centaur Technology, developing tools and working to analyze our x86 processor. On the side, I do some freelance consulting through my company, Kookamara.