The specification language B and its successor Event-B are used for the formal development of software and systems following the correct-by-construction approach. Both are based on first order predicate logic with higher-order sets, relations, functions.

B has originally been developed as a successor to Z by Jean-Raymond Abrial in the 1990s, focusing on two key concepts: using refinement to gradually develop models and tool support for proof and model checking. There are three classes of industrial applications of B: - B for software (classical B): refine specifications until B0, a low-level subset of B, is reached and apply code generators - B for system modelling (Event-B): verify critical properties, understand why a system is correct - B for data validation: express properties in B and check data (possibly using a double chain)

We will describe the history of B, starting with B's genesis as a tool for software validation, discussing industrial applications of B in projects such as train speed control and signalling and other projects with RATP and SNCF performed by Alstom, Line 14 (Meteor) or Canarsie. Following, we will focus on the evolution of B into Event-B and from software to systems modelling, again focusing on industrial applications such as the flushing line NY, OCTYS, GIK/Railground, the HL3 standard and cooperations with Peugeot. Additionally, we will discuss ventures of using B in other domains such as smart cards.

Language evolution aside, we want to discuss tool evolution in the B ecosystem. Both B and Event-B are supported by a range of tools, from provers to animators to model checkers. We want to give an overview over the B-method tools currently in use and their development and history, starting with early tools such as the B-Toolkit to Atelier-B and to Rodin for Event-B. As not all tools are still available, we will also discuss the ones that disappeared or never really appeared.