<figure><img src="image_1.png" /></figure>

HAL
open science

# Proving B with Atelier B

Thierry Lecomte

► To cite this version:

Thierry Lecomte. Proving B with Atelier B. 2024. hal-04612165

HAL Id: hal-04612165

https://hal.science/hal-04612165

Preprint submitted on 17 Jun 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Proving B with Atelier B

Thierry Lecomte

CLEARSY, Aix en Provence, France,
thierry.lecomte@clearsy.com

**Abstract.** The article focuses on the continuous improvement of Atelier B's automatic proof capabilities since its industrialisation in the 90s. The evolution of Atelier B addressed challenges in proof obligations generation and optimisation, adapting to new languages like Event-B and incorporating newer formats for easier analysis and third-party prover connections. Significant developments include enhancing the proof system to handle complex proof obligations efficiently and integrating external provers for improved proof capabilities. The article also showcases B's industrial applications in critical sectors, emphasising the method's importance in safety-critical software development and the ongoing efforts to facilitate proof activities and integrate AI for better proof automation.

**Keywords:** Formal proof, Safety critical, B

## 1 Dedication

The author collaborated with Jim Woodcock over several research projects, together with Peter Larsen. FmeRail was an opportunity to meet for the first time and "battle" over railway case studies that showcased our favourite formal methods, in London for the announcement of the Paris Meteor automatic metro<fnref n="1" /> secured with B, in Toulouse for the successful FM'99 conference, for the development of cyber-physical systems with the INTO-CPS project, in Shonan for the green tea ceremony, rosé wine tasting in the port of Cassis. Many fond memories, um amor compartilhado pelo Brasil, thank you for taking this formal journey together.

## 2 Introduction

Mathematical proof is at the heart of the B method. It's both a strength, because software is better validated than with tests, and a weakness, because it's an activity that requires special skills, more rarely available among a company's workforce. Since Atelier B was industrialised in the 90s, it has undergone continuous improvement, with a focus on its automatic proof capabilities. As the mathematical proof of B models is specific, the improvements made have themselves been specific. This article presents the salient aspects of this work, carried

<footnote n="1">¹ inaugurated in December 1998</footnote>
# Proving B with Atelier B

Thierry Lecomte

CLEARSY, Aix en Provence, France,
thierry.lecomte@clearsy.com

**Abstract.** The article focuses on the continuous improvement of Atelier B's automatic proof capabilities since its industrialisation in the 90s. The evolution of Atelier B addressed challenges in proof obligations generation and optimisation, adapting to new languages like Event-B and incorporating newer formats for easier analysis and third-party prover connections. Significant developments include enhancing the proof system to handle complex proof obligations efficiently and integrating external provers for improved proof capabilities. The article also showcases B's industrial applications in critical sectors, emphasising the method's importance in safety-critical software development and the ongoing efforts to facilitate proof activities and integrate AI for better proof automation.

**Keywords:** Formal proof, Safety critical, B

## 1 Dedication

The author collaborated with Jim Woodcock over several research projects, together with Peter Larsen. FmeRail was an opportunity to meet for the first time and "battle" over railway case studies that showcased our favourite formal methods, in London for the announcement of the Paris Meteor automatic metro <fnref n="1" /> secured with B, in Toulouse for the successful FM'99 conference, for the development of cyber-physical systems with the INTO-CPS project, in Shonan for the green tea ceremony, rosé wine tasting in the port of Cassis. Many fond memories, um amor compartilhado pelo Brasil, thank you for taking this formal journey together.

## 2 Introduction

Mathematical proof is at the heart of the B method. It's both a strength, because software is better validated than with tests, and a weakness, because it's an activity that requires special skills, more rarely available among a company's workforce. Since Atelier B was industrialised in the 90s, it has undergone continuous improvement, with a focus on its automatic proof capabilities. As the mathematical proof of B models is specific, the improvements made have themselves been specific. This article presents the salient aspects of this work, carried

<footnote n="1">¹ inaugurated in December 1998</footnote>
out in an industrial context. It does not present any scientific studies with other
provers or similar tools, as the technical and scientific choices were strongly con-
strained from the beginning. The remainder of this paper is organised as follows.
Section 2 briefly introduces the B method. Section 3 presents the characteris-
tics and constraints associated to the B proof obligations. Section 4 describes
the proof system, its architecture and its requirements. The rationale of using
B for industrial applications is presented in section 5. Section 6 describes the
adaptation of the proof system over almost 3 decades, before concluding.

3 Introduction to the B Method

B[1] is a method for specifying, designing, and coding software systems. It covers central aspects of the software life cycle (Fig. 1): the writing of the technical specification, the design by successive refinement steps and model decomposition (layered architecture), and the source code generation.

<figure><img src="image_1.png" /><figcaption>Fig. 1: A typical B development cycle, from requirements to code.</figcaption></figure>

B is also a modelling language that is used for both specification, refinement (Fig. 2), and implementation (Fig. 3). It relies on substitution calculus, first order logic and set theory. All modelling activities are covered by mathematical proof that finally ensures that the software system is correct.

B is structured with modules and refinements. A module is used to break
down a large software into smaller parts. A module has a specification (called a
machine) where both a static and a dynamic description of the requirements are
formalised. It defines a mathematical model of the subsystem concerned:

- an abstract description of its state space and possible initial states,

- an abstract description of operations to query or modify the state.

This model establishes the external interface for that module: every implemen-
tation will conform to this specification. Conformance is assured by proof dur-
ing the formal development process. A module specification is refined. It is re-
expressed with more information: adding some requirements, refining abstract
notions with more concrete notions, getting to implementable code level. Data
out in an industrial context. It does not present any scientific studies with other
provers or similar tools, as the technical and scientific choices were strongly con-
strained from the beginning. The remainder of this paper is organised as follows.
Section 2 briefly introduces the B method. Section 3 presents the characteris-
tics and constraints associated to the B proof obligations. Section 4 describes
the proof system, its architecture and its requirements. The rationale of using
B for industrial applications is presented in section 5. Section 6 describes the
adaptation of the proof system over almost 3 decades, before concluding.

3 Introduction to the B Method

B[1] is a method for specifying, designing, and coding software systems. It covers central aspects of the software life cycle (Fig. 1): the writing of the technical specification, the design by successive refinement steps and model decomposition (layered architecture), and the source code generation.

<figure><img src="image_3.png" /><figcaption>Fig. 1: A typical B development cycle, from requirements to code.</figcaption></figure>

B is also a modelling language that is used for both specification, refinement (Fig. 2), and implementation (Fig. 3). It relies on substitution calculus, first order logic and set theory. All modelling activities are covered by mathematical proof that finally ensures that the software system is correct.

B is structured with modules and refinements. A module is used to break
down a large software into smaller parts. A module has a specification (called a
machine) where both a static and a dynamic description of the requirements are
formalised. It defines a mathematical model of the subsystem concerned:

- an abstract description of its state space and possible initial states,

- an abstract description of operations to query or modify the state.

This model establishes the external interface for that module: every implemen-
tation will conform to this specification. Conformance is assured by proof dur-
ing the formal development process. A module specification is refined. It is re-
expressed with more information: adding some requirements, refining abstract
notions with more concrete notions, getting to implementable code level. Data
refinement consists in introducing new variables to represent the state variables for the refined component, with their gluing invariant<fnref n="2" />. Algorithmic refinement consists in transforming the operations for the refined component. A refinement

<figure><img src="image_2.png" /><figcaption>Fig. 2: Structure of MACHINE and REFINEMENT components.</figcaption></figure>

may also be refined. The final refinement of a refinement column is called the implementation, it contains only B0-compliant models<fnref n="3" />. In a component (machine,

<figure><img src="image_3.png" /><figcaption>Fig. 3: Structure of IMPLEMENTATION component.</figcaption></figure>

refinement, or implementation), sets, constants, and variables define the state

<footnote n="2">² A B refinement is composed of an abstract and a concrete labeled transition system (LTS) related by a gluing invariant. The gluing invariant is a binary predicate over the states of the abstract LTS and the states of the concrete one.</footnote>

<footnote n="3">³ B0 is a subset of the B language, where OPERATIONS are deterministic and data types are restricted. Its syntax is close to any structured language.</footnote>
refinement consists in introducing new variables to represent the state variables for the refined component, with their gluing invariant<fnref n="2" />. Algorithmic refinement consists in transforming the operations for the refined component. A refinement

<figure><img src="image_4.png" /><figcaption>Fig. 2: Structure of MACHINE and REFINEMENT components.</figcaption></figure>

