Publié le 20/01/2022 |

Atelier B 4.7.1 is available in a Community Edition ( and in a Maintenance Edition for owners of a maintenance contract.

The main innovations consist in:

  • the addition of an extensible mechanism allowing the integration without recompilation of external mathematical provers (CVC4 and Z3 by default), in order to improve the automatic proof performances. This version is used industrially by Alstom, RATP and Siemens Transportation Systems.
  • the improved support for Event B language for Common Criteria certification (

The Agence Nationale de la Recherche (ANR), with the project DISCONT ANR-17-CE25-0005, contributed to the development of:

  • new verification support features (4.7)
  • Event-B manual available in the section Help/Manuals (4.7)
  • proof verification (4.6)
    • support of real numbers utilisation des nombres réels
    • addition of rules only proved by PP
  • consolidation of the proof obligations generation of the NGOP (4.6)

The changes planned for 2022 and 2023 concern:

If you require more detailed information please refer to the 4.7.1 release notes