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).
[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.
The platform is open source and forms part of the Eclipse framework It is extendable using software component plug-ins.
[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.