may also be refined. The final refinement of a refinement column is called the implementation, it contains only B0-compliant models<fnref n="3" />. In a component (machine,

<figure><img src="image_5.png" /><figcaption>Fig. 3: Structure of IMPLEMENTATION component.</figcaption></figure>

refinement, or implementation), sets, constants, and variables define the state

<footnote n="2">² A B refinement is composed of an abstract and a concrete labeled transition system (LTS) related by a gluing invariant. The gluing invariant is a binary predicate over the states of the abstract LTS and the states of the concrete one.</footnote>

<footnote n="3">³ B0 is a subset of the B language, where OPERATIONS are deterministic and data types are restricted. Its syntax is close to any structured language.</footnote>
space while the invariants define the static properties for its state variables. The initialisation phase (for the state variables) and the operations (for querying or modifying the state) define the way variables are modified. From these, proof obligations are computed such as: the static properties are consistent, they are established by the initialisation, and they are preserved by all the operations.

Finally a B project is a set of linked B modules. Each module is formed of components: an abstract machine (its specification), possibly some refinements and an implementation<fnref n="4" />. The principal dependencies links between modules are IMPORTS links (forming a modular decomposition tree<fnref n="5" />) and SEES links (read only transversal visibility<fnref n="6" />). Sub-projects may be grouped into libraries. A software developed in B may integrate or may be integrated with traditionally developed code.

# 4 Atelier B Proof Obligations

## 4.1 Characteristics and Constraints

Proof obligations (PO) are central to the B verification schema[8]. They are computed from B models (see Fig. 4) to cover several aspects: correctness, overflow, and well-definedness.

<figure><img src="image_4.png" /><figcaption>Fig. 4: Proof obligations are linked with model clauses.</figcaption></figure>

<footnote n="4">⁴ Most components are made of one machine and one implementation. In some cases where the proof is too difficult to handle (the proof obligations are too complex), intermediate refinements (algorithm or data) are introduced to reduce this complexity. Four intermediate refinements may be considered as a maximum.</footnote>

<footnote n="5">⁵ B is a top-down approach. Models are decomposed into smaller ones.</footnote>

<footnote n="6">⁶ Read-only components can be seen by components which are not on the same branch of the decomposition tree.</footnote>
space while the invariants define the static properties for its state variables. The initialisation phase (for the state variables) and the operations (for querying or modifying the state) define the way variables are modified. From these, proof obligations are computed such as: the static properties are consistent, they are established by the initialisation, and they are preserved by all the operations.

Finally a B project is a set of linked B modules. Each module is formed of components: an abstract machine (its specification), possibly some refinements and an implementation<fnref n="4" />. The principal dependencies links between modules are IMPORTS links (forming a modular decomposition tree<fnref n="5" />) and SEES links (read only transversal visibility<fnref n="6" />). Sub-projects may be grouped into libraries. A software developed in B may integrate or may be integrated with traditionally developed code.

# 4 Atelier B Proof Obligations

## 4.1 Characteristics and Constraints

Proof obligations (PO) are central to the B verification schema[8]. They are computed from B models (see Fig. 4) to cover several aspects: correctness, overflow, and well-definedness.

<figure><img src="image_6.png" /><figcaption>Fig. 4: Proof obligations are linked with model clauses.</figcaption></figure>

<footnote n="4">⁴ Most components are made of one machine and one implementation. In some cases where the proof is too difficult to handle (the proof obligations are too complex), intermediate refinements (algorithm or data) are introduced to reduce this complexity. Four intermediate refinements may be considered as a maximum.</footnote>

<footnote n="5">⁵ B is a top-down approach. Models are decomposed into smaller ones.</footnote>

<footnote n="6">⁶ Read-only components can be seen by components which are not on the same branch of the decomposition tree.</footnote>
The first proof obligation generator developed in the 90s contained many
hard-coded optimisations, which made it difficult to understand how it worked,
to optimize the generator, and to modify the B language. Atelier B historically
also used custom data formats and specific programming languages. These for-
mats have lasted for several decades because redesigning the formats and the
programs would have been too costly. Specific programming languages (like a
in-house Prolog-like language) have made it more difficult to convince engineers
to work on this software.

In any case, once the first industrial project has been completed, Atelier B
was obliged to keep the proof obligation process constant to avoid any proof
regression. Any modification in the proof obligations shape, naming, or order
would have had a dramatic impact on the effort (i.e. cost) required to maintain
B projects proved over the years. The proof obligations are named after the B
clauses to which they apply. Mathematical demonstrations are associated with
the proof obligations of a clause. Heuristics allow us to continue to associate
these demonstrations correctly with the proof obligations, when refactoring the
B model for which we do not want to lose the interactive proof work already
carried out.

## 4.2 Evolution

The invention of Event-B in the 2000s required to develop a new proof obligation
generator, supporting both B and Event-B languages. The PO file format was left
unchanged, but the core of the generator was split into 2 parts: the generation
engine itself developed in C++ and the theoretical proof obligations expressed
in XSLT[14] that could be modified on the fly without requiring to recompile
the engine. Adding Event-B support as well as REAL and FLOAT numbers [5]
to Atelier B was greatly eased by this decomposition.

More recent developments provide alternative tools using XML based formats
to facilitate the study of B proof obligations and the connection to third party
provers. In particular, the proof obligation format pog is a XML-based format for
proof obligations. Its definition is provided as an XML Schema Definition. This
definition is documented through annotations directly available in the source
file. Xsltproc then generates an HTML version of the documentation.

Finally, this new design has made it possible to add a traceability mechanism
that enables proof obligations to be associated with models in an immediate
and precise manner. This has made it possible to add to the integrated B model
editor a colouring of the text indicating its automatic rate of proof as well as
the remainder to be proven.

# 5 Atelier B Proof System

When Atelier B was built, there was no prover capable of handling proof obli-
gations that mixed set theory and arithmetic, and that could contain thousands
or even tens of thousands of hypotheses. In addition, the processing time had to
The first proof obligation generator developed in the 90s contained many
hard-coded optimisations, which made it difficult to understand how it worked,
to optimize the generator, and to modify the B language. Atelier B historically
also used custom data formats and specific programming languages. These for-
mats have lasted for several decades because redesigning the formats and the
programs would have been too costly. Specific programming languages (like a
in-house Prolog-like language) have made it more difficult to convince engineers
to work on this software.

In any case, once the first industrial project has been completed, Atelier B
was obliged to keep the proof obligation process constant to avoid any proof
regression. Any modification in the proof obligations shape, naming, or order
would have had a dramatic impact on the effort (i.e. cost) required to maintain
B projects proved over the years. The proof obligations are named after the B
clauses to which they apply. Mathematical demonstrations are associated with
the proof obligations of a clause. Heuristics allow us to continue to associate
these demonstrations correctly with the proof obligations, when refactoring the
B model for which we do not want to lose the interactive proof work already
carried out.

## 4.2 Evolution

The invention of Event-B in the 2000s required to develop a new proof obligation
generator, supporting both B and Event-B languages. The PO file format was left
unchanged, but the core of the generator was split into 2 parts: the generation
engine itself developed in C++ and the theoretical proof obligations expressed
in XSLT[14] that could be modified on the fly without requiring to recompile
the engine. Adding Event-B support as well as REAL and FLOAT numbers [5]
to Atelier B was greatly eased by this decomposition.

More recent developments provide alternative tools using XML based formats
to facilitate the study of B proof obligations and the connection to third party
provers. In particular, the proof obligation format pog is a XML-based format for
proof obligations. Its definition is provided as an XML Schema Definition. This
definition is documented through annotations directly available in the source
file. Xsltproc then generates an HTML version of the documentation.

Finally, this new design has made it possible to add a traceability mechanism
that enables proof obligations to be associated with models in an immediate
and precise manner. This has made it possible to add to the integrated B model
editor a colouring of the text indicating its automatic rate of proof as well as
the remainder to be proven.

# 5 Atelier B Proof System

When Atelier B was built, there was no prover capable of handling proof obli-
gations that mixed set theory and arithmetic, and that could contain thousands
or even tens of thousands of hypotheses. In addition, the processing time had to
be a maximum of ten seconds on average for each proof obligation. This section presents the proof system that was developed for this purpose.

## 5.1 Automatic Proof

The Automatic Prover PR was developed from scratch. It is made of two distinct parts: a loader and a solver.

Loader It is designed to minimise PO loading/unloading in memory: PO could have many hypotheses, so unloading all hypotheses from memory when moving to the next PO is not optimal. The hypotheses are grouped into packets, corresponding to the different clauses of a B model. PR unloads from computer memory only those hypotheses that are no longer used and keeps the others. PO file format was structured accordingly.

