The formal verification of low-level code is a problem largely ignored by the academic community although it is seen as a major problem in industry. This paper examines the problems associated with verification at this level and describes SPADE-8080, a verifiable sub-language of the Intel 8080. It also shows how programs written in SPADE-8080 can be analysed and formally verified with the SPADE software tools.