Librerie scritte in Coq
stalin-sort
Aggiungi un algoritmo di ordinamento stalin in qualsiasi lingua ti piaccia ❣️ se ti piace dacci un ⭐️.
- 1.2k
- MIT
UniMath
Questa libreria coq mira a formalizzare un corpus sostanziale di matematica utilizzando il punto di vista univalente..
- 853
- GNU General Public License v3.0
magmide
Un linguaggio di prova tipizzato in modo dipendente inteso a rendere possibile un codice bare metal dimostrabilmente corretto per gli ingegneri del software che lavorano.
- 771
fiat-crypto
Generazione di codice primitivo crittografico da parte di Fiat.
- 594
- GNU General Public License v3.0
CoqGym
Un ambiente di apprendimento per la dimostrazione di teoremi con l'assistente di prova Coq.
- 332
- GNU Lesser General Public License v3.0 only
proofs
Il mio archivio personale di matematica formalmente verificata...
- 259
- GNU General Public License v3.0
Coq-Equations
Un pacchetto di definizione di funzione per Coq.
- 197
- GNU Lesser General Public License v3.0 only
verdi-raft
Un'implementazione del protocollo di consenso distribuito Raft, verificato in Coq utilizzando il framework Verdi.
- 168
- BSD 2-clause "Simplified"
jasmin
Linguaggio per la crittografia ad alta sicurezza e ad alta velocità (di jasmin-lang).
- 159
- MIT
analysis
Libreria di analisi conforme ai componenti matematici (di math-comp).
- 158
- GNU General Public License v3.0
fiat
Sintesi per lo più automatizzata di programmi Correct-by-Construction.
- 140
- GNU General Public License v3.0
kami
Una piattaforma per specifiche hardware parametriche di alto livello e la sua verifica modulare (di mit-plv).
- 126
- MIT
toychain
Un consenso blockchain minimalista implementato e verificato in Coq.
- 106
- BSD 2-clause "Simplified"
koika
Un linguaggio di base per la progettazione hardware basata su regole 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
Specifiche formali e verifica dell'hardware, in particolare per la sicurezza e la privacy.
- 97
- Apache License 2.0
coq-library-undecidability
Una libreria di prove di indecidibilità meccanizzate nell'assistente di prova Coq..
- 96
- GNU General Public License v3.0
vericert
Uno strumento di sintesi di alto livello formalmente verificato basato su CompCert e scritto in Coq..
- 71
- GNU General Public License v3.0 only
scala-escape
Un plug-in del compilatore per controllare la durata degli oggetti in Scala (di TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"