<figure><img src="image_5.png" /><figcaption>Fig. 5: Structure of PR.</figcaption></figure>

Solver It generates new hypotheses and transforms the goal in order to obtain $\top$ (represented with the predefined symbol *btrue*). If the solver is successful, the proof obligation is considered proved. If not, the proof obligation remains unproved. A B project is valid only when 100% PO are proved. The solver (Fig. 5) is itself composed of:

- an hypothesis processor, generating new hypotheses but not modifying (re- placing) existing ones. Heuristics are applied to either combine or instantiate existing hypotheses, usually in relation with the goal to prove.

- a goal processor, simplifying the current goal by adding local hypotheses derived from existing ones, or by replacing the current goal by one or sev- eral sub-goals. Simplification and addition of hypotheses are performed by
be a maximum of ten seconds on average for each proof obligation. This section presents the proof system that was developed for this purpose.

## 5.1 Automatic Proof

The Automatic Prover PR was developed from scratch. It is made of two distinct parts: a loader and a solver.

Loader It is designed to minimise PO loading/unloading in memory: PO could have many hypotheses, so unloading all hypotheses from memory when moving to the next PO is not optimal. The hypotheses are grouped into packets, corresponding to the different clauses of a B model. PR unloads from computer memory only those hypotheses that are no longer used and keeps the others. PO file format was structured accordingly.

<figure><img src="image_7.png" /><figcaption>Fig. 5: Structure of PR.</figcaption></figure>

Solver It generates new hypotheses and transforms the goal in order to obtain $\top$ (represented with the predefined symbol *btrue*). If the solver is successful, the proof obligation is considered proved. If not, the proof obligation remains unproved. A B project is valid only when 100% PO are proved. The solver (Fig. 5) is itself composed of:

- an hypothesis processor, generating new hypotheses but not modifying (re- placing) existing ones. Heuristics are applied to either combine or instantiate existing hypotheses, usually in relation with the goal to prove.

- a goal processor, simplifying the current goal by adding local hypotheses derived from existing ones, or by replacing the current goal by one or several sub-goals. Simplification and addition of hypotheses are performed by
proof mechanisms. Goal transformation (simplification, decomposition) results from the application of mathematical proof rules. These rules are either part of the prover rules database or are developed by users and specific to each project.

The two processors are executed in sequence: the goal is simplified while new hypotheses are generated. We then hope that the hypotheses generated will trigger rules that will ultimately demonstrate the goal.

*Proof mechanisms* The solver, actionable through the parameter *force*, ranging from 0 to 3, contains 35 mechanisms$^{7}$. They were designed, improved then selected by engineers from different companies, based on experiments on several B projects representing a total of 3000 POs. The selection was made based on both the automatic proof percentage and the complexity / difficulty to prove remaining POs. These mechanisms are assembled in two configurations to form respectively:

- The bounded prover, corresponding to the force 0, comes with limited complexity mechanisms. It is the most efficient prover configuration, used first during automatic proof, usually able to demonstrate 70% of the proof obligations, with a mean execution time of 10 seconds.

- The unbounded prover includes heuristics that could generate infinite execution. Force 1 is an extension of force 0 prover where new hypotheses are more simplified by applying a stronger normalisation. Force 2 extends force 1 by generating more derived hypotheses. Force 3 extends force 2 by attempting proof by cases. These 3 forces usually increase automatic proof performance by 1 or 2 % each.

The hypothesis processor is identical for both bounded and unbounded provers. There is another version of the Automatic Prover called MonoLemma ML. It comes without the optimised loader, to demonstrate a single proof obligation. ML is used to power the Rodin platform as "Atelier B provers" plug-in$^{8}$.

## 5.2 Extending the Prover

The automatic prover builds a proof tree. Its root is the initial goal to be proved. The descendants correspond to the result of simplifications made to the goal by applying the rule base. The leaves correspond to existing hypotheses or axioms (trivially verifiable predicates such as $0 \le 1$ or TRUE: BOOL). When one of the

<footnote>$^{7}$ The structure of the prover, the mathematical rules database, the mechanisms constituting both bounded and unbounded provers, and their parameters were designed, defined, and optimised based on the B models developed by the company Matra from 1993 until 1998. Hence the proof performances were not guaranteed when symbols and predicates used are quite different from those in Meteor models. To improve automatic proof percentage, complementary mathematical rule databases need to be designed to address specific symbols or patterns.</footnote>

<footnote>$^{8}$ https://wiki.event-b.org/index.php/Rodin_Platform_Releases</footnote>
proof mechanisms. Goal transformation (simplification, decomposition) results from the application of mathematical proof rules. These rules are either part of the prover rules database or are developed by users and specific to each project.

The two processors are executed in sequence: the goal is simplified while new hypotheses are generated. We then hope that the hypotheses generated will trigger rules that will ultimately demonstrate the goal.

*Proof mechanisms* The solver, actionable through the parameter *force*, ranging from 0 to 3, contains 35 mechanisms$^{7}$. They were designed, improved then selected by engineers from different companies, based on experiments on several B projects representing a total of 3000 POs. The selection was made based on both the automatic proof percentage and the complexity / difficulty to prove remaining POs. These mechanisms are assembled in two configurations to form respectively:

- The bounded prover, corresponding to the force 0, comes with limited complexity mechanisms. It is the most efficient prover configuration, used first during automatic proof, usually able to demonstrate 70% of the proof obligations, with a mean execution time of 10 seconds.

- The unbounded prover includes heuristics that could generate infinite execution. Force 1 is an extension of force 0 prover where new hypotheses are more simplified by applying a stronger normalisation. Force 2 extends force 1 by generating more derived hypotheses. Force 3 extends force 2 by attempting proof by cases. These 3 forces usually increase automatic proof performance by 1 or 2 % each.

The hypothesis processor is identical for both bounded and unbounded provers. There is another version of the Automatic Prover called MonoLemma ML. It comes without the optimised loader, to demonstrate a single proof obligation. ML is used to power the Rodin platform as "Atelier B provers" plug-in$^{8}$.

## 5.2 Extending the Prover

The automatic prover builds a proof tree. Its root is the initial goal to be proved. The descendants correspond to the result of simplifications made to the goal by applying the rule base. The leaves correspond to existing hypotheses or axioms (trivially verifiable predicates such as $0 \le 1$ or TRUE: BOOL). When one of the

<footnote>$^{7}$ The structure of the prover, the mathematical rules database, the mechanisms constituting both bounded and unbounded provers, and their parameters were designed, defined, and optimised based on the B models developed by the company Matra from 1993 until 1998. Hence the proof performances were not guaranteed when symbols and predicates used are quite different from those in Meteor models. To improve automatic proof percentage, complementary mathematical rule databases need to be designed to address specific symbols or patterns.</footnote>

<footnote>$^{8}$ https://wiki.event-b.org/index.php/Rodin_Platform_Releases</footnote>
leaves cannot be demonstrated because it is neither a hypothesis nor an axiom, the prover stops. Interaction with the user then begins, seeking to improve proof performance. Proof helpers available to the user are the addition of user defined rules, a proof-oriented script language, the definition of proof tactics and their selective execution, the conservation of demonstrations when the models change drastically, and graphical display of proof information elements. Interaction is not seen as a one-time action but as an investment in reducing the proof activity on the rest of the project, especially for similar proof obligations.

*Addition of user defined rules* Three kinds of rules can be added to Atelier B:

- backward rules transforming a goal into 0 or more sub-goals,

- rewriting rules working on expressions and predicates,

- forward rules generating new hypotheses, triggered when the Modus Ponens is activated.

Apart from the Atelier B rules database, user defined rules may be added at component or at project level (PatchProver). The PatchProver is central to the proof performance: it has to be set up gradually based on previous completed projects and managed with a source-code management system. It constitutes the palette that each user has to know well. The addition of user rules in proof component files is only permitted if no (combination of) rules is available in the PatchProver. All rules have to be validated before being used in a project, at least with a manual demonstration.

*Proof-oriented script language* It contains more than 30 commands allowing to modify the proof tree or to collect information about it<fnref n="9" />. These commands are able to activate the bounded and unbounded provers, the processing of hypotheses for any force. They are also able to add hypothesis, initiate a proof by cases, trigger the Modus Ponens, start the Predicate Prover or simplify a goal with the Set Solver, and execute an external prover. To avoid long waiting times, some commands are associated with deadlines - the execution of these commands will not last longer than this delay that is a parameter of the command. Similarly, for provers that work better with a limited number of proof obligations, it is possible to specify that only typing hypotheses or hypotheses having a symbol in common with the goal are selected for the proof.

