A ce jour, les méthodes formelles ont montré qu'elles étaient applicables avec succès au développement de logiciels industriels. Pour maîtriser la complexité croissante de ces applications, la mise en oeuvre des paradigmes d'abstraction et de composition est incontournable. La méthode B permet d'assister le processus de développement des spécifications au code et offre une notion de modularité qui permet de composer à la fois les spécifications et les développements. La compositionnalité des preuves est assurée par des restrictions imposées par le langage, qui limitent les formes d'architectures autorisées. A la suite de nos précédents travaux, le manuscrit présenté ici explicite les principes de composition des spécifications et des développements, énonce les théorèmes sous-jacents à la composition des preuves et complète et valide les restrictions imposées par la méthode B. Bien que dédiés à la méthode B, les résultats présentés sont plus généraux : ils peuvent s'appliquer à d'autres approches formelles basées sur la notion d'état, comme les approches objet