The purpose of this thesis is the verification of Atelier B added rules using the framework named BCARe which relies on a deep embedding of the B theory within the logic of the Coq proof assistant. We propose especially three approaches in order to prove the validity of a rule, which amounts to prove a formula expressed in the B theory. These three approaches have been assessed on the rules coming from the rule database maintained by Siemens IC-MOL. To do so, the first approach, so-called autarkic approach, is developed thanks to the Coq tactic language, Ltac. It rests upon a first step which consists in unfolding the set operators so as to obtain a first order formula. A decision procedure which implements an heuristic is applied afterwards to deal with instantiation. We propose a second approach, so-called skeptic approach, which uses the automated first order theorem prover Zenon, after the previous normalization step has been applied. Then we verify the Zenon proofs in the deep embedding of B in Coq. A third approach consists in using anextension of Zenon to the B method thanks to the superdeduction. Superdeduction allows us to add the axioms of the B theory by means of deduction rules in the proof mechanism of Zenon. This last approach is generalized in an extension of Zenon to every theory thanks to a dynamic calculus of the superdeduction rules. This new tool, named Super Zenon, is able to prove problems coming from the problem library TPTP, for example.