*Definition of proof tactics and their selective execution* Proof-oriented commands can be saved as demonstration. These are the demonstrations that are replayed often to ensure that the project is still provable. These demonstrations are supposed to be as generic as possible, to be applied on other similar proof obligations. In the interactive prover, when at least one PO has been demonstrated, the user is asked if these demonstrations could be saved in the User Pass, a specific part of the component proof files that only contains proof tactics (generic

<footnote n="9">⁹ See https://b-method.gitbook.io/training-resources-for-atelier-b/ for more details.</footnote>
leaves cannot be demonstrated because it is neither a hypothesis nor an axiom, the prover stops. Interaction with the user then begins, seeking to improve proof performance. Proof helpers available to the user are the addition of user defined rules, a proof-oriented script language, the definition of proof tactics and their selective execution, the conservation of demonstrations when the models change drastically, and graphical display of proof information elements. Interaction is not seen as a one-time action but as an investment in reducing the proof activity on the rest of the project, especially for similar proof obligations.

*Addition of user defined rules* Three kinds of rules can be added to Atelier B:

- backward rules transforming a goal into 0 or more sub-goals,

- rewriting rules working on expressions and predicates,

- forward rules generating new hypotheses, triggered when the Modus Ponens is activated.

Apart from the Atelier B rules database, user defined rules may be added at component or at project level (PatchProver). The PatchProver is central to the proof performance: it has to be set up gradually based on previous completed projects and managed with a source-code management system. It constitutes the palette that each user has to know well. The addition of user rules in proof component files is only permitted if no (combination of) rules is available in the PatchProver. All rules have to be validated before being used in a project, at least with a manual demonstration.

*Proof-oriented script language* It contains more than 30 commands allowing to modify the proof tree or to collect information about it<fnref n="9" />. These commands are able to activate the bounded and unbounded provers, the processing of hypotheses for any force. They are also able to add hypothesis, initiate a proof by cases, trigger the Modus Ponens, start the Predicate Prover or simplify a goal with the Set Solver, and execute an external prover. To avoid long waiting times, some commands are associated with deadlines - the execution of these commands will not last longer than this delay that is a parameter of the command. Similarly, for provers that work better with a limited number of proof obligations, it is possible to specify that only typing hypotheses or hypotheses having a symbol in common with the goal are selected for the proof.

*Definition of proof tactics and their selective execution* Proof-oriented commands can be saved as demonstration. These are the demonstrations that are replayed often to ensure that the project is still provable. These demonstrations are supposed to be as generic as possible, to be applied on other similar proof obligations. In the interactive prover, when at least one PO has been demonstrated, the user is asked if these demonstrations could be saved in the User Pass, a specific part of the component proof files that only contains proof tactics (generic

<footnote n="9">⁹ See https://b-method.gitbook.io/training-resources-for-atelier-b/ for more details.</footnote>
demonstrations). These demonstrations can be tried on the remaining proof obli-
gations of the current component. These tactics are ordered: the first one is tried
on all unproved POs, the other ones on the remaining POs once the previous
tactic has been applied. Naturally the most generic, efficient tactics have to be
in the first places while the more specific and longest to execute have to posi-
tioned further down the list. In addition, it is possible to use filters to make the
selection even more precise, by specifying the name of the operation and/or the
form of the goal.

5.3 Validation

From 1993 to 1998, the Automatic Prover was reverse-engineered, documented, tested, and extended to be ready for RATP qualification. It was made available to the Community and presented at the occasion of B-User Group meetings. The mathematical rules database was published to enable academic research [3]. Proof mechanisms were validated in conformance with software development best practices: documentation peer review, source code inspection, and requirement-based test-bench. Mathematical rules database (2700+ rules) validation was decomposed in two activities: automatic proof with the Predicate Prover PP, and manual proof for the rules not proved or not handled by PP.

*Automatic proof* The Predicate Prover PP was developed specifically to auto-
mate this error-prone activity. PP [2] is based on semantic tableau proof system.
The 116 inference rules are described by conditional rewrite rules and their ap-
plication is controlled by strategies (case-split, instantiation of quantified pred-
icates, etc.). The specification of PP was made public to encourage formal re-
search [6][7]. Its specification was also peer reviewed and traceability with source
code was established. Its validation consisted in developing an automaton able
to replay the demonstration <sup>10</sup> to obtain a contradiction. Then PP has been in-
cluded into a professional tool including checkers and translator, to specifically
support industrial projects. PP is efficient when the number of hypotheses is
low, which is the case for mathematical rule validation. The use of PP for proof
of OP requires hypothesis filtering to maintain its proof performance.

*Manual proof* The mathematical rules that are not handled or proved by PP had to be verified manually. A form had to be filled with the source code of the rule, its manual translation into mathematical predicate, the verification of its correct typing and the absence of name collision between identifiers and quantified variables. Then a mathematical demonstration with no imposed format had to be provided. Each form was reviewed by a panel of about ten people from five different companies. The remarks made had to be taken into account by the author of the form and then the rule had to be reviewed again, as long as remarks remained. Finally a third party company was in charge on reviewing

<footnote n="10">¹⁰ A sequence of inference rules, with the instantiation value of related quantified vari-
ables if any.</footnote>
demonstrations). These demonstrations can be tried on the remaining proof obli-
gations of the current component. These tactics are ordered: the first one is tried
on all unproved POs, the other ones on the remaining POs once the previous
tactic has been applied. Naturally the most generic, efficient tactics have to be
in the first places while the more specific and longest to execute have to posi-
tioned further down the list. In addition, it is possible to use filters to make the
selection even more precise, by specifying the name of the operation and/or the
form of the goal.

5.3 Validation

From 1993 to 1998, the Automatic Prover was reverse-engineered, documented, tested, and extended to be ready for RATP qualification. It was made available to the Community and presented at the occasion of B-User Group meetings. The mathematical rules database was published to enable academic research [3]. Proof mechanisms were validated in conformance with software development best practices: documentation peer review, source code inspection, and requirement-based test-bench. Mathematical rules database (2700+ rules) validation was decomposed in two activities: automatic proof with the Predicate Prover PP, and manual proof for the rules not proved or not handled by PP.

*Automatic proof* The Predicate Prover PP was developed specifically to auto-
mate this error-prone activity. PP [2] is based on semantic tableau proof system.
The 116 inference rules are described by conditional rewrite rules and their ap-
plication is controlled by strategies (case-split, instantiation of quantified pred-
icates, etc.). The specification of PP was made public to encourage formal re-
search [6][7]. Its specification was also peer reviewed and traceability with source
code was established. Its validation consisted in developing an automaton able
to replay the demonstration <sup>10</sup> to obtain a contradiction. Then PP has been in-
cluded into a professional tool including checkers and translator, to specifically
support industrial projects. PP is efficient when the number of hypotheses is
low, which is the case for mathematical rule validation. The use of PP for proof
of OP requires hypothesis filtering to maintain its proof performance.

*Manual proof* The mathematical rules that are not handled or proved by PP had to be verified manually. A form had to be filled with the source code of the rule, its manual translation into mathematical predicate, the verification of its correct typing and the absence of name collision between identifiers and quantified variables. Then a mathematical demonstration with no imposed format had to be provided. Each form was reviewed by a panel of about ten people from five different companies. The remarks made had to be taken into account by the author of the form and then the rule had to be reviewed again, as long as remarks remained. Finally a third party company was in charge on reviewing

<footnote n="10"><sup>10</sup> A sequence of inference rules, with the instantiation value of related quantified vari-
ables if any.</footnote>
all forms and to evaluate if the demonstrations were convincing. The validation
was completed when all manual demonstrations were deemed to be convincing.
The forms and the evaluation report were added to the validation file.

The validation of the rules was a long process, which lasted much longer than
the five years of Atelier B Meteor’s development. Some errors were detected after
1998. Where possible, the rule was corrected and industry users were invited to
re-prove their projects. Most of the time, the rules were "almost correct". Often a
restriction on the application domain was missing. It was also detected that some
rules were duplicated: as the validation of rules is unitary, this fact remained
undetected for some time. Circumventing the problem required to replace the
duplicated rule by a non-applicable rule <fnref n="11" />.

