Bon pr etre précis ... météor a été analysé avec la méthode SADT puis écrit en langage B (c pas de la prog c des preuves)

120 000 lignes de B ont donné, après 30 000 preuves, dans les 80-90000 lignes de code ADA

=> 1er essai == 0 bugs

pas mal nan ?


ensuite pour les preuves je peux vous donner des exemples mais c pas tres compréhensible ^^