Pour être plus précis : Astrée a prouvé l'absence d'erreurs d'exécution dans le "primary flight control software" de l'Airbus A380. Et surtout, le plus impressionnant, c'est qu'en plus la preuve a signalé 0 fausses alertes (un logiciel de ce type ne laisse passer aucune erreur, mais peut parfois signaler des choses qu'il trouve bizarres mais qui en fait ne sont pas des erreurs : des fausses alertes).