During the development of PP, a first attempt to verify the rules database occurred in 1995. The tool handled 1535 rules, the other rules were not processed because of functional limitations (sequences not supported, several guards not yet translated). 59 were detected false, 55 were corrected and verified by PP successfully, 4 were removed because they were wrong (or too specific). A dedicated proof tool with GUI was designed and integrated to Atelier B to provide a systematic verification framework. Finally a few tens of rules have been corrected since 1998. Their detection is often due to incorrect models proved successfully. Backward analysis allows to locate the origin of the error, if it is a rule. If the cause is a faulty mechanism, then the analysis is our responsibility, as the code of the mechanisms is not accessible through the tool, unlike the mathematical rules.

6 B Industrial Applications

B's preferred field of application remains the railway sector, which strongly rec-
ommends (standard EN50128) the use of formal methods for the software devel-
opment of SIL3 or SIL4 critical functions. B is used for safety-related automatic
signalling systems for automatic metros. If the figures provided by Alstom and
Siemens are aggregated, B would be used for around 30% of CBTC-type<fnref n="12" /> au-
tomatic metros.

For the first application on line 14 of the Paris metro, the ATP (Automatic
Train Protection) function represented 86 kloc of B models, representing 110 kloc
of Ada code. This function triggers emergency braking when a danger is detected,
in conjunction with speed supervision. This software is typical of the applications
that can be developed with B: it is a cyclical, non-parallelised application that
acquires inputs, performs calculations and sets outputs. Its main property is
that it stops the train if the conditions for train movement are no longer met.
Contrary to what one might think, this property is not the absence of collision,
as rail transport safety is distributed across several systems on board the train
and on the tracks. The train knows the topology of the track on which it is

<footnote n="11">¹¹ It was not possible to delete it as it would have modified the order (the name) of the rules, that can be called by their index during interactive proof.</footnote>

<footnote n="12">¹² Radio-based train control.</footnote>
all forms and to evaluate if the demonstrations were convincing. The validation
was completed when all manual demonstrations were deemed to be convincing.
The forms and the evaluation report were added to the validation file.

The validation of the rules was a long process, which lasted much longer than
the five years of Atelier B Meteor’s development. Some errors were detected after
1998. Where possible, the rule was corrected and industry users were invited to
re-prove their projects. Most of the time, the rules were "almost correct". Often a
restriction on the application domain was missing. It was also detected that some
rules were duplicated: as the validation of rules is unitary, this fact remained
undetected for some time. Circumventing the problem required to replace the
duplicated rule by a non-applicable rule <fnref n="11" />.

During the development of PP, a first attempt to verify the rules database occurred in 1995. The tool handled 1535 rules, the other rules were not processed because of functional limitations (sequences not supported, several guards not yet translated). 59 were detected false, 55 were corrected and verified by PP successfully, 4 were removed because they were wrong (or too specific). A dedicated proof tool with GUI was designed and integrated to Atelier B to provide a systematic verification framework. Finally a few tens of rules have been corrected since 1998. Their detection is often due to incorrect models proved successfully. Backward analysis allows to locate the origin of the error, if it is a rule. If the cause is a faulty mechanism, then the analysis is our responsibility, as the code of the mechanisms is not accessible through the tool, unlike the mathematical rules.

6 B Industrial Applications

B's preferred field of application remains the railway sector, which strongly rec-
ommends (standard EN50128) the use of formal methods for the software devel-
opment of SIL3 or SIL4 critical functions. B is used for safety-related automatic
signalling systems for automatic metros. If the figures provided by Alstom and
Siemens are aggregated, B would be used for around 30% of CBTC-type<fnref n="12" /> au-
tomatic metros.

For the first application on line 14 of the Paris metro, the ATP (Automatic
Train Protection) function represented 86 kloc of B models, representing 110 kloc
of Ada code. This function triggers emergency braking when a danger is detected,
in conjunction with speed supervision. This software is typical of the applications
that can be developed with B: it is a cyclical, non-parallelised application that
acquires inputs, performs calculations and sets outputs. Its main property is
that it stops the train if the conditions for train movement are no longer met.
Contrary to what one might think, this property is not the absence of collision,
as rail transport safety is distributed across several systems on board the train
and on the tracks. The train knows the topology of the track on which it is

<footnote n="11">¹¹ It was not possible to delete it as it would have modified the order (the name) of the rules, that can be called by their index during interactive proof.</footnote>

<footnote n="12">¹² Radio-based train control.</footnote>
travelling (rails, signals, points, speed limits). Its position is estimated using beacons, odometer and GNSS signals. To determine the train's ability to keep moving forward, we use graph traversal algorithms (to find out where the train is), numerical calculations using integers to calculate kinetic energy, and Boolean equations to determine the triggering of the emergency braking. SIL3 and SIL4 applications require special hardware architectures, in particular the need to duplicate calculations and process the result by vote to ensure the good health of the execution machine. A difference in behavior then implies a switch to fallback mode and immediate shutdown of the train. In the same way, software functions must be diversified to avoid the same design error being executed at the same time on 2 ECUs without being detected. As a general rule, based on the same software specification, 2 versions of the same software are developed by two independent teams using different technologies, to avoid common modes. The probability of the 2 software versions producing the same safety-related misbehaviour at the same time is therefore negligible<fnref n="13" />.

With Atelier B, only one model needs to be developed. Then two code gen-
erators, developed once and for all by two independent teams with different
technologies or principles, produce the two required instances of the software.
This approach enables us to achieve very significant savings with a single soft-
ware development, with B. In addition, at the time of certification, since unit
and integration tests are replaced by exhaustive mathematical proof, there is no
problem justifying software testing.

For the Paris metro, lines 1, 4, 13, and 14 currently have critical functions de-
veloped with B. With the Olympic Games and the Grand Paris Express project,
lines 15, 16, 17 and 18 will also have such functions by 2030. Other applications
linked to the SIL4 CLEARSY Safety Platform use B and Atelier B to develop
critical SIL3 and SIL4 certified functions, for metro landing door control, locali-
sation and communication. Last but not least, experiments are currently taking
place outside the rail sector for autonomous mobility applications on land and
at sea, within different regulatory frameworks. The results of these experiments
may well lead to changes in industrial practices and associated standards.

7 Adaptation Over Years

To enable greater deployment of B and Atelier B, it is necessary to facilitate
the proof activity by maximising the automatic proof rate. To ensure improved
proof performance and thus lower development costs, extending interactive proof
commands and adding rules packages have reduced scope because the limitations
of the proof kernel PR remain. So improvements were sought through features
implemented externally, i.e. coupling with third-party provers and using AI for
easing interactive proof. Below are listed the main contributions to the proof
kernel.

<footnote n="13">¹³ Systematic failures during design and random failures during execution are handled with this diversity and redundancy.</footnote>
travelling (rails, signals, points, speed limits). Its position is estimated using beacons, odometer and GNSS signals. To determine the train's ability to keep moving forward, we use graph traversal algorithms (to find out where the train is), numerical calculations using integers to calculate kinetic energy, and Boolean equations to determine the triggering of the emergency braking. SIL3 and SIL4 applications require special hardware architectures, in particular the need to duplicate calculations and process the result by vote to ensure the good health of the execution machine. A difference in behavior then implies a switch to fallback mode and immediate shutdown of the train. In the same way, software functions must be diversified to avoid the same design error being executed at the same time on 2 ECUs without being detected. As a general rule, based on the same software specification, 2 versions of the same software are developed by two independent teams using different technologies, to avoid common modes. The probability of the 2 software versions producing the same safety-related misbehaviour at the same time is therefore negligible<fnref n="13" />.

With Atelier B, only one model needs to be developed. Then two code generators, developed once and for all by two independent teams with different technologies or principles, produce the two required instances of the software. This approach enables us to achieve very significant savings with a single software development, with B. In addition, at the time of certification, since unit and integration tests are replaced by exhaustive mathematical proof, there is no problem justifying software testing.

For the Paris metro, lines 1, 4, 13, and 14 currently have critical functions developed with B. With the Olympic Games and the Grand Paris Express project, lines 15, 16, 17 and 18 will also have such functions by 2030. Other applications linked to the SIL4 CLEARSY Safety Platform use B and Atelier B to develop critical SIL3 and SIL4 certified functions, for metro landing door control, localisation and communication. Last but not least, experiments are currently taking place outside the rail sector for autonomous mobility applications on land and at sea, within different regulatory frameworks. The results of these experiments may well lead to changes in industrial practices and associated standards.

# 7 Adaptation Over Years

To enable greater deployment of B and Atelier B, it is necessary to facilitate the proof activity by maximising the automatic proof rate. To ensure improved proof performance and thus lower development costs, extending interactive proof commands and adding rules packages have reduced scope because the limitations of the proof kernel PR remain. So improvements were sought through features implemented externally, i.e. coupling with third-party provers and using AI for easing interactive proof. Below are listed the main contributions to the proof kernel.

