The AMULET group at the University of Manchester has spent a decade designing asynchronous microprocessors of increasing performance and complexity. Getting these large designs (almost) right first time is very challenging, and any verification or validation methodologies that can be brought to bear can help improve the design quality as measured by the number and severity of bugs in the final silicon. This paper presents the methodologies used on the first three AMULET processors and describes the problems that escaped detection. The potential and need for improved tools is discussed, as are looming problems with near-future process technologies which will make right-first-time design much more difficult to achieve.