Un article de ce site fait référence à la revue Technique et science informatique, qui dans son volume 22 (numéro 1 de 2003) dirigé par Véronique Viguié-Donzeau-Gouge, Didier Bert et Henri Habrias, a publié un article de Daniel Dollé, Didier Essamé et Jérôme Falampin consacré à l’écriture du logiciel de contrôle et de pilotage de la ligne de métro sans conducteur METEOR construite par Siemens à Paris. On y apprend que le noyau de sécurité de ce logiciel a été développé par la méthode B, qui consiste à élaborer la preuve de la correction du programme en même temps que son code, ce qui fournit une démonstration formelle de justesse. Avec la méthode B on écrit en langage Z, qui compile vers Ada. Bon, ceci ne concerne que le noyau de sécurité du logiciel, le reste a peut-être été écrit en Eiffel. Et depuis 2003 les choses ont pu changer.