ProB model-checker is being integrated in Atelier B 4.0, in order to provide additional 
proof power and animation capabilities to Atelier B.
With the help of Pr. Michael Leuschel, a MacOS prototype has been developped, allowing to animate and model-check a B model from Atelier B 4.0. At that occasion, a generic interfacing mechanism has been developped and will be enriched and improved in the future. This mechanism is described in the GUI_Project section. ProB 1.3.0+ is now self integrating with AtelierB 4.0, at model level. Ongoing developments at University of Dusseldorf for integration at proof obligation level.