The practical use of formal methods in software engineering (SE) in the light of experience gained from two industrial projects using B abstract language notation will be discussed. The B specifications will be compared with other model-oriented specification methods (VDM, Z, RAISE). Case studies will be described assessing the use of formal specification, refinement, and proof as part of overall system development. In particular, the construction of application-specific theories for balancing automation and interaction in verification of design will be explored.