Gappa est un outil dédié à la vérification et à la preuve formelle des propriétés de programmes numériques s'appuyant sur de l'arithmétique à virgule flottante ou fixe. Il a été utilisé pour écrire des filtres flottants robustes pour CGAL et pour certifier les fonctions élémentaires de CRlibm. Gappa est conçu pour être utilisé directement, mais il peut aussi être utilisé comme prouveur automatique pour la plateforme de vérification de logiciels Why3 ou comme tactique pour l'assistant de preuve Coq.
