Biblioteker skrevet i Coq
stalin-sort
Tilføj en stalin-sorteringsalgoritme på ethvert sprog, du kan lide ❣️ hvis du vil, giv os en ⭐️.
- 1.2k
- MIT
UniMath
Dette coq-bibliotek har til formål at formalisere en betydelig mængde af matematik ved at bruge det univalente synspunkt.
- 853
- GNU General Public License v3.0
magmide
Et afhængigt skrevet korrektursprog beregnet til at muliggøre beviseligt korrekt bar metal-kode for arbejdende softwareingeniører.
- 771
CoqGym
Et læringsmiljø for sætningsbevis med Coq-bevisassistenten.
- 332
- GNU Lesser General Public License v3.0 only
verdi-raft
En implementering af Rafts distribuerede konsensusprotokol, verificeret i Coq ved hjælp af Verdi-rammen.
- 168
- BSD 2-clause "Simplified"
analysis
Mathematical Components-kompatibelt Analysebibliotek (ved math-comp).
- 158
- GNU General Public License v3.0
fiat
For det meste automatiseret syntese af korrekt-for-konstruktion-programmer.
- 140
- GNU General Public License v3.0
kami
En platform for parametrisk hardwarespecifikation på højt niveau og dens modulære verifikation (af mit-plv).
- 126
- MIT
toychain
En minimalistisk blockchain-konsensus implementeret og verificeret i Coq.
- 106
- BSD 2-clause "Simplified"
silveroak
Formel specifikation og verifikation af hardware, især for sikkerhed og privatliv.
- 97
- Apache License 2.0
coq-library-undecidability
Et bibliotek med mekaniserede beviser for uafgørlighed i Coq-korrekturassistenten.
- 96
- GNU General Public License v3.0
vericert
Et formelt verificeret synteseværktøj på højt niveau baseret på CompCert og skrevet i Coq..
- 71
- GNU General Public License v3.0 only
scala-escape
Et compiler-plugin til at styre objektlevetider i Scala (af TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"