B has been used in major safety-critical system applications in Europe (such as the automatic Paris Métro lines 14 and 1 and the Ariane 5 rocket).
Subsequently, another formal method called Event-B[8][9][10] has been developed based on the B-Method, support by the Rodin Platform.
[16] The toolkit uses a custom X Window Motif Interface[17] for GUI management and runs primarily on the Linux, Mac OS X and Solaris operating systems.
[8][21][11] Rodin is based on an Eclipse software IDE (integrated development environment) and provides support for refinement and mathematical proof.
[8] BHDL provides a method for the correct design of digital circuits, combining the advantages of the hardware description language VHDL with the formality of B.