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.1k
- MIT
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é.
- 672
fiat-crypto
Génération de code primitif cryptographique par Fiat.
- 470
- GNU General Public License v3.0
CoqGym
Un environnement d'apprentissage pour la preuve de théorèmes avec l'assistant de preuve Coq.
- 282
- GNU Lesser General Public License v3.0 only
Coq-Equations
Un package de définition de fonction pour Coq.
- 175
- 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.
- 155
- BSD 2-clause "Simplified"
fiat
Synthèse principalement automatisée de programmes de correction par construction.
- 130
- 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).
- 113
- MIT
silveroak
Spécification formelle et vérification du matériel, en particulier pour la sécurité et la confidentialité.
- 97
- Apache License 2.0
toychain
Un consensus blockchain minimaliste implémenté et vérifié en Coq.
- 96
- BSD 2-clause "Simplified"
koika
Un langage de base pour la conception matérielle basée sur des règles 🦑.
- 88
- GNU General Public License v3.0 only
coq-library-undecidability
Une bibliothèque de preuves mécanisées d'indécidabilité dans l'assistant de preuve Coq.
- 76
- GNU General Public License v3.0
colorlight-led-cube
Cube LED 64x64 basé sur la carte de commande LED Colorlight 5a-75B.
- 74
- 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).
- 61
- BSD 3-clause "New" or "Revised"
vericert
Un outil de synthèse de haut niveau formellement vérifié basé sur CompCert et écrit en Coq.
- 59
- GNU General Public License v3.0 only
comonad-transformers
Transformateurs Haskell 98 comonad - à partir de la version 4.0, ils ont fusionné dans le package comonad.
- 12
- BSD 3-clause "New" or "Revised"