This web site is related to the open use of B tools and related documents, in order to improve B dissemination and exploitation.

R&D projects contributing to Atelier B components


ClearSy has decided to release as open-source several of the tools composing Atelier B 4.0, in order to boost B technology dissemination. The reasons for not releasing all tools are as follow:

  • Due to the workload required to have documentation (mostly initially in latex and in French) exposed on the web for international readers (translation in English, pdf or wiki format), the number of open-source projects has been limited. We prefer to concentrate on the central/new tools.
  • BART, B-Compiler, C4B code generator and Atelier B Gui are under development. Designers and developers have an accurate knowledge of these tools and are quite available for writing/contributing to the documentation.
  • These tools are programmed in C++. Other tools like the proof obligation generator, the automatic, interactive and predicate provers, are based on a in-house, prolog-like language (known as “theory language”). As such, finding contributers is certainly trickier.

Releasing other tools as open-source projects could be envisaged in the future upon request. Source code is hosted on Sourceforge.net (see the Tools section for details).


ClearSy plans to release an “official” Atelier B version every 2 years, and intermediate versions regularly. Official versions are available to all, intermediate versions are available to those paying maintenance fees.

Further developments are based on:

  • the Community
  • ClearSy contribution to the tools
  • publically funded projects : funding tool development at regional, national or european level is easier when the tool is (partly) open:
    • Bart development has been funded by French Ministry of Research in the project RIMEL.
    • New proof obligation generator is being funded by French Ministry of Research in the project CERCLES-2.
    • New proof interface to external provers is being funded by French Ministry of Research in the project BWare
  • maintenance fees : ClearSy will provide additional support for error correction, packaqe and release intermediate Atelier B versions (bug correction, improved features, new tools), and provide additional material (tutorials, examples, documentation). Maintenance fees are also a mean for volunteers to support Atelier B development.


Programs are released under GPL v3.0 licence.
Documents are released under Creative Commons Attribution licence.



For any question/comment on this website, please contact us at: open-source@clearsy.com