<footnote n="13">¹³ Systematic failures during design and random failures during execution are handled with this diversity and redundancy.</footnote>
ProB In the early 2000’s, formal data validation started to become more wide-
spread in the railways [10]. In particular, the ProB model-checker was first
demonstrated during the EU project DEPLOY [13]. After some optimisations,
ProB was able to fully handle large size metro data and validation rules, re-
sulting in the generation of one B machine per validation rule and instantiated
with the data related to this rule. To date, the biggest B machine generated for
data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3,
ProB was added as an interactive command [12]. Its behaviour is similar to the
predicate prover: it does not modify the goal, only trying to demonstrate it. It
comes with a time limit (maximum duration) and the possibility to reduce the
number of hypotheses by selecting those having one symbol in common with the
goal. PRoB allows better handling of arithmetic goals and case-based proofs on
reduced domains.

Zenon, iProver, and Alt-Ergo BWare [9] (2012-2016) was an industrial research project aimed at providing a mechanised framework to support the automated verification of proof obligations. The adopted methodology consists in building a generic verification platform relying on different automated theorem provers, such as first order provers and SMT solvers. This generic platform is built upon the Why3 platform for deductive program verification. The considered first order provers are Zenon and iProver Modulo, while we opted for the Alt-Ergo SMT solver. In this framework, B proof obligations are translated by a specific tool into Why3 files, which are compatible with a Why3 encoding of the B set theory. From these files, Why3 can produce (by means of appropriate drivers) the proof obligations for the automated theorem provers, using the TPTP format for Zenon and iProver Modulo, and a native format for Alt-Ergo. This translation together with the encoding of the B set theory aims to generate valid statements that are appropriate for the automated theorem provers, i.e. whose proofs can be found by these provers. Finally, once proofs have been found by these tools, some of these provers can generate proof objects to be verified by proof checkers. This is the case of Zenon, which can produce proof objects for Coq and Dedukti, and iProver Modulo, which can also produce proof objects for Dedukti. An initial bench of 13,000 proof obligations, issued from several industrial projects, was constituted to evaluate the BWare platform. Atelier B PR prover was able to demonstrate 85% of them, Alt-Ergo 58%, iProver Modulo 19 %, and Zenon less than 1%. As can be observed, the first order provers encounter difficulties, which can be explained by the fact that these provers do not know the B set theory. At the end of the project, Alt-Ergo was able to demonstrate 98% of the PO, Zenon 95%, and iProver 28%. We also completed the set of provers: CVC4 was able to demonstrate 94% of the PO, Z3 84%, Vampire 78%, and E 61%. It appears that the project and the supply of POs has improved the performance of some provers. In the case of Alt-Ergo, the remaining POs are existential and require human intelligence to prove.

Alt-Ergo LCHIP [11] (2016-2020) was an industrial project aimed at develop-
ing a safety computer programmed with B and with enhanced proof capabili-
ProB In the early 2000’s, formal data validation started to become more wide-
spread in the railways [10]. In particular, the ProB model-checker was first
demonstrated during the EU project DEPLOY [13]. After some optimisations,
ProB was able to fully handle large size metro data and validation rules, re-
sulting in the generation of one B machine per validation rule and instantiated
with the data related to this rule. To date, the biggest B machine generated for
data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3,
ProB was added as an interactive command [12]. Its behaviour is similar to the
predicate prover: it does not modify the goal, only trying to demonstrate it. It
comes with a time limit (maximum duration) and the possibility to reduce the
number of hypotheses by selecting those having one symbol in common with the
goal. PRoB allows better handling of arithmetic goals and case-based proofs on
reduced domains.

Zenon, iProver, and Alt-Ergo BWare [9] (2012-2016) was an industrial research project aimed at providing a mechanised framework to support the automated verification of proof obligations. The adopted methodology consists in building a generic verification platform relying on different automated theorem provers, such as first order provers and SMT solvers. This generic platform is built upon the Why3 platform for deductive program verification. The considered first order provers are Zenon and iProver Modulo, while we opted for the Alt-Ergo SMT solver. In this framework, B proof obligations are translated by a specific tool into Why3 files, which are compatible with a Why3 encoding of the B set theory. From these files, Why3 can produce (by means of appropriate drivers) the proof obligations for the automated theorem provers, using the TPTP format for Zenon and iProver Modulo, and a native format for Alt-Ergo. This translation together with the encoding of the B set theory aims to generate valid statements that are appropriate for the automated theorem provers, i.e. whose proofs can be found by these provers. Finally, once proofs have been found by these tools, some of these provers can generate proof objects to be verified by proof checkers. This is the case of Zenon, which can produce proof objects for Coq and Dedukti, and iProver Modulo, which can also produce proof objects for Dedukti. An initial bench of 13,000 proof obligations, issued from several industrial projects, was constituted to evaluate the BWare platform. Atelier B PR prover was able to demonstrate 85% of them, Alt-Ergo 58%, iProver Modulo 19 %, and Zenon less than 1%. As can be observed, the first order provers encounter difficulties, which can be explained by the fact that these provers do not know the B set theory. At the end of the project, Alt-Ergo was able to demonstrate 98% of the PO, Zenon 95%, and iProver 28%. We also completed the set of provers: CVC4 was able to demonstrate 94% of the PO, Z3 84%, Vampire 78%, and E 61%. It appears that the project and the supply of POs has improved the performance of some provers. In the case of Alt-Ergo, the remaining POs are existential and require human intelligence to prove.

Alt-Ergo LCHIP [11] (2016-2020) was an industrial project aimed at develop-
ing a safety computer programmed with B and with enhanced proof capabili-
<figure><img src="image_6.png" /><figcaption>Fig. 6: The BWare Platform for the Automated Verification of B Proof Obligations.</figcaption></figure>

Alt-Ergo prover was selected from the excellent results obtained during the project BWare. One possibility for improvement was to specialise the production of the Why3 to exploit Alt-Ergo strong points. However the input B models, issued from the safety library, were quite different (lower level modelling) with more arithmetic and bit-wise Boolean functions. In the meantime, Why3 and its programming language WhyML have evolved enough to prevent reusing Why3 generator developed during BWare. Finally the 5000 PO generated from the safety library models were translated into SMT-LIB format and proved with 3 provers: Alt-Ergo proved 56% of the PO, CVC4 54%, and Z3 31%. The results are disappointing, but illustrate the difficulty to develop a universal prover / solver and to maintain a toolchain over the time.

*Proof drudges* DISCONT (2017-2021) aims to provide efficient and easy to use
refinement and proof-based techniques and tools that scale to complex systems
and offer more convenient and automatic proof platforms centred around B and
Event-B, with Atelier B. Iapa [4] is an extension of Atelier B aiming at both
integrating additional proof engines and offering hypotheses selection facilities
to the user. The iapa tool is invoked within Atelier B on a given component, once
the proof obligations of that component have been generated and from the XML-
based file. Navigating through these proof obligations is a first core functionality
available in iapa. Iapa comes with 6 commands for selecting hypotheses and
<figure><img src="image_8.png" /><figcaption>Fig. 6: The BWare Platform for the Automated Verification of B Proof Obligations.</figcaption></figure>

Alt-Ergo prover was selected from the excellent results obtained during the project BWare. One possibility for improvement was to specialise the production of the Why3 to exploit Alt-Ergo strong points. However the input B models, issued from the safety library, were quite different (lower level modelling) with more arithmetic and bit-wise Boolean functions. In the meantime, Why3 and its programming language WhyML have evolved enough to prevent reusing Why3 generator developed during BWare. Finally the 5000 PO generated from the safety library models were translated into SMT-LIB format and proved with 3 provers: Alt-Ergo proved 56% of the PO, CVC4 54%, and Z3 31%. The results are disappointing, but illustrate the difficulty to develop a universal prover / solver and to maintain a toolchain over the time.

*Proof drudges* DISCONT (2017-2021) aims to provide efficient and easy to use
refinement and proof-based techniques and tools that scale to complex systems
and offer more convenient and automatic proof platforms centred around B and
Event-B, with Atelier B. Iapa [4] is an extension of Atelier B aiming at both
integrating additional proof engines and offering hypotheses selection facilities
to the user. The iapa tool is invoked within Atelier B on a given component, once
the proof obligations of that component have been generated and from the XML-
based file. Navigating through these proof obligations is a first core functionality
available in iapa. Iapa comes with 6 commands for selecting hypotheses and
identifiers<sup>14</sup>, in order to limit the number of hypotheses used to prove a goal. Iapa then calls third-party provers through Why3 interface. Finally iapa offers the possibility to take into account proof obligations that are only proved by more than one external prover<sup>15</sup>, and thus to improve automatic proof percentage.

