Bibliothèques écrites en Coq
stalin-sort
Ajoutez un algorithme de tri de Staline dans la langue de votre choix ❣️ si vous aimez, donnez-nous un ⭐️.
- 1.2k
- MIT
Coq-HoTT
Une bibliothèque Coq pour la théorie des types homotopiques.
- 1.2k
- GNU General Public License v3.0
UniMath
Cette bibliothèque coq vise à formaliser un corpus conséquent de mathématiques en utilisant le point de vue univalent.
- 853
- GNU General Public License v3.0
magmide
Un langage de preuve typé de manière dépendante destiné à rendre possible un code bare metal correct et prouvé pour les ingénieurs logiciels en activité.
- 771
fiat-crypto
Génération de code primitif cryptographique par Fiat.
- 594
- GNU General Public License v3.0
CoqGym
Un environnement d'apprentissage pour la preuve de théorèmes avec l'assistant de preuve Coq.
- 332
- GNU Lesser General Public License v3.0 only
proofs
Mon référentiel personnel de mathématiques formellement vérifiées..
- 259
- GNU General Public License v3.0
Coq-Equations
Un package de définition de fonction pour Coq.
- 197
- GNU Lesser General Public License v3.0 only
verdi-raft
Une implémentation du protocole de consensus distribué Raft, vérifiée en Coq à l'aide du framework Verdi.
- 168
- BSD 2-clause "Simplified"
analysis
Bibliothèque d'analyse conforme aux composants mathématiques (par math-comp).
- 158
- GNU General Public License v3.0
fiat
Synthèse principalement automatisée de programmes de correction par construction.
- 140
- GNU General Public License v3.0
kami
Une plate-forme pour la spécification matérielle paramétrique de haut niveau et sa vérification modulaire (par mit-plv).
- 126
- MIT
toychain
Un consensus blockchain minimaliste implémenté et vérifié en Coq.
- 106
- BSD 2-clause "Simplified"
koika
Un langage de base pour la conception matérielle basée sur des règles 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
Spécification formelle et vérification du matériel, en particulier pour la sécurité et la confidentialité.
- 97
- Apache License 2.0
coq-library-undecidability
Une bibliothèque de preuves mécanisées d'indécidabilité dans l'assistant de preuve Coq.
- 96
- GNU General Public License v3.0
vericert
Un outil de synthèse de haut niveau formellement vérifié basé sur CompCert et écrit en Coq.
- 71
- GNU General Public License v3.0 only
scala-escape
Un plug-in de compilateur pour contrôler la durée de vie des objets dans Scala (par TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"