Méthodes formelles & preuves mathématiques
Nous prouvons mathématiquement que votre code fait ce qu'il doit, et rien d'autre. Alt-Ergo, Rocq, Why3 : les outils de référence de la vérification formelle industrielle, développés et maintenus par nos équipes.
Preuves de programmes avec Rocq
Spécification et vérification formelle interactive. Nous développons des preuves mathématiques de correction de vos algorithmes critiques avec le prouveur Rocq (ex-Coq).
Solveur SMT Alt-Ergo
Notre solveur SMT open source, moteur de preuve derrière Frama-C, SPARK, Why3, Atelier B et EasyCrypt. En production chez AdaCore, Thales, CEA List et Mitsubishi Electric.
Certification haute assurance
Vérification formelle pour les processus de certification Critères Communs, de la diffusion restreinte jusqu'au niveau EAL6+.
Alt-Ergo : le solveur SMT de référence
Développé depuis 2006, maintenu par OCamlPro depuis 2013. Moteur de preuve derrière Frama-C, SPARK (Ada), Why3, Atelier B et EasyCrypt. Club industriel : AdaCore, Thales, CEA List, Mitsubishi Electric. Projet DéCySif avec Inria et TrustInSoft.
Nos capacités en vérification formelle
Vérification déductive
Spécification de propriétés en logique du premier ordre, preuve automatique via Why3 et Alt-Ergo.
Preuves interactives Rocq
Développement de preuves formelles en Rocq pour les algorithmes et protocoles les plus exigeants : correction, terminaison, absence d'erreurs.
Analyse de code C
Via Frama-C avec Alt-Ergo comme backend : absence de comportements indéfinis, overflows, violations mémoire.
Vérification de programmes Rust
Avec Creusot, notre outil de vérification formelle pour Rust : annotations de contrats, preuves de correction automatisées.
Formation méthodes formelles
Formations en Rocq, Alt-Ergo et vérification déductive. Certifiées Qualiopi, finançables OPCO, dispensées par les auteurs des outils.
Problèmes résolus par la preuve formelle
Systèmes critiques sans bug prouvé
Éliminer par preuve les classes entières de vulnérabilités : dépassements mémoire, erreurs arithmétiques, conditions de course.
Certification EAL5 et EAL6+
Prouver formellement les propriétés de sécurité exigées pour les niveaux d'assurance les plus élevés des Critères Communs.
Vérification Ada via SPARK
Alt-Ergo est le moteur de preuve de SPARK, l'outil de vérification formelle de référence pour les programmes Ada.
Protocoles cryptographiques
Vérification d'implémentations cryptographiques via EasyCrypt avec Alt-Ergo, pour prouver la sécurité de vos protocoles.