**SMT and SAT solvers** BLaSST (2022-2026) is a research project aimed at bridging combinatorial and symbolic techniques in automatic theorem proving. The current approach to encoding POs arising from B models in SMT solvers is based on rewriting set-theoretical expressions into pure first-order logic with a primitive binary predicate representing set membership. With this approach, the structure of the original formula gets lost and it introduces many quantifiers that are difficult for solvers to handle. Instead, BLaSST will enhance the solvers to handle a richer input language based on fragments of higher-order logic. In this way, sets and relations can be represented by their characteristic predicates, and the solver can exploit the structure of the original formula, flattening it only when necessary. In particular, we will explore specific strategies for handling higher-order terms that arise from expressions of the B language. The two techniques described previously will be combined in order to embed in a solver with a highly expressive input language the power to reason combinationally. Specifically, we expect that SMT solvers will be able to recognize variables for which a finite set of a priori known values can be relevant and propagate these values in the sense of SAT solving. Similar techniques are used today for reasoning efficiently about bit vectors in SMT solving, and we intend to lift them to POs arising from B models. Second, we will explore to which extent it is possible to generalize the production of counter-examples and abductive reasoning beyond SAT-based encodings. The challenge here is to find useful compromises: there is no hope for fully general techniques and some of the theoretical bases are conflicting.

**Dedukti** ICSPA (2022-2026) is a research project aimed at enabling sharing and reusing proofs and theories coming from other proof systems for both B/Event-B and TLA+. The logical framework $\lambda\mathcal{I}\mathcal{I}$-calculus modulo theory, implemented in the system Dedukti, allows to express any formal proof system. We propose to use Dedukti as a unique backend for both B/Event-B and TLA+, where proofs can be verified. This will not only provide confidence in the proofs obtained, but also enable interoperability between proofs, which goes hand in hand with interoperability of models, which we are also aiming for in this project. Importing theories from Dedukti will provide users of B/Event-B and TLA+ with access to their mutual formal library, which has been impossible until now although they are both set-theory oriented.

<footnote n="14"><sup>14</sup> identifiers are used to select hypotheses - typing hypotheses and hypotheses containing this identifier.</footnote>

<footnote n="15"><sup>15</sup> the probability that two tools developed independently show the same faulty behaviour on the same false proof obligation is neglected.</footnote>
identifiers<sup>14</sup>, in order to limit the number of hypotheses used to prove a goal. Iapa then calls third-party provers through Why3 interface. Finally iapa offers the possibility to take into account proof obligations that are only proved by more than one external prover<sup>15</sup>, and thus to improve automatic proof percentage.

SMT and SAT solvers BLaSST (2022-2026) is a research project aimed at bridging combinatorial and symbolic techniques in automatic theorem proving. The current approach to encoding POs arising from B models in SMT solvers is based on rewriting set-theoretical expressions into pure first-order logic with a primitive binary predicate representing set membership. With this approach, the structure of the original formula gets lost and it introduces many quantifiers that are difficult for solvers to handle. Instead, BLaSST will enhance the solvers to handle a richer input language based on fragments of higher-order logic. In this way, sets and relations can be represented by their characteristic predicates, and the solver can exploit the structure of the original formula, flattening it only when necessary. In particular, we will explore specific strategies for handling higher-order terms that arise from expressions of the B language. The two techniques described previously will be combined in order to embed in a solver with a highly expressive input language the power to reason combinationally. Specifically, we expect that SMT solvers will be able to recognize variables for which a finite set of a priori known values can be relevant and propagate these values in the sense of SAT solving. Similar techniques are used today for reasoning efficiently about bit vectors in SMT solving, and we intend to lift them to POs arising from B models. Second, we will explore to which extent it is possible to generalize the production of counter-examples and abductive reasoning beyond SAT-based encodings. The challenge here is to find useful compromises: there is no hope for fully general techniques and some of the theoretical bases are conflicting.

Dedukti ICSPA (2022-2026) is a research project aimed at enabling sharing and reusing proofs and theories coming from other proof systems for both B/Event-B and TLA+. The logical framework $\lambda\mathcal{I}\mathcal{I}$-calculus modulo theory, implemented in the system Dedukti, allows to express any formal proof system. We propose to use Dedukti as a unique backend for both B/Event-B and TLA+, where proofs can be verified. This will not only provide confidence in the proofs obtained, but also enable interoperability between proofs, which goes hand in hand with interoperability of models, which we are also aiming for in this project. Importing theories from Dedukti will provide users of B/Event-B and TLA+ with access to their mutual formal library, which has been impossible until now although they are both set-theory oriented.

<footnote n="14"><sup>14</sup> identifiers are used to select hypotheses - typing hypotheses and hypotheses containing this identifier.</footnote>

<footnote n="15"><sup>15</sup> the probability that two tools developed independently show the same faulty behaviour on the same false proof obligation is neglected.</footnote>
**AI for Easing Proof Process** AIDOART (2021-2024) is a research project aimed at providing a model-based framework to more efficiently support the continuous software and system engineering of CPSs and CPSoS via AI-augmentation. Our main goal is to develop a module within the Interactive prover that can learn interactive theorem proving from the developer and adapt it to unsolved proofs of the system. Such a module is also expected to provide hints based on PO inspection, rules database survey, and analysis of existing PO demonstration for the project. In this respect, examples of railways systems written in B, with complete specifications and thousands of proofs, are going to be used to train machine learning infrastructure. Unsupervised and supervised learning phases are expected to provide automatic demonstration. Another phase will address the commands with parameters and possibly the reuse / generation of mathematical rules.

**Model Editor with Proof Information** Atelier B contains a model editor merging model and proof (Fig. 7) by displaying the number of proof obligations associated to any line of a B model, its current proof status (fully proved or not) and the body of the related proof obligations.

<figure><img src="image_7.png" /><figcaption>Fig. 7: Atelier B model editor showing proof status.</figcaption></figure>

**Proof Obligation Data Set to Experiment with Third-Party Provers** Apero <fnref n="16" /> (Atelier B oPEn ResSources) is a repository providing resources collected during the last decades, for software component development using the B method and for system modelling using Event-B. Proof obligations are anonymous (identifiers are replaced by random ones). They are issued from industry projects involving

<footnote n="16">¹⁶ https://github.com/CLEARSY/apero</footnote>
**AI for Easing Proof Process** AIDOART (2021-2024) is a research project aimed at providing a model-based framework to more efficiently support the continuous software and system engineering of CPSs and CPSoS via AI-augmentation. Our main goal is to develop a module within the Interactive prover that can learn interactive theorem proving from the developer and adapt it to unsolved proofs of the system. Such a module is also expected to provide hints based on PO inspection, rules database survey, and analysis of existing PO demonstration for the project. In this respect, examples of railways systems written in B, with complete specifications and thousands of proofs, are going to be used to train machine learning infrastructure. Unsupervised and supervised learning phases are expected to provide automatic demonstration. Another phase will address the commands with parameters and possibly the reuse / generation of mathematical rules.

**Model Editor with Proof Information** Atelier B contains a model editor merging model and proof (Fig. 7) by displaying the number of proof obligations associated to any line of a B model, its current proof status (fully proved or not) and the body of the related proof obligations.

<figure><img src="image_9.png" /><figcaption>Fig. 7: Atelier B model editor showing proof status.</figcaption></figure>

**Proof Obligation Data Set to Experiment with Third-Party Provers** Apero <fnref n="16" /> (Atelier B oPEn ResSources) is a repository providing resources collected during the last decades, for software component development using the B method and for system modelling using Event-B. Proof obligations are anonymous (identifiers are replaced by random ones). They are issued from industry projects involving

<footnote n="16">¹⁶ https://github.com/CLEARSY/apero</footnote>
a large range of human modellers and providing some diversity some diversity
in the style. Most of the B operators appear in the POs. All proof obligations
are considered true as they were demonstrated automatically or interactively for
these projects. As such, they provide a solid basis for the evaluation of provers.

8 Conclusion and Perspectives

This article presents the development and improvement cycle of the Atelier B
prover over the last 30 years. This tool was designed and developed within an in-
dustrial framework with a regulatory objective of certifiability. Regular scientific
work has validated certain aspects. However, the impossibility of correcting the
proof kernel made it necessary to connect and use third-party proof tools. The
increase in processor performance allowed the automatic demonstration timing
requirement (10 seconds meantime) to be met. Research projects managed to
increase automatic proof rate from 75% to 98% on some specific kind of mod-
elling. The combination of tools with the same positive result has improved their
level of confidence and allowed their use in industrial setting. However a number
of challenges remain:

