A quick search on METEOR Ada on http://www.google.com gives: http://www.atelierb.societe.com/other_papers/english/using_B/using_B.htm http://www.atelierb.societe.com/other_papers/french/utilise_B/utilisation_de_B.htm It gives some insight on how the thing was formally validated. There is the email of an RATP guy in the French version. --LG