We adopt an extension of case-base reasoning (CBR) to also include generalised design information in the form of models. We have a repository of models as well as one of cases. We consider the design of the two repositories, the relations within them, and the relations between them. We add a rule language that can be used to check cases and also for retrieval and selection. We use formal specification to capture these data structures, and the meaning of rules, precisely and unambiguously. Formal specification is also a useful abstraction mechanism: we are abstract about the design domain (whose properties are a parameter of the specification), and about the implementation details.