Download Atelier B

 Atelier B Support & Maintenance


The Atelier B V4 is distributed free of charge, through its Community Version, to all those who wish to use Atelier B for research, teaching and development of their industrial projects. As soon as the tool is used for the first time it is allocated for an unlimited time.

The atelier B V4 comprises all the tools required for developing an industrial project and is available in WINDOWS, MAC and LINUX.

Users, companies and research or teaching organisations can subscribe to a maintenance contract for the latest version (corrective or with new functional features). The licence contract supplied with Atelier B can be obtained upon request, in French and English, at atelierb (at) clearsy (dot) com .






  • Atelier B now supports macOS 11.0 « Big Sur »
  • The addition of an extensible mechanism allowing the integration without recompilation of external provers (CVC4 and Z3 by default), in order to improve the automatic proof performance. This version is used industrially by Alstom, RATP and Siemens Transportation Systems.
  • Improved support for event-driven B for Common Criteria certification
  • Several improvements for both the automatic and interactive prover UI
  • New options to particularize the behaviour of the new proof obligation generator
  • Event-B manual available in the Help/Manuals section


  • Atelier B CSSP: B modelling and application programming for CLEARSY Safety Platform starter kit SK0
  • Atelier B now supports macOS 10.15 « Catalina »
  • Interactive proof
    • Saved proofs can now be replayed until the first failing command
    • User pass can now be saved in the patchprover file
  • Project management
    • Improvement of the use of MANIFEST
    • MANIFEST files can now be used through the console
  • Translator
    • C4B: add the translation of tables indexed by an enumeration.
    • B2C: control on table initialization
  • Proof drudge
    • Use of real numbers
    • It is now possible to add only rule validated by PP
  • NPOG
    • Event-B: add the WITNESS keyword
    • Consolidation of PO generation
  • Addition of the proof obligation generator parametrization manual


  • Simplified installation with Linux (Universal Installer)
  • For Event-B, specific proof obligations may be generated by the new proof obligation generator: deadlock freeness, non-divergence, feasibility, coverage and exclusivity
  • Interfacing tool « IAPA » (Linux only) to connect with provers from Why3 platform
  • Interactive proof
    • New feature to use SMT solvers to define proof rules applying to the current goal
    • New feature to add its own groups of proof commands
    • Improvement in typing of proof commands
    • C4B code generator now supports arrays indexed by enumerated type variables


  • Proof obligations displayed in the model editor.
  • A new proof command at for Apply Tactic.
  • A configurable timeout for the pp family proof commands.
  • New functionalities for the Proof Rules Validator.


  • Checking of coding rules inside B models.
  • Integration of ProB model-checker inside the interactive prover interface


  • Full 64-bit support
  • A new traceable, generic, proof obligation generator
  • A better integration of real and floating point numbers
  • Accessors added to BART in order to solve refinement conflicts
  • Boolean and integer translation fine-tuning in C4B code generator
  • Addition of a proof server, in order to speed up proof


  • Improved support of integers : maximum implementable value (MAXINT) can be 16, 32 or 64 bit-wide, integer literals are not bounded (BigINT)
  • Experimental support of real numbers
  • Experimental support of floating point numbers
  • Support of hexadecimal literals.
  • New C code generator, C4B, with translation profile and makefile creation.
  • Localization of the software in English, French, Japanese, and Portuguese.
  • Support of Unicode. Strings and comments may contain non-ASCII characters.
  • Addition of a components status graphical view
  • Parallel execution of proof tasks
  • Improved Integrated Editor
  • The interactive prover displays pending goals
  • Generation of coverage and exclusivity proof obligations
  • Tool for validating user added mathematical rules
  • Spell-checking B model comments
  • Mathematical rules displayed in the view “Theory List” are sorted according to their applicability
  • B model editor informs the user when the edited file has been modified on the disk.
  • Addition of a search function “à la grep”
  • Added rules when using the command “pc” are now displayed.

More informations about "Atelier B Support & Maintenance"