- Proof obligations requiring human intelligence to complete - for example, finding the correct valuation of an existential one. Event-B solve the issue by requiring this value to be part of the model as a witness.

- Merging demonstrations when the modelling is modified. Keeping interactive demonstrations associated to a given PO is difficult, especially when the model is highly refactored.

- Finding counter examples. Trying to demonstrate false proof obligations is a loss. Identifying false proof obligations by exhibiting counter examples would help models to converge quicker.

- Helping to add easing modelling assertions. Assertions appear as hypotheses in proof obligations and could help to demonstrate POs. Suggesting assertions while modelling would also help to converge quicker towards a correct model.

- Stating the equivalence between 2 proof obligation generators. The development of two different tools, with different implementations and optimisations, leads to two different sets of POs that are not trivial to compare as both the hypotheses and goals could have different shapes.

Acknowledgements

The work and results described in this article were partly funded by:

- ECSEL JU under the framework H2020, as part of the project AIDOaRt (AI-augmented automation supporting modelling, coding, testing, monitoring and continuous development in Cyber-Physical Systems).

- ANR under the framework "appel à projets générique 2020", as part of the project ICSPA (Interoperable and Confident Set-based Proof Assistants).
a large range of human modellers and providing some diversity some diversity
in the style. Most of the B operators appear in the POs. All proof obligations
are considered true as they were demonstrated automatically or interactively for
these projects. As such, they provide a solid basis for the evaluation of provers.

8 Conclusion and Perspectives

This article presents the development and improvement cycle of the Atelier B
prover over the last 30 years. This tool was designed and developed within an in-
dustrial framework with a regulatory objective of certifiability. Regular scientific
work has validated certain aspects. However, the impossibility of correcting the
proof kernel made it necessary to connect and use third-party proof tools. The
increase in processor performance allowed the automatic demonstration timing
requirement (10 seconds meantime) to be met. Research projects managed to
increase automatic proof rate from 75% to 98% on some specific kind of mod-
elling. The combination of tools with the same positive result has improved their
level of confidence and allowed their use in industrial setting. However a number
of challenges remain:

- Proof obligations requiring human intelligence to complete - for example, finding the correct valuation of an existential one. Event-B solve the issue by requiring this value to be part of the model as a witness.

- Merging demonstrations when the modelling is modified. Keeping interactive demonstrations associated to a given PO is difficult, especially when the model is highly refactored.

- Finding counter examples. Trying to demonstrate false proof obligations is a loss. Identifying false proof obligations by exhibiting counter examples would help models to converge quicker.

- Helping to add easing modelling assertions. Assertions appear as hypotheses in proof obligations and could help to demonstrate POs. Suggesting assertions while modelling would also help to converge quicker towards a correct model.

- Stating the equivalence between 2 proof obligation generators. The development of two different tools, with different implementations and optimisations, leads to two different sets of POs that are not trivial to compare as both the hypotheses and goals could have different shapes.

Acknowledgements

The work and results described in this article were partly funded by:

- ECSEL JU under the framework H2020. as part of the project AIDOaRt (AI-augmented automation supporting modelling, coding, testing, monitoring and continuous development in Cyber-Physical Systems).

- ANR under the framework "appel à projets générique 2020", as part of the project ICSPA (Interoperable and Confident Set-based Proof Assistants).
References

1. Abrial, J.: The B-book - assigning programs to meanings. Cambridge University Press (2005)

2. Abrial, J.R., Cansell, D.: Click'n prove: Interactive proofs within set theory. In: TPHOLs (2003)

3. Berkani, K., Dubois, C., Faivre, A., Falampin, J.: Validation des règles de base de l'atelier b. Technique et Science Informatiques 23, 855-878 (07 2004)

4. Burdy, L., Deharbe, D., Prun, E.: Interfacing automatic proof agents in atelier b: Introducing iapa. Electronic Proceedings in Theoretical Computer Science 240 (01 2017)

5. Burdy, L., Dufour, J.L., Lecomte, T.: The b method takes up floating-point numbers (2011)

6. Cirstea, H., Kirchner, C.: Theorem proving using computational systems: The case of the b predicate prover (04 2000)

7. Cirstea, H., Kirchner, C.: Using rewriting and strategies for describing the b predicate prover (01 2001)

8. Clearasy: Proof Obligations Reference Manual 3.7

9. Delahaye, D., Dubois, C., Marché, C., Mentré, D.: The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. In: Abstract State Machines, Alloy, B, VDM, and Z - 5th Int'l Conf., ABZ 2016, Linz, Austria, May 23-27, 2016, Proc. LNCS, vol. 9675, pp. 167-182. Springer (2016)

https://hal.archives-ouvertes.fr/hal-00998092

10. Hansen, D., Schneider, D., Leuschel, M.: Using B and prob for data validation projects. In: Butler, M.J., Schewe, K., Mashkoor, A., Biró, M. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th Int'l Conf., ABZ 2016, Linz, Austria, May 23-27, 2016, Proc. LNCS, vol. 9675, pp. 167-182. Springer (2016)

11. Lecomte, T., Déharbe, D., Sabatier, D., Prun, E., Péronne, P., Chailloux, E., Varoumas, S., Susungi, A., Conchon, S.: Low Cost High Integrity Platform. In: ERTS 2020 - 10th European Congress on Embedded Real Time Systems. Toulouse, France (Jan 2020), https://hal.archives-ouvertes.fr/hal-02446132

12. Leuschel, M., Butler, M.: Prob: A model checker for b. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: Formal Methods. pp. 855-874. Springer Berlin Heidelberg, Berlin, Heidelberg (2003)

13. Romanovsky, A.: After and outside DEPLOY: The deploy ecosystem, pp. 197-202 (07 2013)

14. Wikipedia contributors: Xslt — Wikipedia, the free encyclopedia (2023), https://en.wikipedia.org/wiki/XSLT
References

1. Abrial, J.: The B-book - assigning programs to meanings. Cambridge University Press (2005)

2. Abrial, J.R., Cansell, D.: Click'n prove: Interactive proofs within set theory. In: TPHOLs (2003)

3. Berkani, K., Dubois, C., Faivre, A., Falampin, J.: Validation des règles de base de l'atelier b. Technique et Science Informatiques 23, 855-878 (07 2004)

4. Burdy, L., Deharbe, D., Prun, E.: Interfacing automatic proof agents in atelier b: Introducing iapa. Electronic Proceedings in Theoretical Computer Science 240 (01 2017)

5. Burdy, L., Dufour, J.L., Lecomte, T.: The b method takes up floating-point numbers (2011)

6. Cirstea, H., Kirchner, C.: Theorem proving using computational systems: The case of the b predicate prover (04 2000)

7. Cirstea, H., Kirchner, C.: Using rewriting and strategies for describing the b predicate prover (01 2001)

8. Clearasy: Proof Obligations Reference Manual 3.7

9. Delahaye, D., Dubois, C., Marché, C., Mentré, D.: The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. In: Abstract State Machines, Alloy, B, VDM, and Z - 5th Int'l Conf., ABZ 2016, Linz, Austria, May 23-27, 2016, Proc. LNCS, vol. 9675, pp. 167-182. Springer (2016)

https://hal.archives-ouvertes.fr/hal-00998092

10. Hansen, D., Schneider, D., Leuschel, M.: Using B and prob for data validation projects. In: Butler, M.J., Schewe, K., Mashkoor, A., Biró, M. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th Int'l Conf., ABZ 2016, Linz, Austria, May 23-27, 2016, Proc. LNCS, vol. 9675, pp. 167-182. Springer (2016)

11. Lecomte, T., Déharbe, D., Sabatier, D., Prun, E., Péronne, P., Chailloux, E., Varoumas, S., Susungi, A., Conchon, S.: Low Cost High Integrity Platform. In: ERTS 2020 - 10th European Congress on Embedded Real Time Systems. Toulouse, France (Jan 2020), https://hal.archives-ouvertes.fr/hal-02446132

12. Leuschel, M., Butler, M.: Prob: A model checker for b. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: Formal Methods. pp. 855-874. Springer Berlin Heidelberg, Berlin, Heidelberg (2003)

13. Romanovsky, A.: After and outside DEPLOY: The deploy ecosystem, pp. 197-202 (07 2013)

14. Wikipedia contributors: Xslt — Wikipedia, the free encyclopedia (2023), https://en.wikipedia.org/wiki/XSLT