Atelier B

Atelier B is the industrial toolset for the B method, developed and maintained by ClearSy. It provides an integrated environment for writing B specifications, generating proof obligations, and discharging them through a combination of automatic and interactive theorem proving. Atelier B translates abstract machine specifications into proof obligations — logical formulas that must be established to verify that a refinement preserves the behavior of the original specification. The tool handles the syntactic and proof-management burden that would otherwise make B impractical for large-scale development. It has been used in the verification of railway control systems, including the driverless Paris Métro Line 14 and several European signaling projects. Atelier B demonstrates that formal methods live or die by their tooling: a beautiful refinement calculus without mechanical proof support is a theory, not an engineering practice. The tool remains one of the few examples of a formal method integrated into a genuine industrial workflow, rather than confined to research demonstrations.