Reuse of approved software components has been identified as one of the key factors for successful software engineering projects. Although the reuse process also covers many non-technical aspects we will restrict ourselves to the retrieval of software components (SCR) based on their formal specifications. Our system NORA/HAMMR is based on a library of software components with associated specifications of their pre- and postconditions written in VDM-SL. A query consists of pre- and postconditions pre_q, post_q and the signature of the desired component. Plug-in-compatibility of a library component c is guaranteed, if (pre_q => pre_c) \& (post_c => post_q) can be shown. This "retrieval-by-proof'' or deduction-based approach to SCR has been proposed before but without convincing success. These earlier failures result from the strong application requirements, like critical ("sub-minute'') response times and full automatic processing: the proof tasks must be generated and processed completely automatically as we cannot expect the end-user to cope with ATP details.