B has been widely used in critical systems in industry, particularly in train control and protection systems and in smartcard applications.
RSDS provides tool support for generating B specifications from statemachine specifications of reactive systems.