The actions taken by software should be consistent with relevant constraints arising in the real world. For example, computations should not mix values that are understood as being expressed in incompatible physical units. To enable checking of such consistency our previous work introduced: (a) a new structure, the interpreted formalism, that is a software analog of the notion of an informal interpretation from classical logic, and (b) a practical implementation of the concept in the form of real- world type systems. We reported preliminary results of the value of interpreted formalisms in improving software dependability. In this paper, we present details of a new case study, the results of which indicate that: (a) interpreted formalisms can be applied to large systems, and (b) the fault-detection potential is substantial.