The last decade has seen impressive steps towards creating fully verified software systems with formally verified applications, crypto libraries, compilers, operating systems. The foundation on which we are building these towers of verified software is the processor specification that forms the contract between the hardware designer and the programmer.
But can we trust these processor specifications on which we build these soaring towers?
The approach we have taken in creating specifications of ARM processors is to make the specifications useful for many different purposes by different teams. This leads to a virtuous cycle where any bug fixed by one team benefits all users. I will illustrate this by talking about the diversity of uses of the specification: from formal verification of hardware to checking for security holes in new architecture extensions.